Proof: $X$ exists, or there exists a proof that $X$ does not exist

Question

"I went on the internet today", as it were, and happened upon a devious proof for the claim that either a thing $X$ exists, or there exists a proof that $X$ does not exist.

The proof, if I understood its author correctly, is as follows:

Define proof to mean a valid argument with all true premises. Let $P_1$ be the proposition that $X$ exists. Then

1. Either $X$ exists, or $X$ does not exist: $P_1 \vee \neg P_1$ is true by assumption. If $X$ exists, then our claim is satisfied and we may stop here; otherwise:

2. Let us assume that there does not exist a proof that $X$ does not exist.

3. Disjunctive syllogism, $((P \vee Q) \wedge \neg P) \rightarrow Q $, is a valid argument, with premises $P \vee Q$ and $\neg P$.

4. $((P_1 \vee \neg P_1) \wedge \neg P_1) \rightarrow \neg P_1 $ is a disjunctive syllogism, thus a valid argument, with premises $P_1 \vee \neg P_1$ and $\neg P_1$.

5. If $((P_1 \vee \neg P_1) \wedge \neg P_1) \rightarrow \neg P_1 $ has all true premises, it is a proof (since it is a valid argument). But this violates our assumption in step 2, so at least one of the premises $P_1 \vee \neg P_1$ and $\neg P_1$ must be false.

6. $P_1 \vee \neg P_1$ is true by assumption, so of the two premises only $\neg P_1$ can be false.

7. Therefore, $\neg P_1$ is false, thus $P_1$ is true: if there is no proof that $X$ does not exist, then $X$ has been shown to exist!

...now this feels extremely wrong, but I simply cannot tell why. I'm almost certain that there is an error at least in step 5, but I cannot see it. I can't even tell if the proof contains a logical error or if it has employed some form of verbal trickery. The proof seems correct, yet feels wrong.

What error(s), if any, have been made in the above proof? Is the original claim correct even if the proof itself fails?

Answer 1

This "proof" is conflating modalities.

The $((P_1 \lor \lnot P_1) \land \lnot P_1) \to \lnot P_1$ part can be simplified to just saying $\lnot P_1 \to \lnot P_1$ while retaining the same fallacy. You can also get rid of all the negations while retaining the same fallacy, e.g., let $Q = \lnot P_1$. And the subscript 1 is just pointlessly annoying.

Here is a cleaned up version of what the author is trying to put up:

1. To establish contradiction, assume some arbitrary $Q$ and that there is no proof of $Q$.
2. Well $Q \implies Q$, and since we assumed $Q$, this is a valid proof of $Q$.
3. But that is a contradiction with the assumption no proof exists.

Obviously the flaw is that $X \implies Y$ is only a valid proof of $Y$ if there is already a valid proof of $X$ established.