Are there any good nonconstructive "existential metatheorems"?

Question

Are there any good examples of theorems in reasonably expressive theories (like Peano arithmetic) for which it is substantially easier to prove (in a metatheory) that a proof exists than it is actually to find the proof? When I say "substantially easier," the tediousness of formalizing an informal proof should not be considered. In other words, a rigorous but informal proof doesn't count as a nonconstructive demonstration that a formal proof exists, since there is no essential difficulty in producing a formal proof besides workload. If there is some essential barrier, then there's something wrong either with the proof or with the definition of "formal proof." (Although the concept of "informal proof" is by nature vague, it seems reasonable to say that the procedure transforming a typical informal proof to a formal proof is a primitive recursive computation, even though it's probably impossible to make that precise enough to prove.)

I don't know what such a nonconstructive meta-proof could look like, but I also don't see why one couldn't exist. The only near-example I can think of right now is in the propositional calculus: you can prove that a propositional formula is a theorem by checking its truth table, which does not explicitly provide a deduction from the axioms; however, in most interesting cases, that probably isn't much easier (if at all) than exhibiting a proof, just maybe more mechanical. (Of course, estimating the difficulty of proving or disproving a candidate for a propositional theorem is a huge open problem.) Also, I think there is actually a simple way to convert a truth-table proof into an actual deduction from the axioms of propositional calculus, although I don't remember and didn't retrace all of the details. (Anyway, I'm not even so interested in the propositional calculus for this question, since it's not very expressive.)

Another thing that seems vaguely relevant is Godel's completeness theorem, which states that a formula is a theorem of a first-order theory if and only if it is true in every model of that theory. I don't know in what cases it would be easier, though, to show that some formula were true in every model than it would be just to prove the theorem in the theory.

Answer 1

Set theory provides a good example. It is often convenient in set theory to work with the concept of "classes" and treat them as mathematical objects of their own kind. The standard axiomatization of set theory with classes is called Goedel-Bernays set theory, denoted GBC, whereas the usual ZFC axioms have only set objects. But there is a general theorem that any statement purely about sets that is proved by using classes in GBC can be proved without them purely in ZFC. This is what it means to say that GBC is a conservative extension of ZFC. To prove this general theorem, it suffices to observe that any ZFC model can be expanded to a model of GBC, by adding only the classes definable from parameters.

There are many other examples of conservative extensions in mathematics, and all of them would seem to be examples of the type that you seek. For example, PA has a conservative extension to the analogous theory true in the collection HF of hereditarily finite sets. Thus, to prove a theorem about numbers in PA, one can freely use heredtiarily finite sets (e.g. sequences of numbers, sequences of sets of numbers, etc.), not just as coded by numbers via Goedel coding, but as actual mathematical objects. And surely this makes proofs much easier.

Perhaps another type of example arises in the absoluteness phenomenon in set theory. For example, the Shoenfield Absoluteness theorem states that any $\Sigma^1_2$ statement has the same truth value in any two models of set theory with the same ordinals. In particular, to prove that a particular $\Sigma^1_2$ statement is true in ZFC, it suffices to prove it under the assumption also that V=L, where one also has all kinds of additional structure available. The Absoluteness Theorems (and there are many) can therefore be viewed under the rubric you mention.

But of course, in all these cases, we have an actual proof in the weaker theory. To prove that there is a proof, is a proof, so I believe ultimately there will be no way to avoid the quibbling over whether it is easy or hard to translate the high-level proof into a low level proof, since in principle it will always be possible to do this.

Answer 2

Eh, this is more of an "existential meta-algorithm," but I think it's perhaps worth mentioning...

One consequence of the Robertson-Seymour graph minor theorem is that for any given surface, there's a polynomial-time algorithm (actually cubic time!) to decide if a graph can be drawn on that surface. But this algorithm isn't explicit -- since it relies on testing a finite but not effectively bounded number of graphs to see whether they're minors of the input graph. Actually, as far as I know we can't even describe this algorithm for checking if a graph is embeddable on a torus -- and computing the graph genus in general is known to be NP-complete! So we know that an "efficient" algorithm exists, although describing it is known (assuming P \neq NP) to be hard.

Answer 3

Harvey Friedman has an example of a finite statement (that's actually "finite" and not "finitary," i.e., $\Pi_0^0$ rather than $\Pi^0_1$) that has a proof, using large cardinal axioms, that is no more than a million symbols in length, but whose proof in ZFC with abbreviations must contain more than $10^{1000}$ symbols. Obviously, explicitly "finding" the ZFC proof is totally infeasible. See the last theorem (Theorem 5) in this post to the Foundations of Mathematics mailing list.

In some sense, computational infeasibility is the only kind of obstruction that can exist here. If there is a proof then you can find it by exhaustive search, so there cannot be a nonconstructive argument for the existence of a proof in the strong sense of an argument that gives you no algorithm whatsoever for finding the proof. Thus by some measure, Friedman's example is about the strongest kind of example you could hope for.

Answer 4

This is not quite what the original question is asking, but certainly in computer science there are plenty of problems which one can decide quickly by a probabilistic argument, but no deterministic algorithm is known (the P=BPP problem, basically). For instance, consider the task of deciding whether a polynomial identity in many variables over a fixed finite field is true. One can decide this to arbitrarily high probability quickly, just by testing random assignments of the variables and seeing if one ever gets a counterexample. (The Schwarz-Zippel lemma tells us that if the identity fails, then it fails a lot, and so will be picked up with high probability by random sampling.)

So if a polynomial identity is true, then one can fairly quickly be extremely convinced that it is true, but this gives no clue how to find a formal proof that the identity holds, short of evaluating every single choice of assignment, or expanding out the identity completely and comparing coefficients (which ends up being about the same amount of work (i.e. exponential in the dimension), actually).

Answer 5

This isn't a perfect answer to your question, but I believe that there are theorems that tell you that anything you prove in area Y using tool X (e.g., in number theory using complex analysis) can be proved without using tool X. And I think that these theorems don't tell you nice ways of eliminating X but just give some rather formal abstract argument that it can be done. I'm sure someone else will know what I am talking about and will be able to supply the details.

Answer 6

Gödel's second incompleteness theorem leads to a curious example as follows. The diagonalization method (as in the proof of the first incompleteness theorem) produces, for any reasonable theory T that contains arithmetic (e.g., PA or ZFC), a sentence S provably equivalent (in T) to "S is provable in T." (One often abbreviates such an S as "I am provable in T.")

Löb's theorem says that this S is in fact provable in T. (Proof: The theory T' obtained from T by adding "not S" proves, by our choice of S, "S is not provable in T," which is easily equivalent to the consistency of T'. By Gödel's second incompleteness theorem, T', having proved its own consistency, must be inconsistent. Thus, T proves S.)

I've never seen a direct argument for this, say in the case of PA or of ZFC.

Answer 7

A basic principle of first order logic is that, if a theorem follows from a list of axioms, then it follows from some finite subset of that list. This can often give nontrivial consequences. For example:

(1) If $T$ is any true first order statement about characteristic zero fields, then there is a constant $N$ so that $T$ is true for fields of characteristic $>N$.

Proof: take your list of axioms to be the standard field axioms plus, in case (1), the axiom $1+1+1+\cdots+1 \neq 0$ where the sum is over $p$ ones for each prime $p$.

A similar example is:

(2) If $T$ is any true first order statement about algebraically closed fields, there is a constant $N$ such that $T$ is true for any field $K$ in which every polynomial of degree $\leq N$ has a root.

In both of these cases, it can be easier to (informally) prove a result about characteristic zero/algebraically closed fields than it is to extract the constant $N$.

Here is a different example. Recall that Ramsey's theorem (in a special case) says:

(3) For any positive integer $N$, there is an integer $M$ such that, for any bicoloring of the complete graph on $M$ vertices, there is a monochromatic complete subgraph on $N$ vertices.

As I understand it, the original proof was to show

(3') For any bicoloring of the complete graph on infinitely many vertices, there is an monochromatic infinite complete subgraph.

This clearly implies

(3'') For any positive integer $N$, and any bicoloring of the complete graph on infinitely many vertices, there is an monochromatic complete subgraph on $N$ vertices.

Writing (3'') formally, you wind up with an infinite sequence of axioms, saying that the graph has more than $k$ vertices for every $k$. Since only finitely many of those axioms are used in the proof of (3''), we see that (3) must hold. Of course, there are now direct proofs of (3), but my understanding is that the logic theory proof came first.

Answer 8

A nice source of examples of this kind are decidable theories whose decision procedures have very high computational complexities.

For example, consider Presburger arithmetic, the first-order theory of arithmetic without multiplication. You can show that the theory is decidable (the proof is simple and very pretty, IMO), which means that any statement in the theory is either provably true or provably false. However, the lower bound on the complexity is $2^{2^{\Omega(n)}}$, and the best actually known algorithms are triply-exponential.

Another example, which you might find more mathematically compelling, is that the first-order theory of real closed fields is also decidable. (Tarski showed this back in the 50s, I think.) A corollary of this is that the theory of Euclidean geometry is decidable. However, it's manifestly not the case that geometry is trivial! Tarski's algorithm had nonelementary complexity, and I think the lower bound is doubly-exponential, though I don't know the complexity of the best modern algorithms.

EDIT: these examples are constructive, in the sense that they are decision procedures. This might not really be what you want.

An example of a fully non-constructive existence proof can be found in the usual proof of the completeness of the Kripke semantics of intuitionistic logic. Since this is a classical proof, the disjunction property of intuitionistic logic (i.e., that $A \vee B$'s provability entails either the provability of $A$ or the provability of $B$) is stated classically -- the completeness proof doesn't yield a procedure to give you a particular disjunct.

Answer 9

This is almost a result of the type the OP wanted: In his attempt to prove what is now known as the prime number theorem, Chebyshev used an elementary argument involving a cleverly chosen finite sequence of numerical weights to show that the number of primes up to $x$ is between $0.92 x/\log x$ and $1.11 x/\log x$ for large $x$. It is natural to ask whether Chebyshev's method can be extended to get closer to the prime number theorem. It was shown by Rosser and Erdos-Kalmar independently that for any $\varepsilon>0$, there existed a sequence of weights for which the elementary method of Chebyshev showed that the number of primes up to $x$ lay between $(1-\varepsilon) x/\log x$ and $(1+\varepsilon) x/\log x$. Sending $\varepsilon \to 0$, this would seemingly give an elementary proof of the PNT! But there is a very important catch: the arguments of Rosser and Erdos-Kalmar use the PNT in the proof (and at the time, there was no known elementary proof of the PNT). So we have a non-elementary proof that elementary proofs of (arbitrary approximations to) the PNT exist! See Chapter 9 of

Harold G. Diamond, MR 670132 Elementary methods in the study of the distribution of prime numbers, Bull. Amer. Math. Soc. (N.S.) 7 (1982), no. 3, 553--589.

for further discussion.

As it turns out, this particular result is not quite answering the original question, because it can be made constructive: numerically established zero-free regions of zeta can be converted constructively to elementary proofs of the PNT with an epsilon loss. But it is at least an example of a non-elementary metatheorem about the existence of elementary proofs.

Answer 10

Arrow's Impossibility Theorem, from Social Choice Theory, provides an example of the sort of thing you're talking about:

Specifically, it reads:

For a finite set of individuals and alternatives, where there are at least three alternatives, then any social welfare function that satisfies unanimity and independence of irrelevant alternatives is a dictatorship

The proof may be carried out in higher order logic, employing two inductions. Here is a discussion of a formalization of the proof in Higher Order Logic, in the computer proof assistant Isabelle: http://www4.informatik.tu-muenchen.de/~nipkow/pubs/arrow.pdf

While the statement of the theorem is higher order, for a fixed number of individuals and a fixed number of alternatives it may be expressed in first order logic. Using our meta-theorem from higher order logic, and completeness of first order logic, we know in principle one should be able to prove in first order logic any of the relativisations of Arrow's impossibility theorem...

But actually constructing a proof in first order logic in practice is impossible. Here's a paper where the author provides a first order formulation of the problem and tried to hand it off to an automated theorem prover: http://staff.science.uva.nl/~grandi/Papers/GrandiEndrissLORI2009.pdf

In short, the computer produced a first order proof of the relativised Arrow's theorem for 2 agents and three alternatives in 3 hours, in approximately 200 steps. The author used the first order resolution/paramodulation based program Prover9, and mentioned to me he had somewhat more success with E and Vampire, two other automated proof systems. He also mentioned that, empirically, scaling the problem in either parameter lead to computation time that grew faster than exponential. So proving the theorem for 100000 individuals and 100000 alternatives in first order logic is beyond any person or machine.

TL;DR: Higher Order Logic/First Order completeness affords a metatheorem that all first order instances of Arrow's Impossibility Theorem must be provable in first order logic, but in practice producing a first order proof is transcomputable.

Answer 11

Jacobson's theorem that X^m = X rings are commutative provides an enlightening example, see my post below for further discussion and references
Abstract Thought vs Calculation

Answer 12

I am not sure about the role of the word "nonconstructive" in your question. See whether the following gives you something:

Sometimes it is easier to show that something is true in all models, rather than proving it.

In topos theory, for certain 1st order theories ("geometric theories") one has a generic model, every other model in any other topos (including the category of sets) is an image of the generic model under a map, which preserves the validity of geometric formulas. So if you can show that a certain geometric formula is true for the generic model, then it is true in any given model. Often showing something about the generic model amounts to exhibiting a proof, because in general the only description one has is as a syntactic model. But if you have, say, given a local ring (=a model for the geometric theory of local rings in the topos of sets), and prove a geometric statement about the generic local ring then you know it holds in your given local ring without having provided a proof. Since we have a direct description of the generic local ring as some functor (i.e. not just as a syntactical model), one may well use non-constructive methods for the proof.

Very much related is the statement that, for some geometric theory T, a geometric statement holds for every model of T in every topos iff it holds for every model in Sets (see the last page, before the appendix, of Moerdijk/MacLane). To stay with the above example, you can accordingly prove a theorem about local rings (i.e. usual local rings in sets), using axiom of choice and whatever you want, and then deduce that it must be true e.g. for sheaves of rings with local rings as stalks (i.e. local ring objects in a sheaf topos) - as long as the statement is of the right syntactic form, namely geometric. By topos theoretic completeness there must exist a (constructive) proof, but you deduced this now without exhibiting it.

Answer 13

The most comprehensible example of what the submitter is asking for, in my judgement, is 'duality' in Projective Geometry: For any theorem and its proof, there is a 'dual' theorem and proof, derived from the given theorem/proof by interchanging the terms 'point' and 'line' everywhere.