# Are there any good nonconstructive “existential metatheorems”?

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.

-
"The only near-example I can think of right now is in the propositional calculus." This really depends on what you're looking at. First truth tables aren't necessarily the easiest method in 2-valued logic. You can assume the denial of the formula, show that such a denial leads to a contradiction, and then the formula follows as a theorem (by completeness). For formulas with enough variables that does work out as easier than using a truth table. Second, producing a formal proof can, in my opinion, end up as harder than producing a truth table. Consider proving CpNNp or CNNpp. –  Doug Spoonwood Jun 1 '14 at 5:16

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 sufficies to obserrve 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 analagous 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.

-
Is there any sense in which this is non-constructive? When showing that GBC is a conservative extension to ZFC, are you not ultimately defining a machine that can construct ZFC proofs from GBC proofs? –  Dan Piponi Nov 20 '09 at 21:04
A proof of provability which makes essential use of classical logic is nonconstructive, since it doesn't give you a procedure that will construct the proof. Now, since proofs are finite objects, you can enumerate them smallest to larger and check them one at a time, with the fact that the statement is provable serving as a guarantee of termination. This is called "Markov's principle", and is characteristic of the Russian school of constructivism. It is not, however, a universally accepted principle of constructive mathematics, since the search procedure is indefinite and unbounded. –  Neel Krishnaswami Nov 21 '09 at 12:17
I'll go ahead and accept this as the most complete answer among the ones given, but I must note that the other answers all gave interesting perspectives. Thanks to everybody who replied! –  Darsh Ranjan Dec 13 '09 at 21:40
Is this quite correct? I know one can build a GB-universe out of a ZF-universe in this way, but I thought forcing was necessary to bring Choice into the picture. –  Chad Groft Feb 27 '10 at 1:28
Chad, yes, forcing is used in the version with choice, since GBC is usually stated with a global choice principle uniformizing all the set choices into one large class. But if the groud model has ZFC, then the class forcing to attain this is kappa-closed for every kappa and adds no new sets. So even with this global choice, it remains true that GBC is conservative over ZFC. –  Joel David Hamkins Feb 27 '10 at 13:03

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.

-
That's a very neat result. (While not strictly answering the question, it's certainly in the spirit of it.) –  Darsh Ranjan Nov 20 '09 at 23:38
This reminds me of a fact that I noticed from M. Braverman's work that all quadratic Julia sets are computable (in the sense that it can be approximated in the Hausdorff norm to arbitrary precision) but in general it is undecidable how to compute quadratic Julia sets even for effective coefficients (due to the fact that the function mapping from coefficients of the quadratic to Julia sets is discontinuous). –  Russell O'Connor Aug 19 '11 at 14:02

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).

-

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.

-

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.

-
One example is Nonstandard Analysis, which introduces an extra predicate ("nonstandard") and rules for manipulating it into the usual logic (say real analysis). Then it is a theorem that any statement that can be written without the new predicate, if it's provable with the new predicate then it is provable without it. –  Theo Johnson-Freyd Nov 20 '09 at 19:02
I like both gowers' and Theo's examples here. Clearly, it can be hard to take a proof that uses some auxiliary apparatus and rewrite it in the original theory. The difficulty must be somewhere along the continuum between "mere tediousness" and "can't be done effectively in general," but I have no idea where. –  Darsh Ranjan Nov 21 '09 at 0:11
One example of this is where Y is "first order tableaux proof systems" and "X" is the cut rule. In his paper "Don't Eliminate Cut", George Boolos gives a problem which a tableaux with the cut rule can prove in about a page of symbols, but without cut it takes more symbols than there are atoms in the universe. @Darsh - "Don't Eliminate Cut" shows the difficulty can indeed be "can't be done effectively in general" in some situations. Here's Boolos' paper: springerlink.com/content/pj2775t3j0435262 –  Matthew Wampler-Doty Jul 7 '10 at 14:12

G"odel'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"ob'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\"odel'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.

-

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 $O(2^{2^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.

-

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.

-

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 $T$ 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 unichromatic 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 unichromatic 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 unichromatic 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.

-

Arrow's Impossibility Theorem, from Social Choice Theory, provides an example of the sort of thing you're talking about: http://en.wikipedia.org/wiki/Arrow%27s_impossibility_theorem

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.

-

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

-