16
$\begingroup$

Is there a known theorem $T$ in $ZF+DC$ (or $ZF$ or $ZFC$) such that the only proof we know of $T$ is by using the LEM applied to $A$ ( "$A$ or not $A$" ), where $A$ is independent of $ZF+DC$ ?

$\endgroup$
4
  • 7
    $\begingroup$ Many theorems in analytic number theory (e.g. the Siegel-Walfisz theorem en.wikipedia.org/wiki/Siegel%E2%80%93Walfisz_theorem) are ineffective because they apply the law of excluded middle to a statement $A$ (e.g. the existence of a Siegel zero en.wikipedia.org/wiki/Siegel_zero) which is not known to be decidable. But this statement is generally believed to be false (and decidably so), so this probably isn't an example to your claim. (Presumably the continuum hypothesis would be an obvious candidate for your $A$?) $\endgroup$
    – Terry Tao
    Nov 19, 2016 at 16:53
  • 2
    $\begingroup$ When you use a logic that does not prove $A\vee \lnot A$, it is not immediately clear (to me, at least) what you mean by ZFC. I can think of several versions which are equivalent in classical logic, but not obviously equivalent with the excluded middle. $\endgroup$
    – Goldstern
    Nov 19, 2016 at 18:38
  • $\begingroup$ Are you asking for proofs of $T$ where both $A\to T$ and $\lnot A\to T$ avoid using the excluded middle? Say, using intuitionistic logic? $\endgroup$
    – Goldstern
    Nov 19, 2016 at 21:02
  • 5
    $\begingroup$ @Goldstern I find it reasonable to interpret the question as concerned not with proofs in intuitionistic logic, but rather with classical logic proofs that happen to branch on a case distinction, which is itself an independent statement. $\endgroup$ Nov 19, 2016 at 21:59

6 Answers 6

27
$\begingroup$

Here is an example:

It is provable from $\sf ZF$ that there exists four infinite cardinals, $\frak p,q,r,s$ with $\frak p<q, r<s$ such that $\frak p^r=q^s$. (Here cardinals do not mean just finite ordinals and $\aleph$ numbers.)

You can find the proof here.

The proof using the axiom of choice is easy, and the proof not using the axiom of choice begins by using the fact that there is a set which cannot be well-ordered in order to construct the example.

Of course, the axiom of choice is indepedendent of $\sf ZF$. I also don't know an explicit proof of this theorem (in fact, before seeing this in a a math.SE question, I don't know if someone had proven this outside of a $\sf ZFC$ context either).

$\endgroup$
2
  • $\begingroup$ The link is broken...Can you provide a new one? $\endgroup$ Mar 11, 2019 at 15:12
  • $\begingroup$ Yes, sorry. I've fixed that. $\endgroup$
    – Asaf Karagila
    Mar 11, 2019 at 16:01
16
$\begingroup$

Another example is: Mycielski proved in 1964 under ZF that there is some $A \subseteq \omega_1^{\omega}$ such that the two-player game with payoff set in $A$ is not determined. The proof uses that either the axiom of determinacy fails, in which case this is easy, or else the axiom of determinacy holds, in which case there is no injection from $\omega_1$ into $\mathbb{R}$.

See exercise 27.12 in Kanamori "The Higher Infinite" for a short proof.

$\endgroup$
7
  • 3
    $\begingroup$ One can avoid the case division with a uniform definition of a nondetermined game, as in theorem 5 of my paper: jdh.hamkins.org/open-determinacy-for-class-games. $\endgroup$ Nov 19, 2016 at 20:05
  • $\begingroup$ Interesting! This was essentially stated as an open problem in Kanamori. $\endgroup$ Nov 19, 2016 at 20:09
  • 3
    $\begingroup$ Except, that seems to produce a nondetermined game on $\mathcal{P}(\mathbb{R})$ rather than $\omega_1$? $\endgroup$ Nov 19, 2016 at 20:26
  • $\begingroup$ Yes, our game is on $P(\mathbb{R})$. I wonder if a similar idea would apply to answer Kanamori's question? $\endgroup$ Nov 19, 2016 at 20:39
  • $\begingroup$ It occurs to me that if $M$ is an inner model of $\mathbb{V}$, $\mathbb{V} \models ZFC$, $M \models ZF+AD_{\mathbb{R}}$, and $M^\omega \subseteq M$ (is this possible?), then any $A \subseteq \omega_1^\omega$ with $A \in M$ is determined in $\mathbb{V}$: In $\mathbb{V}$, $A$ is equivalent to a certain game $A' \subseteq \mathbb{R}^\omega$ (just play codes for ordinals). $A'$ is determined in $M$, hence since $M^\omega \subseteq M$, it is determined in $\mathbb{V}$. So this is a partial negative answer to Kanamori's question (asssuming the setup I described is possible.) $\endgroup$ Nov 28, 2016 at 4:45
12
$\begingroup$

In this 1978 paper, Shelah and M. Rudin have proven that for each cardinal $\kappa$, there exists $2^{2^{\kappa}}$ many Rudin-Keisler incompatible ultrafilters on $\kappa$.

In the case that $2^{2^{\kappa}}>(2^{\kappa})^{+}$, the result follows from the free set lemma. The case where $2^{2^{\kappa}}=(2^{\kappa})^{+}$ has been proven separately by Shelah.

$\endgroup$
11
$\begingroup$

This 1991 paper in the Proceedings of the AMS presents the following result of Shelah: there exists a regular topological space of size $>\aleph_2$ in which there are no closed sets of size $\aleph_2$.

If $2^{2^{\aleph_0}}>\aleph_2$, then $\beta\omega$ will serve; otherwise $\diamondsuit_{\{\alpha<\omega_2:cf(\alpha)=\aleph_0\}}$ holds, and this can be used to construct a suitable topology on $\aleph_2^{\aleph_2}$.

Math Reviews: MR1052572

$\endgroup$
1
  • $\begingroup$ That's lovely! +1. $\endgroup$ Nov 19, 2016 at 22:36
4
$\begingroup$

$T:= CH \vee \lnot CH$.

Or, let $S$ be your favorite theorem, and consider $T:= S\wedge (CH\vee \lnot CH)$.

$\endgroup$
5
  • 13
    $\begingroup$ (What a stupid answer...) $\endgroup$
    – Goldstern
    Nov 19, 2016 at 18:39
  • $\begingroup$ For example why ${\bf IZF}+\{\phi \lor \neg \phi| {\bf IZF}\nvdash \phi \leftrightarrow CH\}\nvdash CH \lor \neg CH$? At least you should prove this claim to consider your post as an answer. $\endgroup$ Nov 20, 2016 at 15:30
  • $\begingroup$ @BjørnKjos-Hanssen I don't understand what you mean by $\forall p(p\vee \lnot p)$. First: In the language of ZFC, variables range over sets, not over statements. Second: $p\vee \lnot p$, where $p$ is a sentence, is for me an instance of the "Law of the excluded middle", which is not permitted in this context. (That is my understanding of the question, morally. I do not know what the question means "technically".) $\endgroup$
    – Goldstern
    Nov 22, 2016 at 21:51
  • $\begingroup$ @ErfanKhaniki My claim is empirical, not mathematical. I claim that (as the poster demands) there is no known proof of "CH or non-CH" from ZFC which does not use the excluded middle. If you show me such a proof, I will retract my claim. (Or rather, edit my answer and point out that it is wrong, to help others learn from my mistake.) - It is my understanding that ZFC can be replaced by slightly different axiom systems, but only systems that are sufficiently natural (and at least decidable). $\endgroup$
    – Goldstern
    Nov 22, 2016 at 22:01
  • $\begingroup$ Ok, that makes sense. $\endgroup$ Nov 23, 2016 at 20:13
2
$\begingroup$

When I was in grad school I learned about the following fact which was actually intended as a joke.

Theorem: There are irrational numbers $x$ and $y$ such that $x^y$ is rational.
Proof. Look at $\sqrt2^{\sqrt2}$. Is it rational? If so, take $x=y=\sqrt2$, and we are done. Otherwise, take $x=\sqrt2^{\sqrt2}$ and $y={\sqrt2}$, and we are again done since $$x^y = \left(\sqrt2^{\sqrt2}\right)^{\sqrt2} = \sqrt2^{\left(\sqrt2\times\sqrt2\right)} = \sqrt2^2 = 2.$$ QED

I have no idea if the rationality of $\sqrt2^{\sqrt2}$ is decidable or not (most likely it is), so this is not quite an answer.

$\endgroup$
3
  • 7
    $\begingroup$ It is (decideable), and it isn't (rational): en.wikipedia.org/wiki/Gelfond%E2%80%93Schneider_theorem . (Quite possibly it was this classical example that prompted the original question.) $\endgroup$
    – LSpice
    Nov 19, 2016 at 23:48
  • 1
    $\begingroup$ @Spice, thanks very much. It is always good to learn something new! $\endgroup$
    – Ruy
    Nov 20, 2016 at 0:25
  • 5
    $\begingroup$ This can be used to make similar examples, though. Let $A$ be a statement independent of some classical theory like ZFC, and define $x$ to be $2$ if $A$ holds and $3$ otherwise. Then the theory proves "$x$ is rational", but apparently only by an excluded middle argument that branches on $A$. $\endgroup$ Nov 20, 2016 at 4:42

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.