<p>While I am not aware of any such results, other than your own, I think you could broaden the scope somewhat and ask: what results in TCS have been proved using (any kind of) non-standard axioms. By non-standard here I mean something other than classical logic with ZF (or ZFC).</p>

<p>A beautiful example of the kind of work I have in mind are Alex Simpson's results on properties of programming languages using synthetic domain theory. He uses intuitionistic set theory with axioms that contradict classical logic.</p>

<p>Also, Alex and I used intuitionistic axioms with anti-classical continuity principles to show results about Banach-Mazur computabilty.</p>

<p>However, none of the mentioned examples have an "open" status, like your proofs, because we know that the non-standard axioms we used can be understood simply as working inside a model of intuitionistic mathematics, where the model can be shown to exist in ZFC. So the non-standard setup is really a way of getting things done more elegantly, and in principle they could be done in straight ZFC (although I am afraid to think about how exactly that would go).</p>

CC BY-SA 3.0
2011-04-08T11:20:03.013Z
Thank you! I'll ask alex more details about this when I'll be writing the introduction.
OldFella
CC BY-SA 3.0
2011-04-08T09:12:27.973Z
2011-04-08T09:12:27.973Z
Andrej Bauer
<p>It depends on your definition of "Computer Science". Take the example below - does it count?</p>

<p>A <em>coding of the integers</em> is a uniquely decodable binary code of $\mathbb{N}$. If the length of the codewords is non-decreasing we call the code <em>monotone</em>. A code $C_1$ is <em>better</em> than a code $C_2$ if $|C_1(n)| - |C_2(n)| \rightarrow -\infty$. In other words, for every $L$, from some point on the codewords of $C_1$ are at least $L$ bits shorter.</p>

<p>A set of codes $S$ is called <em>cofinal</em> if for every code $C$ there is a code $D \in S$ which is better than $C$. It is well-ordered if it is well-ordered with respect to "better". A <em>scale</em> is a well-ordered cofinal set of codes.</p>

<p>Here are two properties which are independent of ZFC:</p>

<ol>
<li>There exists a scale of codes.</li>
<li>There exists a scale of monotone codes (i.e. a well-ordered set of monotone codes which is cofinal in the set of all monotone codes).</li>
</ol>

CC BY-SA 3.0
2011-04-10T09:32:15.157Z
Hello Yuval, thanks for the answer.
I'm not sure your example fits my definition "Computer Science". Surely talking about "codes" is not enough for classifying it as CS. What makes a paper "a CS paper" imho is the following:

Did it appeared in some CS conference/journal, or was it used to prove some result in CS conference/journal? by CS paper i'm quite flexible but topics might be "information theory, complexity, program/system logics, recursion theory" etc.

Anyway can you cite the source of the example and/or  papers which make use of "there exists a scale of codes"? Thanks! Bye
OldFella
CC BY-SA 3.0
2011-04-10T15:36:49.883Z
Papers about codes of the integers appear in electrical engineering journals, such as the IEEE transactions on information theory. That hits one of your keywords.
Yuval Filmus
CC BY-SA 3.0
2011-04-10T15:38:11.770Z
I don't think there's any paper using these results. Moreover, I strongly believe that a result independent of ZFC has no use in complexity, so in a sense your question is about stretching the limits of what's considered computer science.
Yuval Filmus
CC BY-SA 3.0
2011-04-10T20:16:14.290Z
Hello Yuval, first of all let me thank you again for the answers.

I don't agree with your strong position however. For example the Robertson-Seymour theorem (which seems to require choice) has important consequences in complexity. So it is clear the Choice is useful (perhaps a bit surprisingly) in Complexity theory. 

Now working with consistent extensions of ZFC obviously simplify the task of proving, complexity say, results, even if these results are maybe  provable in ZFC but nobody know how, yet.
OldFella
CC BY-SA 3.0
2011-04-10T20:17:49.283Z
Furthermore I don't see why there shouldn't be concrete results in complexity independent of ZFC, in the same way the Robertson-Seymour  theorem is (perhaps) independent of ZF.
OldFella
CC BY-SA 3.0
2011-04-11T02:42:21.043Z
I agree that AC may be used implicitly, but if you ask a random complexity theorist whether her latest proof uses AC, I'm not sure you'll get any meaningful answer. The moral is that AC is taken for granted, and as for other axioms, it's hard to imagine a natural situation where they'd be relevant.
Yuval Filmus
CC BY-SA 3.0
2011-04-13T12:04:12.703Z
@Yuval, Harvey Friedman may disagree with you. :)
Kaveh
CC BY-SA 3.0
2012-03-15T05:30:39.977Z
@MatteoMio Robertson-Seymour theorem doesn't need AC, read this: http://cstheory.blogoverflow.com/2011/09/what-does-it-really-mean-to-prove-the-graph-minor-theorem/
didest
CC BY-SA 3.0
2011-04-09T23:45:46.433Z
2011-04-09T23:45:46.433Z
Yuval Filmus
<p>A <em>cone</em> of Turing degrees is a set $D$ of degrees with some base $b \in D$ such that for all degrees $c$, $b \leq_T c$ if and only if $c \in D$.</p>

<p>The statement of <em>Turing degree determinacy</em>:</p>

<blockquote>
  <p>Every set of Turing degrees either contains a cone or is disjoint from some cone</p>
</blockquote>

<p>is a consequence of the axiom of determinacy (AD), which is independent of ZF and incompatible with ZFC. The weaker statement </p>

<blockquote>
  <p>Every Borel set of reals that is closed under Turing equivalence either contains a cone or is disjoint from a cone </p>
</blockquote>

<p>is a consequence of Martin's theorem on Borel determinacy, which is provable in ZFC. Both of these statements were studied before Martin's result on Borel determinacy was proved, at which time it was only known that they are both provable in ZF+AD. </p>

<p>The second quoted result has the following interesting conclusion: suppose that $S$ is a Borel set of reals closed under Turing equivalence such that for every real $b$ there is some $c \in S$ with $b \leq_T c$ (this just says that $S$ is upwards dense in the Turing degrees). Then $S$ must contain an entire cone of Turing degrees. </p>

CC BY-SA 3.0
2012-03-14T21:04:41.123Z
2012-03-14T21:12:10.710Z
2012-03-14T21:12:10.710Z
Carl Mummert
<p>I recently attended a talk with one such result, for the determinacy of one-counter Büchi games: Olivier Finkel, <em>The Determinacy of Context-Free Games</em>, STACS 2012, <a href="http://drops.dagstuhl.de/opus/volltexte/2012/3389/pdf/5.pdf" rel="noreferrer">http://drops.dagstuhl.de/opus/volltexte/2012/3389/pdf/5.pdf</a>.</p>

CC BY-SA 3.0
2012-03-15T07:35:14.767Z
2012-03-15T07:35:14.767Z
Sylvain
<p>A lot of constructive mathematics. See Per Martin-Löf's work on constructive set theory, used as a basis for dependently-typed programming languages.</p>

CC BY-SA 3.0
2011-04-08T09:39:46.033Z
IIRC, Martin-Lof type theory has the same consistency strength as Kripke-Platek set theory, which is vastly weaker than ZFC. Also, MLTT doesn't have any explicitly anti-classical principles, like the continuity axioms Andrej mentioned.
Neel Krishnaswami
CC BY-SA 3.0
2011-04-09T07:39:55.160Z
@Neel I never said anything about consistency or strength of MLTT. However, I consider some results in constructive mathematics to be relevant to the question, asking for "interesting result in CS which is ... independent of ZFC".
Rob
CC BY-SA 3.0
2011-04-09T23:52:03.890Z
I assume "independent" here is meant in the formal sense.
Mark Reitblatt
CC BY-SA 3.0
2011-04-08T09:29:39.403Z
2011-04-08T09:29:39.403Z
Rob
<p>I'm going to ask a quite vague question, since the borderline between theoretical computer science and math is not always easy to distinguish.</p>

<p><strong>QUESTION:</strong> Are you aware of any interesting result in CS which 
is either independent of ZFC (i.e. standard set theory),
or that was originally proven in ZFC (+ some other axiom) and only later proven in ZFC alorne?</p>

<p>I'm asking because I'm close to finish my PhD thesis, and my main result (the determinacy of a class of games which are used to give "game semantics" to a probabilistic modal $\mu$-calculus) is at the moment proven in ZFC extended with other Axioms (namely the negation of the Continuum hypothesis $\neg CH $ and, Martin's Axiom $MA$).</p>

<p>So the setting is clearly Computer Science (the modal $\mu$-calculus is a temporal logic, and I'm extending it to work with probabilistic systems).</p>

<p>I would like to cite in my thesis other examples (if you are aware of any) of this kind.</p>

<p>Thank you in advance,</p>

<p>bye</p>

<p>Matteo </p>

CC BY-SA 2.5
2011-04-07T18:07:26.077Z
These previous questions might be helpful: http://cstheory.stackexchange.com/questions/4816/axioms-necessary-for-theoretical-computer-science http://cstheory.stackexchange.com/questions/1923/which-interesting-theorems-in-tcs-rely-on-the-axiom-of-choice-or-alternatively
Mark Reitblatt
CC BY-SA 3.0
2011-04-08T09:04:01.397Z
I was going to answer that Matteo Mio and Alex Simpson used Martin's Axiom to prove very interesting results...
Andrej Bauer
CC BY-SA 3.0
2011-04-08T13:11:25.140Z
This may be the best example I've seen of a question whose best answer is contained in the question itself!  I was unaware of your very interesting result.
Timothy Chow
<reference-request><lo.logic><set-theory>
Results in Theoretical CS independent of ZFC
OldFella
# Results in Theoretical CS independent of ZFC

(Asked by: username_0 on 2011-04-07)

I'm going to ask a quite vague question, since the borderline between theoretical computer science and math is not always easy to distinguish.

**QUESTION:** Are you aware of any interesting result in CS which
is either independent of ZFC (i.e. standard set theory),
or that was originally proven in ZFC (+ some other axiom) and only later proven in ZFC alorne?

I'm asking because I'm close to finish my PhD thesis, and my main result (the determinacy of a class of games which are used to give "game semantics" to a probabilistic modal $\mu$-calculus) is at the moment proven in ZFC extended with other Axioms (namely the negation of the Continuum hypothesis $\neg CH $ and, Martin's Axiom $MA$).

So the setting is clearly Computer Science (the modal $\mu$-calculus is a temporal logic, and I'm extending it to work with probabilistic systems).

I would like to cite in my thesis other examples (if you are aware of any) of this kind.

Thank you in advance,

bye

Matteo

**Tags:** reference-request, lo.logic, set-theory

> **Comments:**
> **username_1**: These previous questions might be helpful: http://cstheory.stackexchange.com/questions/4816/axioms-necessary-for-theoretical-computer-science http://cstheory.stackexchange.com/questions/1923/which-interesting-theorems-in-tcs-rely-on-the-axiom-of-choice-or-alternatively  
> **username_2**: I was going to answer that Matteo Mio and Alex Simpson used Martin's Axiom to prove very interesting results...  
> **username_3**: This may be the best example I've seen of a question whose best answer is contained in the question itself!  I was unaware of your very interesting result.  

---

## 5 answers

### Answer by username_2 on 2011-04-08. Score: 20

While I am not aware of any such results, other than your own, I think you could broaden the scope somewhat and ask: what results in TCS have been proved using (any kind of) non-standard axioms. By non-standard here I mean something other than classical logic with ZF (or ZFC).

A beautiful example of the kind of work I have in mind are Alex Simpson's results on properties of programming languages using synthetic domain theory. He uses intuitionistic set theory with axioms that contradict classical logic.

Also, Alex and I used intuitionistic axioms with anti-classical continuity principles to show results about Banach-Mazur computabilty.

However, none of the mentioned examples have an "open" status, like your proofs, because we know that the non-standard axioms we used can be understood simply as working inside a model of intuitionistic mathematics, where the model can be shown to exist in ZFC. So the non-standard setup is really a way of getting things done more elegantly, and in principle they could be done in straight ZFC (although I am afraid to think about how exactly that would go).

> **Comments:**
> **username_0**: Thank you! I'll ask alex more details about this when I'll be writing the introduction.  

---

### Answer by username_4 on 2011-04-09. Score: 13

It depends on your definition of "Computer Science". Take the example below - does it count?

A *coding of the integers* is a uniquely decodable binary code of $\mathbb{N}$. If the length of the codewords is non-decreasing we call the code *monotone*. A code $C\_1$ is *better* than a code $C\_2$ if $|C\_1(n)| - |C\_2(n)| \rightarrow -\infty$. In other words, for every $L$, from some point on the codewords of $C\_1$ are at least $L$ bits shorter.

A set of codes $S$ is called *cofinal* if for every code $C$ there is a code $D \in S$ which is better than $C$. It is well-ordered if it is well-ordered with respect to "better". A *scale* is a well-ordered cofinal set of codes.

Here are two properties which are independent of ZFC:

1. There exists a scale of codes.
2. There exists a scale of monotone codes (i.e. a well-ordered set of monotone codes which is cofinal in the set of all monotone codes).

> **Comments:**
> **username_0**: Hello Yuval, thanks for the answer. I'm not sure your example fits my definition "Computer Science". Surely talking about "codes" is not enough for classifying it as CS. What makes a paper "a CS paper" imho is the following:  Did it appeared in some CS conference/journal, or was it used to prove some result in CS conference/journal? by CS paper i'm quite flexible but topics might be "information theory, complexity, program/system logics, recursion theory" etc.  Anyway can you cite the source of the example and/or  papers which make use of "there exists a scale of codes"? Thanks! Bye  
> **username_4**: Papers about codes of the integers appear in electrical engineering journals, such as the IEEE transactions on information theory. That hits one of your keywords.  
> **username_4**: I don't think there's any paper using these results. Moreover, I strongly believe that a result independent of ZFC has no use in complexity, so in a sense your question is about stretching the limits of what's considered computer science.  
> **username_0**: Hello Yuval, first of all let me thank you again for the answers.  I don't agree with your strong position however. For example the username_9ertson-Seymour theorem (which seems to require choice) has important consequences in complexity. So it is clear the Choice is useful (perhaps a bit surprisingly) in Complexity theory.   Now working with consistent extensions of ZFC obviously simplify the task of proving, complexity say, results, even if these results are maybe  provable in ZFC but nobody know how, yet.  
> **username_0**: Furthermore I don't see why there shouldn't be concrete results in complexity independent of ZFC, in the same way the username_9ertson-Seymour  theorem is (perhaps) independent of ZF.  
> **username_4**: I agree that AC may be used implicitly, but if you ask a random complexity theorist whether her latest proof uses AC, I'm not sure you'll get any meaningful answer. The moral is that AC is taken for granted, and as for other axioms, it's hard to imagine a natural situation where they'd be relevant.  
> **username_5**: @Yuval, Harvey Friedman may disagree with you. :)  
> **username_6**: @MatteoMio username_9ertson-Seymour theorem doesn't need AC, read this: http://cstheory.blogoverflow.com/2011/09/what-does-it-really-mean-to-prove-the-graph-minor-theorem/  

---

### Answer by username_7 on 2012-03-14. Score: 10

A *cone* of Turing degrees is a set $D$ of degrees with some base $b \in D$ such that for all degrees $c$, $b \leq\_T c$ if and only if $c \in D$.

The statement of *Turing degree determinacy*:

> Every set of Turing degrees either contains a cone or is disjoint from some cone

is a consequence of the axiom of determinacy (AD), which is independent of ZF and incompatible with ZFC. The weaker statement

> Every Borel set of reals that is closed under Turing equivalence either contains a cone or is disjoint from a cone

is a consequence of Martin's theorem on Borel determinacy, which is provable in ZFC. Both of these statements were studied before Martin's result on Borel determinacy was proved, at which time it was only known that they are both provable in ZF+AD.

The second quoted result has the following interesting conclusion: suppose that $S$ is a Borel set of reals closed under Turing equivalence such that for every real $b$ there is some $c \in S$ with $b \leq\_T c$ (this just says that $S$ is upwards dense in the Turing degrees). Then $S$ must contain an entire cone of Turing degrees.


---

### Answer by username_8 on 2012-03-15. Score: 6

I recently attended a talk with one such result, for the determinacy of one-counter Büchi games: Olivier Finkel, *The Determinacy of Context-Free Games*, STACS 2012, <http://drops.dagstuhl.de/opus/volltexte/2012/3389/pdf/5.pdf>.


---

### Answer by username_9 on 2011-04-08. Score: 1

A lot of constructive mathematics. See Per Martin-Löf's work on constructive set theory, used as a basis for dependently-typed programming languages.

> **Comments:**
> **username_10**: IIRC, Martin-Lof type theory has the same consistency strength as Kripke-Platek set theory, which is vastly weaker than ZFC. Also, MLTT doesn't have any explicitly anti-classical principles, like the continuity axioms Andrej mentioned.  
> **username_9**: @Neel I never said anything about consistency or strength of MLTT. However, I consider some results in constructive mathematics to be relevant to the question, asking for "interesting result in CS which is ... independent of ZFC".  
> **username_1**: I assume "independent" here is meant in the formal sense.  

---

