If I can prove $Y$ from "$X$ is true" and from "$X$ is false", can I prove $Y$ without using $X$ at all?

Question

Suppose I have a statement $X$, for which I do not know whether it is true or false. And suppose further that I want to prove a statement $Y$:

• I first assume that $X$ is true, and I construct an involved argument that shows that $Y$ follows.
• I then assume that $X$ is false, and another involved argument shows that $Y$ still follows.

I have then proven $Y$ (assuming excluded middle). Now, is there any kind of meta-theorem in mathematics that tells me that there should be a proof of $Y$ that is not mentioning $X$ at all (whatever that means formally)?

You can think about this as follows:

Was it necessary to have formulated $X$ in order to give a proof for $Y$, or could we have proven $Y$ right away without the "halt in between"?

For example, the Riemann hypothesis seems to be such an important "halt in the middle" for some statements.

I know, this is a rather informal question. I do not want to formulate it in terms of mathematical logic and proof theory, simply beacuse I do not know enough about these subjects. Maybe the question has a trivial counterexample if we go formal enough. But then again, maybe someone with enough knowledge still sees an interesting variant of the question. I am also happy to receive quite technical answers.

Answer 1

Proposition: The set $c\mathbb R = \{cx : x\in\mathbb R\}$ is closed.

You can prove this if you assume $c=0,$ and also if you assume $c\ne0.$ But I will be surprised if you can do it without considering those two cases.

Answer 2

It is hard to say about what does a proof "contains" in here, indeed if $T∪\{a\}⊢x$ and $T∪\{¬a\}⊢x$ then $T⊢x$ because in any model of $T$ either $a$ or $¬a$ are true, hence $T⊨x⇒T⊢x$, but how do you define "not mentioning"?

One interpretation you can think of is if $a$ is not in the language of $T$, that is:

Given a theory $T$ in the language $\cal{L}$, and given a language $\cal{L}'\supset\cal{L}$, is it possible to have a formula $a$ in the language of $\cal{L}'$ such that $T∪\{a\}⊢_{\cal{L}'}x$ and $T∪\{¬a\}⊢_{\cal{L}'}x$ and $T⊢_{\cal{L}}x$ is false?

***In this interpretation the answer is false:

Let $\cal{L}$ be empty and $\{f,g\}=\cal{L}'$ be 1-ary functional symbols, and let $a$ be the following theory:

$$(f\text{ is injective}∧f\text{ is not surjective})∧(g\text{ is injective}∧g\text{ is surjective})$$ And let $x$ be: $$∃z,y\ (z≠y)$$

Notice that $a$ does prove $x$, as well as $¬a$ proves $x$, but $x$ is not tautology.***

***As Noah said, this example is wrong, $¬a$ does not prove $x$.

Although the above answer is wrong, I leave this post up and not deleting it because it is yet another possible interpretation of the question.

Answer 3

Lets give a minimal formalization in Gentzen style proof systems: Assume $X \Rightarrow Y$ and $\neg X \Rightarrow Y$. From these two we can deduce $X \lor \neg X \Rightarrow Y$ (1). On the other hand, in classical mathematics, we have $\Rightarrow X \lor \neg X$ (2). You proved your statement by using a cut rule on (1) and (2). Gerhard Gentzen's main result was cut elimination theorem for his system. So your question can be reformulated in this formalism as "Is cut rule always eliminable?" For some logics and theories it is proved. But generally speaking, it is not answered and "hardly seems possible".