27
$\begingroup$

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.

$\endgroup$
3
  • $\begingroup$ "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. $\endgroup$ Jun 1, 2014 at 5:16
  • $\begingroup$ There's a famous proof that the n-by-n game of Hex has a forced win for the first player, by a strategy-stealing argument. That proof gives no clue what the winning strategy is, but finding it for any fixed n is a finite (though large, like chess) calculation. $\endgroup$
    – none
    Nov 12, 2019 at 9:51
  • $\begingroup$ Not what you asked but sort of related: If P=NP, then Levin's universal search algorithm is a concrete and simple algorithm for solving SAT in polynomial time. But it gives no clue at all about its own complexity, about whether P really equals NP, or what the "actual" algorithm doing the "work" is. $\endgroup$
    – none
    Nov 12, 2019 at 10:26

13 Answers 13

27
$\begingroup$

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.

$\endgroup$
8
  • 2
    $\begingroup$ 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? $\endgroup$
    – Dan Piponi
    Nov 20, 2009 at 21:04
  • 5
    $\begingroup$ 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. $\endgroup$ Nov 21, 2009 at 12:17
  • 1
    $\begingroup$ 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! $\endgroup$ Dec 13, 2009 at 21:40
  • 2
    $\begingroup$ 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. $\endgroup$ Feb 27, 2010 at 13:03
  • 4
    $\begingroup$ @DanPiponi The simple model-theoretic proof of conservativity of GBC over ZFC is indeed nonconstructive. There are also constructive, proof-theoretic proofs of this result, but they are considerably more complicated, and due to reliance on cut elimination, the resulting algorithm has insane complexity (an unbounded tower of exponentials), so it's dubious whether the result is constructive "in practice". This complexity is intrinsic, it's known that some theorems of GBC do require that much longer proofs in ZFC. $\endgroup$ May 11, 2016 at 20:50
31
$\begingroup$

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.

$\endgroup$
5
  • $\begingroup$ That's a very neat result. (While not strictly answering the question, it's certainly in the spirit of it.) $\endgroup$ Nov 20, 2009 at 23:38
  • 3
    $\begingroup$ 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). $\endgroup$ Aug 19, 2011 at 14:02
  • 1
    $\begingroup$ Actually, the situation is worse than you describe and does not rely on $P \neq NP$. That is, it is actually undecidable to compute excluded minors, even though it is polynomial to test for any fixed minor-closed property. For more details see my answer to this MO question. mathoverflow.net/questions/48014/… $\endgroup$
    – Tony Huynh
    May 12, 2016 at 1:26
  • $\begingroup$ Not that it matters for the main point, but by a more recent result of Kawarabayashi, one can make do with quadratic time instead of cubic. $\endgroup$ May 12, 2016 at 8:57
  • 1
    $\begingroup$ @EmilJeřábek The quadratic algorithm is actually a joint result of Kawarabayashi, Kobayashi and Reed. For those interested here is a preprint research.nii.ac.jp/~k_keniti/quaddp1.pdf The journal version has appeared in JCTb (but is behind a paywall). $\endgroup$
    – Tony Huynh
    May 15, 2016 at 11:25
24
$\begingroup$

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.

$\endgroup$
14
$\begingroup$

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

$\endgroup$
8
$\begingroup$

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.

$\endgroup$
3
  • 5
    $\begingroup$ 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. $\endgroup$ Nov 20, 2009 at 19:02
  • $\begingroup$ 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. $\endgroup$ Nov 21, 2009 at 0:11
  • 4
    $\begingroup$ 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 $\endgroup$ Jul 7, 2010 at 14:12
8
$\begingroup$

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.

$\endgroup$
2
  • $\begingroup$ Your argument that $T$ proved $S$ is a direct argument in $T$ that $T$ proves $S$ - i.e. a proof of $S$. $\endgroup$
    – Will Sawin
    May 11, 2016 at 21:04
  • $\begingroup$ Sorry I don't get what you're saying here. Once you prove the Hilbert-Bernays' provability conditions, it is simple to get a direct proof of S within T. Specifically, each instance of (D1) has a direct proof in T, and both (D2) and (D3) have direct proofs in T too, and the properties of the fixed-point you pick also can be proven directly. We never have to go outside of T, unlike the proof in your answer. Of course, it is easier to do reason "T can get from X to Y" in the meta-theory than to actually prove "if X then Y" in T, but the more painful proof only has a constant blow-up in size. $\endgroup$
    – user21820
    May 15, 2016 at 7:15
8
$\begingroup$

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.

$\endgroup$
8
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ The computational complexity of Presburger arithmetic is known precisely: it is complete for the class of problems computable on an alternating Turing machine in doubly exponential time with a linear number of alternations. $\endgroup$ Feb 26, 2020 at 9:32
6
$\begingroup$

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.

$\endgroup$
6
$\begingroup$

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.

$\endgroup$
5
$\begingroup$

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

$\endgroup$
4
$\begingroup$

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.

$\endgroup$
-2
$\begingroup$

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.

$\endgroup$
1
  • 2
    $\begingroup$ This doesn't sound like what the OP is looking for: the question mentioned "... substantially easier to prove (in a metatheory) that a proof exists than it is actually to find the proof". In your example, once one is given a statement and its proof, it is easy to find the proof of the dual statement $\endgroup$
    – Yemon Choi
    May 12, 2016 at 0:00

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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