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$ ?

7Many theorems in analytic number theory (e.g. the SiegelWalfisz 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$?) – Terry Tao Nov 19 '16 at 16:53

2When 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. – Goldstern Nov 19 '16 at 18:38

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? – Goldstern Nov 19 '16 at 21:02

3@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. – Joel David Hamkins Nov 19 '16 at 21:59
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.)
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 wellordered 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).
Another example is: Mycielski proved in 1964 under ZF that there is some $A \subseteq \omega_1^{\omega}$ such that the twoplayer 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.

3One can avoid the case division with a uniform definition of a nondetermined game, as in theorem 5 of my paper: jdh.hamkins.org/opendeterminacyforclassgames. – Joel David Hamkins Nov 19 '16 at 20:05

Interesting! This was essentially stated as an open problem in Kanamori. – Douglas Ulrich Nov 19 '16 at 20:09

3Except, that seems to produce a nondetermined game on $\mathcal{P}(\mathbb{R})$ rather than $\omega_1$? – Douglas Ulrich Nov 19 '16 at 20:26

Yes, our game is on $P(\mathbb{R})$. I wonder if a similar idea would apply to answer Kanamori's question? – Joel David Hamkins Nov 19 '16 at 20:39

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.) – Douglas Ulrich Nov 28 '16 at 4:45
In this 1978 paper, Shelah and M. Rudin have proven that for each cardinal $\kappa$, there exists $2^{2^{\kappa}}$ many RudinKeisler 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.
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
$T:= CH \vee \lnot CH$.
Or, let $S$ be your favorite theorem, and consider $T:= S\wedge (CH\vee \lnot CH)$.

12

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. – Erfan Khaniki Nov 20 '16 at 15:30

@BjørnKjosHanssen 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".) – Goldstern Nov 22 '16 at 21:51

@ErfanKhaniki My claim is empirical, not mathematical. I claim that (as the poster demands) there is no known proof of "CH or nonCH" 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). – Goldstern Nov 22 '16 at 22:01

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.

6It 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.) – LSpice Nov 19 '16 at 23:48

1

2This 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$. – Carl Mummert Nov 20 '16 at 4:42