11
$\begingroup$

Gödel's speed-up theorem implies that some proofs can get significantly shortened when allowing extra axioms. There are concrete examples of this phenomenon for instance when moving from Peano arithmetic (PA) to PA + consistency(PA), or when moving from PA to second-order arithmetic, see for instance this question.

However, I am not aware of concrete examples of such a dramatic shortening when moving from constructive logic to classical logic.

So, is there a known example of a statement that is both true in constructive and classical logic, that has a reasonably short proof in classical logic, but such that any proof in constructive logic would be gigantic (and thus not "human-readable")?

Ideally, an example would be a statement that would feel "concrete enough" for the average mathematician, i.e. a statement involving numbers, graphs, algebraic structures, etc. (Friedman's examples on Kruskal's tree theorem fit the bill)

(I would also be interested in an example that has a simple proof in classical logic, that is not yet known to be true in constructive logic but such that a proof, if it exists, must be gigantic.)

Update: There are indeed ways to construct such examples as indicated below, but which feel a bit like cheating as they essentially add the extra axiom in the statement. I am more thinking of some existence theorem of the form

"For every object x satisfying ..., there exists an object y satisfying ...".

Think Friedman's examples, Four-Color Theorem, etc. In other words, an existence theorem where every constructive proof would be gigantic, but where there exists a short nonconstructive proof. Here again, one may hack this by artificially adding something of the form "or (A or not(A))" in the statement, but of course that's not really what I have in mind, nor the sort of statement a mathematician working with classical logic would try to prove on a regular day ;-)

Improve this question
$\endgroup$
3
  • $\begingroup$ Very interesting question. In my personal experience in algebra, a classically provable and interesting statement is either also constructively provable, with a proof of similar length, or there's an obvious reason for why there is no hope that a constructive proof exists. I'm speaking about informal proofs here, not proofs in some formal system. I'm looking forward to making a new experience and adapting my intuition! $\endgroup$
    – Ingo Blechschmidt
    Commented Mar 1, 2018 at 13:15
  • $\begingroup$ I did encounter some example of things that where true constructively but whose proof was considerably harder than the classical one. One of them was the the following: let G be a compact localic group acting on a decidable set X. Then $X$ can be covered by finite subset stable under the action of $G$. Classically one easily show that the orbit of any point is a finite $G$ stable subset. but constructively it fails if we do not assume $G$ to be locally positive (Overt). I gave a completely different constructive proof of it in arxiv.org/abs/1505.04987. (prop 4.3 and lemma 4.2 and 4.1). $\endgroup$
    – Simon Henry
    Commented Mar 1, 2018 at 21:16
  • $\begingroup$ It is indeed an existence statement as asked, But that does not qualifies as something where the proof would become so long that it is not 'human readable' (It only takes 2 pages in the end) $\endgroup$
    – Simon Henry
    Commented Mar 1, 2018 at 21:17

4 Answers 4

Reset to default
12
$\begingroup$

Here is a general method to construct numerous examples.

Let $A$ be something that is provable constructively, but only with a very long proof. Now consider the statement $$A\vee \neg A$$ This has a very short proof in classical logic, but constructively, you'd have to give the proof of $A$, as $\neg A$ will have no proof.

Improve this answer
$\endgroup$
16
  • 2
    $\begingroup$ My thought had been to just prepend "$(X \lor \lnot X)$" to any formula that is constructively provable with an extra propositional variable $X$. But I think the spirit and challenge of these kinds of questions is to find natural examples, rather than something analogous to "Either Ramsey's theorem is true, or it is false" $\endgroup$
    – Carl Mummert
    Commented Feb 28, 2018 at 20:55
  • 2
    $\begingroup$ Well, you can hide bifurcation, but I think it will be a central phenomenon of such natural examples that the classical proof proceeded in a proof by cases, without deciding which case occurs, but the constructive proof had to give more difficult information. $\endgroup$
    – Joel David Hamkins
    Commented Feb 28, 2018 at 20:59
  • 4
    $\begingroup$ I don’t think this method works in general: $A \vee \lnot A$ may have a short constructive proof even if $A$ only has a long proof. For instance, let $A$ be the statement “there is no counterexample to FLT with $a,b,c,n < 10^{10^{10^{10}}}$”. Then $A \vee \lnot A$ has a short proof (using the fact that $A$ is a finitely-bounded quantification of an arithmetic statement), but $A$ has no known short proof. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Mar 1, 2018 at 10:58
  • 3
    $\begingroup$ I'm feeling that we're mixing "$\mathrm{HA} \vdash A \vee \neg A$" with "$\mathrm{HA} \vdash (\mathrm{HA} \vdash A \vee \neg A$)". The latter statement implies the former, but only because we trust Heyting arithmetic. HA itself doesn't trust HA; there is no HA-proof of "$(\mathrm{HA} \vdash C) \Rightarrow C$". Formal HA-proofs of "$A \vee \neg A$" can be long, while formal HA-proofs of "$\mathrm{HA} \vdash A \vee \neg A$" can be short. $\endgroup$
    – Ingo Blechschmidt
    Commented Mar 1, 2018 at 13:07
  • 6
    $\begingroup$ @IngoBlechschmidt: No, I’m not mixing them up; my sketch really is a sketch of a short HA-proof of $A \vee \lnot A$ — unwinding the details is too long for a comment, but isn’t too much work. @ Joel: You’re not misunderstanding entirely — as @ SimonHenry says, there’s a procedure (cut-elimination) which takes any HA-proof of “$A \vee \lnot A$” to a proof in canonical form, which must come from either a proof of $A$ or a proof of $\lnot A$. So indeed, if you can prove $A \vee \lnot A$, you can prove either $A$ or $\lnot A$. But cut-elimination can greatly blow up the length of proofs. $\endgroup$
    – Peter LeFanu Lumsdaine
    Commented Mar 1, 2018 at 14:15
6
$\begingroup$

I am no expert in logic, but let me give it a try. There is an old (1970) theorem of M. Waldschmidt that at least one of the numbers $e^e$ and $e^{e^2}$ is transcendental. So, the statement is a disjunction $A\lor B$. To prove this in constructive logic, you need to prove either $A$ or $B$ which, for the best of my knowledge, is wide open. (Though nobody doubts that both $A$ and $B$ are true as it follows from the Schanuel conjecture.) I do not know if a proof in constructive logic would be gigantic, but this far there is no proof whatsoever. Of course, this example is still in the same direction is one given by Joel Hamkins, but personally I would not call it cheating.

[EDIT] Wait, I think I know a better example: the Roth's theorem!

For any irrational algebraic number $\alpha$ and any $\varepsilon>0$ there is $c>0$ such that $$\left|\alpha-\frac{p}{q}\right|>\frac{c}{q^{2+\varepsilon}}$$ for all integers $q>0$ and $p$.

This is a $\Pi_2^0$ statement whose known proofs are nonconstructive. (The existence is proved by contradiction.) A constructive proof of this theorem would be really big news.

Improve this answer
$\endgroup$
5
  • 3
    $\begingroup$ Along the same lines, we currently don't know that $e + \pi$ is transcendental, nor do we know that $e\pi$ is transcendental. But we know one of them must be, because if both were algebraic, then the roots of $x^2 - (e + \pi)x + e\pi$ would also be algebraic, contrary to what we know about $e$ and $\pi$. $\endgroup$
    – Todd Trimble
    Commented Mar 1, 2018 at 11:59
  • $\begingroup$ These are interesting examples, but the OP had requested examples where the statement is in fact provable both constructively and classically, but where the constructive proof was necessarily much longer. Do you have any reason to think that your examples are constructively provable, but do not have short constructive proofs? $\endgroup$
    – Joel David Hamkins
    Commented Mar 1, 2018 at 12:43
  • $\begingroup$ You are right. I am convinced that the Schanuel conjecture can be proved in constructive logic, but this is just my personal opinion. Of course, such a proof ought to be pretty long. As for the Roth's theorem, I have no idea. It is conceivable that it cannot be proved in constructive second order arithmetic, for example. $\endgroup$
    – Alex Gavrilov
    Commented Mar 1, 2018 at 12:57
  • 1
    $\begingroup$ Since the statement of Roth’s theorem is $\Pi_2$, not only it automatically has a constructive proof once it has a classical proof, also the constructive proof is not much longer than the classical one. See en.wikipedia.org/wiki/Friedman_translation. $\endgroup$
    – Emil Jeřábek
    Commented Feb 9, 2021 at 10:33
  • 2
    $\begingroup$ My comment above should read “If the statement of Roth’s theorem were $\Pi_2$, ...”. In fact, as far as I can see, Roth’s theorem is only $\Pi_3$, now that I think about it. $\endgroup$
    – Emil Jeřábek
    Commented Feb 9, 2021 at 14:18
2
$\begingroup$

Here is a something which might be an example:

Sometimes there are statements $A$ and $A^*$ which a classical mathematician would consider equivalent and a constructive mathematician would not. An example is the existence of a winning strategy for Hex.

$A(n):$ the game of Hex on an $n \times n$ board will never end in a draw AND there is no winning strategy for the second player (the first could steal it)

$A^*(n)$ There is a winning strategy for the first player in the game of Hex on an $n \times n$ board.

There is a short constructive proof of “$\forall n\,A(n)$ “

I think a constructive mathematician would accept that $A^*(13)$ is true but consider it possible that any explicit strategy would be enormous.

A classical mathematician would easily accept “ $\forall n\, A^*(n)$ “ That might be unprovable constructively.

———

A variation:

$B$ no position can end in a draw.

$B^*$ for every position is either a winning strategy for the next player or a winning strategy for the previous player.

From Wikipedia:

In 1976, Shimon Even and Robert Tarjan proved that determining whether a position in a game of generalized Hex played on arbitrary graphs is a winning position is PSPACE-complete.[12] A strengthening of this result was proved by Reisch by reducing quantified Boolean formula in conjunctive normal form to Hex played on arbitrary planar graphs.[13] In computational complexity theory, it is widely conjectured that PSPACE-complete problems cannot be solved with efficient (polynomial time) algorithms. This result limits the efficiency of the best possible algorithms when considering arbitrary positions on boards of unbounded size, but it doesn't rule out the possibility of a simple winning strategy for the initial position (on boards of unbounded size), or a simple winning strategy for all positions on a board of a particular size.

Improve this answer
$\endgroup$
4
  • 1
    $\begingroup$ I'm not really sure, but it seems to me in light of the comments on my answer that for any particular $n$, since this is a finite game, one might constructively prove (perhaps even by a short proof) the equivalence of the first player having a winning strategy with the second player not having a winning strategy. The reason I expect this might be true is that the equivalence of these two statements is essentially a statement of de Morgan's law in an instance where all quantifiers are bounded (essentially by n), and that seemed to be what was driving the phenomenon in the other case. $\endgroup$
    – Joel David Hamkins
    Commented Mar 1, 2018 at 21:45
  • $\begingroup$ That is true. So could a constructive mathematician say “I accept that $\forall n$ there is a proof of player one has a winning strategy but not that there is a proof of $\forall n$ player one has a winning strategy.? That would speak to complexity disparity. Then there are examples like $x_n$ is $1$ or $0$ according as $2^{p_n}-1$ is or is not prime and $y_n=x_n(1-x_n)$. Then $y_n=0$ or $y_{1000000}=0$ is very different constructively than classically. Maybe $2^{2^n}$ is better. $\endgroup$
    – Aaron Meyerowitz
    Commented Mar 1, 2018 at 22:47
  • 1
    $\begingroup$ Joel is right, one can constructively prove that the first player has a winning strategy. If you interpret that proof as a program and run it, you'll get an explicit winning strategy; however, the resulting algorithm will simply apply a brute-force search to find the strategy. If you want the extracted algorithm to be more clever, then you have to supply a more insightful proof that the first player has a winning strategy (one which doesn't use a strategy-stealing argument). $\endgroup$
    – Ingo Blechschmidt
    Commented Mar 2, 2018 at 15:52
  • 1
    $\begingroup$ Aaron: This happens in some situations, but not here; and also, it's not a phenomenon particular to constructive mathematics. For instance, Peano arithmetic can prove, for any fixed natural number $n$, that Hercules can beat any hydra with $n$ heads. But Peano arithmetic can't prove "for any $n$, Hercules can beat any hydra with $n$ heads". $\endgroup$
    – Ingo Blechschmidt
    Commented Mar 2, 2018 at 15:57
1
$\begingroup$

I'm not quite sure about the exact constructive content of these proofs but the following is perhaps in line with what you're looking for.

Recall Ramsey's theorem: For any natural numbers $c, k, m$ there is a natural number $n$ so that any $c$-coloring of the complete hypergraph of $k$-tuples of $[n] = \{0,...,n-1\}$ has a monochromatic subgraph of size $m$. The standard (relatively straightforward) proof of this fact uses infinite Ramsey's theorem which itself is a consequence of Konig's lemma and requires the axiom of choice (so not constructive) but one can prove this result in PA by triple induction on $c$, $k$ and $m$. If I'm not mistaken the $n$ that you get from any such triple is in fact computable from that triple (though not in any feasible sense) so I imagine that the theorem is in fact provable constructively though with considerably more effort.

Improve this answer
$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .