40

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

Kaveh
  • 21,577
  • 8
  • 82
  • 183
OldFella
  • 501
  • 3
  • 4
  • 9
    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 Apr 07 '11 at 18:07
  • 9
    I was going to answer that Matteo Mio and Alex Simpson used Martin's Axiom to prove very interesting results... – Andrej Bauer Apr 08 '11 at 09:04
  • 7
    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 Apr 08 '11 at 13:11

5 Answers5

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).

Andrej Bauer
  • 28,823
  • 1
  • 80
  • 133
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).
Yuval Filmus
  • 14,445
  • 1
  • 48
  • 92
  • 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 Apr 10 '11 at 09:32
  • 1
    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 Apr 10 '11 at 15:36
  • 1
    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 Apr 10 '11 at 15:38
  • 1
    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 Apr 10 '11 at 20:16
  • 1
    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 Apr 10 '11 at 20:17
  • 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 Apr 11 '11 at 02:42
  • @Yuval, Harvey Friedman may disagree with you. :) – Kaveh Apr 13 '11 at 12:04
  • @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 Mar 15 '12 at 05:30
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.

Carl Mummert
  • 305
  • 2
  • 6
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.

Sylvain
  • 3,374
  • 26
  • 22
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.

Rob
  • 815
  • 8
  • 19
  • 6
    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 Apr 08 '11 at 09:39
  • @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 Apr 09 '11 at 07:39
  • 5
    I assume "independent" here is meant in the formal sense. – Mark Reitblatt Apr 09 '11 at 23:52