18
$\begingroup$

So, one of the things that mathematical logic does is study theorems as abstract objects. There also many theorems about mathematical logic, and these theorems can have connections to other fields.

Additionally, mathematical logic also proven that certain conjectures are not formally decidable within certain formal systems. This means that mathematicians need stronger formal systems to prove them.

However, has a mathematical theorem ever been proven by constructing the proof with mathematical logic? Or proving that a proof exists?

By this, I mean for statement $C$ which is a mathematical conjecture, instead of writing out a proof of $C$, they write either a constructive or nonconstructive proof that proof exists.

For example:

  • Use proof theory to prove there are a sequence of inferences to lead to $C$ (this is implied by the previous two bullets, of course)
  • Use model theory to prove that all models of some theory $T$, where $T$ is a theory that mathematicians typically use for proofs, satisfy $C$
  • Use computer science to construct a program $P$, such that the Curry–Howard correspondence applied to $P$ results in a proof of $C$

What I am not looking for is examples where someone writes a proof of $C$, citing theorems from mathematical logic. In this case, they have actually written down a proof, not simply proved it exists. Like, that is still super cool, and has huge implications for the rest of mathematics, but I am asking about something different.

EDIT: If the conjecture uses a lemma $L$ that satisfies the above, that's fine. However, it must directly use the statement the lemma is stating, not the fact that is has abstractly been proven. That is, the proof of $C$ involves showing that $L$ implies $C$, not that the existence of a proof of $L$ implies $C$.


This is one technical caveat. T can not prove "$\forall C. Provable(C) \implies C$". Moreover, if it does for some $C$, it is vacuously true even within $T$, since one can technically just write a direct proof of $C$ in $T$. However, if $T$ is sound, then Provable(C) does in fact imply C. Since mathematicians usually implicitly assume that the theories they work in are sound (unless they are working in the theory for its meta-mathematical significance instead of its soundness), this should be acceptable. Moreover, proving a proof exists might be more tractable than writing the proof is some instances.

$\endgroup$
  • 3
    $\begingroup$ Not exactly what you are after, but Herbrand's theorem has been used quite successfully to extract explicit bounds from theorems in several areas of analysis whose proofs only establish the existence of bounds, typically via nonconstructive (or nonexplicit) means. $\endgroup$ – Andrés E. Caicedo Feb 12 at 20:21
  • $\begingroup$ @PyRulez For more on such uses of Herbrand's theorem and related tools, you want to search for "proof mining". $\endgroup$ – Andrés E. Caicedo Feb 12 at 20:28
  • $\begingroup$ Here is a concrete obstacle to what you are after literally, if not in spirit. $\endgroup$ – Andrés E. Caicedo Feb 12 at 21:34
  • $\begingroup$ @PyRulez I do not know that Goodstein's theorem is "almost equivalent" to PA. It is an independent sentence at the next level of complexity, and the extra layer of complexity has explicit consequences. For instance, Goodtein's theorem is still unprovable after adding to PA all true $\Pi^0_1$ statements. $\endgroup$ – Andrés E. Caicedo Feb 12 at 21:36
  • $\begingroup$ @AndrésE.Caicedo I added an edit addressing the issue. I actually was just realizing the problem when you posted that comment. $\endgroup$ – PyRulez Feb 12 at 21:43
14
$\begingroup$

I do not know about a conjecture, but I would like to mention the Ax–Grothendieck_theorem.

A very nice way of proof is to show that the (first-order) theory $ACF_0$ of algebraically closed fields with characteristic zero is complete (through quantifier elimination iirc).

Thus, if the statement is false, there is a “somewhat” equivalent (because of the number of variables and degree of polynomials) first-order statement the negation of which can be proved in $ACF_0$.

Since the proof has finite length, there exists some prime $p$ such that the assumption “$p \neq 0$” is not used in the proof. So that first-order statement never holds in any algebraically closed field with characteristic $p$.

It remains to prove that the Ax-Grothendieck theorem holds in the algebraic closure of $\mathbb{F}_p$ for each prime $p$.

In a nutshell, we actually disprove the existence of a general disproof in $ACF_0$ ; since $ACF_0$ is complete, this entails the existence of a proof.

$\endgroup$
  • $\begingroup$ Yes, that definitely works! I think you can technically translate it to a proof not using mathematical logic, but that's just a consequence of Löb's theorem. $\endgroup$ – PyRulez Feb 12 at 22:02
  • 2
    $\begingroup$ If you've proven something by proving that a lower-order proof exists then you will always be able to find a lower-order proof, because after all one was proven to exist. $\endgroup$ – Display Name Feb 12 at 22:29
  • 1
    $\begingroup$ @DisplayName Oh whoops, I meant a "simple-ish" proof. As long as the meta-theory is ω-consistent, then yes, the direct proof will exist. $\endgroup$ – PyRulez Feb 12 at 22:34
  • 2
    $\begingroup$ @DisplayName: That's not quite true. You need the system you're working in to be Σ1-sound before you can conclude that if you prove the existence of a proof it really implies the existence of a proof. For all we know, strong extensions of ZFC might be consistent but Σ1-unsound, in which case ZFC may prove the existence of a proof over ZFC but actually there is none. So far though, most theorems do not use anything near the full strength of ZFC, so it is not hard to convert a proof of provability to an actual proof. $\endgroup$ – user21820 Feb 13 at 9:43
  • 2
    $\begingroup$ @PyRulez: As per my above comment, you only need Σ1-soundness (which is implied by either ω-consistency or arithmetical-soundness). You may also be interested in this post. $\endgroup$ – user21820 Feb 13 at 9:47
10
$\begingroup$

The original proof of the Halpern-Läuchli theorem seems to be the sort of thing you asked for. In their paper, Halpern and Läuchli first set up a formal deductive system and show that a certain formula is deducible in this system. Then they provide a semantics, i.e., meanings for the formulas of their system. They show that the system is sound, i.e., the meanings of deducible formulas are true. And finally, they note that the particular formula whose deducibility they established earlier has, as its meaning, the conclusion that they want to prove.

The MathSciNet citation for the paper is

MR0200172 (34 #71)

Halpern, J. D.; Läuchli, H.

A partition theorem.

Trans. Amer. Math. Soc. 124 1966 360–367.

$\endgroup$
  • $\begingroup$ I'd never actually looked at the original paper before - that's fascinating! $\endgroup$ – Noah Schweber Feb 13 at 3:02

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.