Is it valid/useful to prove statement $X$ by finding $Y$ such that $Y\to X$ and $\lnot Y\to X$?

Question

Background: Suppose I want to prove theorem X. Typically, I'd have to use a set of axioms $A = \{A_1,A_2, \ldots ,A_n\}$ or previously proved theorems $T=\{T_1,T_2, \ldots,T_n\}$ and consider all of those as True. Then, I 'd typically prove that $A \rightarrow X$ or $T \rightarrow X$.

Question: I am wondering whether the idea I am about to describe is a valid or useful approach to doing mathematics. The idea is about proving something without needing any axioms or previous theorems, the only exception being the Axiom of Excluded Middle. With this approach, If I want to prove $X$ I do the following.

1. Find the right statement Y
2. Prove $Y \rightarrow X$
3. Also prove $¬Y \rightarrow X$
4. $(Y \rightarrow X) \land (¬Y \rightarrow X)$ is the same as $(Y \lor¬Y) \rightarrow X$
5. $(Y \lor¬Y)$ is true due to the Axiom of Excluded Middle.
6. Because $(True \rightarrow X)$ then $X$ must be also $True$

In plain words, if you prove that a statement X is true regardless of whether another statement Y is true or false, then X must be true.

While I suspect that the approach is valid, step 1. might be difficult or impossible in practice to make this a useful approach, but I 'd love to hear if anyone has seen something similar before.

Answer 1

Yes, this works and is useful. I would vote to close this as a duplicate, except it's a duplicate of a question from MathOverflow.

Answer 2

You can get convincing examples for this sort of idea, and indeed I'd free the principle from negations (here appearing in the excluded middle).

Common logic example:

"My friend told me she was born in Korea. I don't know if she means North Korea or South Korea. Both North and South Korea are less than ten thousand kilometers from Japan. So either way, my friend was born less than ten thousand kilometers from Japan."

We derive new knowledge about the friend (her birthplace is close to Japan, $J$) from a collection of possibilities where one of which is necessary true (she was either born in North Korea, $N$, or she was born in South Korea $S$), while we remaining in the dark about which of those possibilities is actually true.

Formally, the main principle at work is thus

$$\left((N\lor S)\,\,\land\,\,((N\to J)\land (S\to J))\right)\,\,\to\,\,J$$

where of course you can read the three letters as generic propositions.

The core equivalence to easier see this holds is

$$(N\to J)\land (S\to J)\iff(N\lor S)\to J$$

which express two ways of saying that both of two proposition lead us to a certain conclusion. This equivalence is one of the nicer ones connecting $\land$ and $\lor$, as it still holds in logics without excluded middle or explosion. It's particularly constructive.

With this our main principle reads

$$\left((N\lor S)\,\,\land\,\,((N\lor S)\to J)\right)\,\,\to\,\,J$$

Abbreviate $N\lor S$ by $K$, then this is just a case of modus ponens as a theorem:

$$\left(K\land(K\to J)\right)\to J$$

Again, the interesting aspect of this is that we can work with a validated $K$ that is actually in the form a disjunction, $\lor$, on this level where we don't actually need to know in which way that disjunction holds.

This idea is also not limited to exactly two propositions.

---

The disjunction $N\lor S$ in my example happened to be that statement about where my friend is born, taken to be true by her telling us this. Your initial question is a disjunction of the more particular form $Y\lor \neg Y$ (excluded middle for $Y$), which we may derive or adopt in general.

Answer 3

It happens quite often, and in situations where it is not a clever trick but required.

Let’s say you want to prove that f(x) has some property, and first you prove that it has the property for small x because of reason A, and then you prove it has the property for large x for some completely different reason B.