40
$\begingroup$

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

Improve this question
$\endgroup$
3

5 Answers 5

Reset to default
20
$\begingroup$

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

Improve this answer
$\endgroup$
1
  • $\begingroup$ Thank you! I'll ask alex more details about this when I'll be writing the introduction. $\endgroup$
    – OldFella
    Commented Apr 8, 2011 at 11:20
13
$\begingroup$

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).
Improve this answer
$\endgroup$
8
  • $\begingroup$ 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 $\endgroup$
    – OldFella
    Commented Apr 10, 2011 at 9:32
  • 1
    $\begingroup$ 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. $\endgroup$
    – Yuval Filmus
    Commented Apr 10, 2011 at 15:36
  • 1
    $\begingroup$ 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. $\endgroup$
    – Yuval Filmus
    Commented Apr 10, 2011 at 15:38
  • 1
    $\begingroup$ 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. $\endgroup$
    – OldFella
    Commented Apr 10, 2011 at 20:16
  • 1
    $\begingroup$ 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. $\endgroup$
    – OldFella
    Commented Apr 10, 2011 at 20:17
10
$\begingroup$

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.

Improve this answer
$\endgroup$
6
$\begingroup$

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.

Improve this answer
$\endgroup$
1
$\begingroup$

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.

Improve this answer
$\endgroup$
3
  • 6
    $\begingroup$ 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. $\endgroup$
    – Neel Krishnaswami
    Commented Apr 8, 2011 at 9:39
  • $\begingroup$ @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". $\endgroup$
    – Rob
    Commented Apr 9, 2011 at 7:39
  • 5
    $\begingroup$ I assume "independent" here is meant in the formal sense. $\endgroup$
    – Mark Reitblatt
    Commented Apr 9, 2011 at 23:52

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.