Prove that a construction exists: is this a constructive proof or existential proof?
This top answer claims that it is possible to prove that a constructive proof cannot exist.
I think, if "non-existence of constructive proof" can be proven, then for some other questions, it is also possible to prove "the existence of constructive proof".
Consider the following statement: "existence of constructive proof without actually giving the construction algorithm."
I am very curious if this statement is considered a "constructive proof" or "existential proof".
You have a formal system equipped with some notion of "constructive proof" (note that "constructive proof" is nigh-impossible to pin down with any kind of generality - there are only a few standard proof systems such as Peano Arithmetic where the distinction between constructive and non-constructive proofs is more-or-less agreed upon and understood, or systems such as Heyting Arithmetic or Martin-Löf Type Theory which only admit constructive proofs by design).
You start with a sentence (formula, proposition-as-type, etc.) $\psi$ of your chosen formal system, and consider a sentence (formula, etc.) $\varphi$ which denotes something like "$\psi$ has a constructive proof (in the formal system under consideration)". Then you ask:
Would a non-constructive proof of $\varphi$ be considered a constructive or non-constructive proof of $\psi$?
By offering two alternatives, you unintentionally turned this into trick question! The short and correct answer is that a proof of $\varphi$ is not considered a proof of $\psi$ at all.
First, the easy formalities. Each formal proof has a conclusion, the sentence (formula, etc.) $\varphi$ that the proof actually establishes. This conclusion is unique: formally, a proof of $\varphi$ is a proof of $\varphi$, and not a proof of anything else. In particular, it's never a proof of some other formula, say $\psi$.
At this point, you might think that you can get around these formal issues by rephrasing your question slightly, via some tricky phrasing such as "can a proof of $\varphi$ always be turned into a proof of $\psi$ algorithmically..."
But Gödelian obstacles prevent you from doing that. The statements $\varphi$ and $\psi$ are not related in a sufficiently strong way. For example, $PA+\neg Con(PA)$ proves $\varphi$ (no matter what $\psi$ is), but (unless PA is inconsistent) it does not prove an arbitrarily chosen formula $\psi$, say $0 = 1$. Basically, a sufficiently strong formal system won't go from a proof of "there exists a proof of $\psi$" to a genuine proof of $\psi$ unless it believes itself consistent: but then, by the second incompleteness theorem the formal system was gravely mistaken about its own consistency anyway.
This answers your question: a non-constructive proof of "$\psi$ has a constructive proof" would not be considered a proof of $\psi$ at all, much less a constructive proof of $\psi$.
For further reading, assuming you already have a firm grasp of Gödel's theorems including Rosser's variant, you might want to read up on arithmetical soundness (if you can track down the first email of this FOM list discussion, it might be a good starting point; or see e.g. Boolos' The Logic of Provability), and the reflection theorem showing that PA is not finitely axiomatizable.
It's constructive. Proofs are finite objects. If you know that a proof of $P$ exists, then you can find one, using the following method:
- Generate every possible proof, starting with the shortest and working up by length
- When you find a proof of $P$, stop
Note that this method only works if you already know that $P$ is provable.