6

Suppose we are studying the Zermelo–Fraenkel set theory as a first-order logic and our metatheory is also the Zermelo–Fraenkel set theory.

Is there a statement $P$ such that

  • no direct proof of $P$ has ever been written down
  • but an algorithm has been formulated in the metatheory that has been shown to terminate and has been shown to output a valid proof of $P$?

EDIT: as pointed out by Emil Jeřábek if one assumes $\Sigma_1$-soundness then a variant of "this statement cannot be proven in fewer than a googol symbols" works. Ideally I would like an example where $\Sigma_1$-soundness/consistency is not assumed.

metameme
  • 61
  • Anything here will work https://mathoverflow.net/q/112097/30186 – Wojowu Feb 18 '21 at 16:32
  • @Wojowu I don't think it will. There the algorithm either outputs a proof of $P$ or $\neg P$ but you don't know which one. – metameme Feb 18 '21 at 17:15
  • 3
    If you don't mind me asking what may be an elementary question, a proof that an algorithm produces a proof of P is in fact a proof of P, isn't it? – Pierre PC Feb 18 '21 at 21:31
  • 2
    How about a long long $(\forall x)(x = x) \land (\forall x)(x = x) \land (\forall x)(x = x) \land (\forall x)(x = x) \land \cdots \land (\forall x)(x = x)$? – François G. Dorais Feb 18 '21 at 22:21
  • @PierrePC: No: for example, Peano arithmetic proves that ZFC proves that Peano arithmetic is consistent (so proves the correctness of an algorithm returning said proof), but Peano arithmetic does not prove that Peano arithmetic is consistent. – Gro-Tsen Feb 18 '21 at 23:56
  • @FrançoisG.Dorais I don't think your example works because the length of the proof is a small constant times the length of the statement. – metameme Feb 19 '21 at 12:27
  • @Gro-Tsen I see. What about a such an example within the same theory? I assumed that is what the OP meant, saying that the theory and metatheory are ZF. I like your posted answer very much, but I don't think it's an example of it, since ∀n,P(n) is not the statement proved, but rather P(n) is proved for all n. – Pierre PC Feb 19 '21 at 13:26
  • @PierrePC To clarify, in my answer, $P(n)$ ($:=\mathrm{Consis}(\mathsf{ZFC}_n)$), for some large $n$, is supposed to be the statement answer OP's question, not $\forall n.P(n)$. I added the remark on the latter as a strengthening of the question which is otherwise too trivial (just take $n+1=1+n$ for some very large $n$). … – Gro-Tsen Feb 19 '21 at 13:32
  • (contd.) My example that “$T$ proves that $T'$ proves $P$” is distinct from “$T'$ proves $P$” uses two different theories to illustrate the importance of separating them; of course, if $T$ proves that $T$ proves $P$ and if $T$ is arithmetically sound (which we certainly hope for ZFC and know for Peano), then $T$ proves $P$ (and the converse is trivial). But the statements are still quite distinct. – Gro-Tsen Feb 19 '21 at 13:35
  • You can’t avoid assuming that ZF is consistent, or at least, that it has no short proof of contradiction. Otherwise, every statement $P$ has a short proof. – Emil Jeřábek Feb 21 '21 at 08:02
  • @EmilJeřábek Let us shift focus to shortest proofs that somebody actually has written down. As far as I am aware nobody has written down a proof of a contradiction in ZF. – metameme Feb 21 '21 at 08:52

4 Answers4

10

For every concrete natural number $n$, $\mathsf{ZFC}$ proves the consistency of the subset, let's call it $\mathsf{ZFC}_n$, of the axioms of $\mathsf{ZFC}$ where the axiom scheme of Replacement is restricted to $\Sigma_n$ predicates: this follows from standard arguments around the reflection principles (there exists a $V_\alpha$ which reflects any finite number of formulas of set theory, and furthermore, $\Sigma_n$-replacement can be written as a single statement). Let $\mathrm{Consis}(\mathsf{ZFC}_n)$ be the statement in question (that $\mathsf{ZFC}_n$ is consistent): then

  • “$\mathrm{Consis}(\mathsf{ZFC}_n)$” is a theorem of $\mathsf{ZFC}$ for every $n$; this fact is a theorem of, say, Peano arithmetic, and furthermore, there exists an explicit algorithm which, given $n$, produces a proof of $\mathrm{Consis}(\mathsf{ZFC}_n)$ in $\mathsf{ZFC}$ (the “standard arguments” I alluded to),

  • but of course, by Gödel's incompleteness theorem, “$\forall n. \mathrm{Consis}(\mathsf{ZFC}_n)$”, which is just $\mathrm{Consis}(\mathsf{ZFC})$ by compactness) cannot be a theorem of $\mathsf{ZFC}$ if $\mathsf{ZFC}$ is consistent, in other words, the proof cannot be made uniform within $\mathsf{ZFC}$.

So for $n$ large enough, $\mathrm{Consis}(\mathsf{ZFC}_n)$ is an example of what you are asking for: its proof has never been explicitly written down within $\mathsf{ZFC}$, only as a template algorithm which demonstrably produces a proof for any given $n$, yet it's not a trivial matter of instancing a single uniform proof¹ because no single uniform proof exists.

  1. I mean, it's not like something like $n+1=1+n$ which is obviously provable for each $n$ and for many $n$ the proof has never been written down yet we have an algorithm which produces it by applying the proof of $\forall n.(n+1=1+n)$ to that particular $n$ (this formally answers your question, but obviously you want more than that): in my above example, you simply cannot make the proof uniform, because Gödel's theorem prevents it.
Gro-Tsen
  • 29,944
  • 4
  • 80
  • 335
  • Can one estimate how quickly the length of the proof of this statement grows with $n$? – metameme Feb 19 '21 at 05:05
  • 1
    I believe the length of the proof grows just polynomially with a reasonable exponent (maybe $2$ or $3$?): each alternation of quantifiers brings a new batch of standard arguments that need to be called in, possibly in a once or twice nested fashion, nothing dramatic. But I didn't check any of this carefully. – Gro-Tsen Feb 19 '21 at 08:32
1

This is a suggested clarification of the question; judging from the responses, I think the question is not completely clear. [EDIT: Under the assumption that this clarification is correct, an answer to the question is given below.]

The intended question, I believe, is something like this. If there is a short ZF proof of "ZF proves P" then is there necessarily a short ZF proof of P? If not, then can we write down an explicit example of a short ZF proof of "ZF proves P" for which it is infeasible to write down an explicit ZF proof of P?

The first thing to note is that there need not be a ZF proof of P at all, unless we assume some kind of soundness condition on ZF. For example, suppose P is the statement 1=0. We don't know a way of deducing the inconsistency of ZF from the assumption that ZF proves "ZF is inconsistent." Now, this observation does not torpedo the question, because if someone explicitly writes down a ZF proof of "ZF proves P" then we are all going to be convinced both that ZF proves P and that P. But it does show that passing from a proof of "ZF proves P" to a proof of P is not entirely trivial.

The second observation is that examples involving infeasibly large P do not really answer the intended question. We are, I think, supposed to fix some straightforward algorithm for converting P into "ZF proves P". In particular, if P is infeasibly large then "ZF proves P" will be infeasibly large, so that writing down an explicit proof of "ZF proves P" will be infeasibly large. What is being asked is, how much of a blowup in proof size can there be when passing from "ZF proves P" to P itself?

EDIT (based on Emil Jeřábek's comments below): Suppose we interpret the phrase "has been shown" as permitting us to assume that ZF is $\Sigma_1$-sound. Then, as explained in the comments below, we can take some fast-growing recursive function $f$ (Ackermann, say), and let $P$ be the following "self-referential" statement:

There exists $x$ such that there is a ZF-proof of $\mathsf{Prov}(P)$ of length at most $x$ but no ZF-proof of $P$ of length at most $f(x)$.

Since $P$ is $\Sigma_1$, one can explicitly construct a relatively short ZF-proof of $\mathsf{Prov}(P)$. If we now assume that ZF is $\Sigma_1$-sound, then we can conclude that $P$ is true, so that means that the "trivial" algorithm that searches for a proof of $P$ will terminate with a valid proof of $P$. However, the shortest such proof will be infeasibly long and hence has never been (and never will be) written down explicitly.

If the assumption that ZF is $\Sigma_1$-sound bothers you, then you can try carrying out the following thought experiment. Imagine yourself following the above recipe and explicitly constructing the ZF-proof of $\mathsf{Prov}(P)$. Imagine yourself reading through this ZF-proof line by line. Presumably, reading and understanding a ZF-proof of something convinces you that it is true, so at the end of this process, you will become convinced that $P$ is in fact provable in ZF. Now you have to decide for yourself whether the ZF-provability of $P$ "has been shown."

Timothy Chow
  • 78,129
  • 1
    It’s not very clear to me that this is actually the intended question. But for the record, the answer is that the shortest ZF-proof of $P$ can be insanely enormously longer than a ZF-proof of “ZF proves $P$”. More precisely, there is no ZF-provably total recursive function $f$ such that for any $P$, whenever “ZF proves $P$” has a ZF-proof of length $n$, then $P$ has a ZF-proof of length at most $f(n)$. There is nothing special about ZF here, this holds for any $\Sigma^0_1$-sound recursively axiomatized theory that extends, say, $I\Delta_0+\mathrm{EXP}$. – Emil Jeřábek Feb 19 '21 at 16:47
  • @EmilJeřábek Ah, good! That's what I expected but I wasn't sure. A followup question is, can we explicitly write down a P for which we could explicitly write down a ZF proof of "ZF proves P" if we really wanted to, but such that the shortest ZF proof of P is infeasible? Even if that turns out to not quite answer the original question as stated, I think it would come very close. – Timothy Chow Feb 19 '21 at 17:36
  • 2
    Basically, yes. The statement is quite artificial, but the argument is constructive: if you fix a provably total $\Sigma_1$ definition of $f$, you define $P$ by Gödel’s diagonal lemma (which is itself an explicit construction) so that it is ZF-provably equivalent to the $\Sigma_1$ sentence “there is a ZF-proof of $\Box P$ of length $x$ such that no ZF-proof of $P$ has length $\le f(x)$” (where $\Box$ is the formalized provability predicate for ZF). Then $\mathrm{ZF}+\neg P\vdash\Box\Box P\to\Box P$, while $\vdash P\to\Box P$ as $P$ is $\Sigma_1$, hence ZF proves $\Box\Box P\to\Box P$, ... – Emil Jeřábek Feb 19 '21 at 18:24
  • 2
    ... hence ZF proves $\Box P$ by Löb’s theorem. Löb’s theorem only blows up the proof size polynomially. Thus, you can explicitly construct both $P$ and a ZF-proof of $\Box P$, and they will be fairly short. (The argument continues by using the assumed $\Sigma_1$-soundness of ZF to infer that $P$ is true in $\mathbb N$, which gives the desired speed-up.) – Emil Jeřábek Feb 19 '21 at 18:28
  • 1
    I should perhaps clarify that $\Sigma_1$ -soundness is only really needed to make sure $f$ is truly a total recursive function in the real world (which will hold anyway if you take an explicit known total function such as Ackermann). Simply put, if ZF is consistent but $\Sigma_1$-unsound, there is a statement $P$ such that ZF proves "ZF proves $P$", but ZF does not actually prove $P$ at all, hence the gap between the lengths of the proofs is "infinite". – Emil Jeřábek Feb 19 '21 at 20:13
  • @EmilJeřábek Good point, although the way I'm interpreting the question, the search for a proof of $P$ has to be "shown" to terminate. – Timothy Chow Feb 20 '21 at 02:46
  • I don't understand one point. In your example is the object theory and the metatheory the same? It seems to me you allow the metatheory to assume something ($\Sigma_1$-soundness in this case) but not the object theory. – metameme Feb 20 '21 at 05:15
  • @metameme The object theory and the meta-theory are both ZF. The meta-meta-theory (which is where you establish that any proof in object theory is much longer than the proof in meta-theory saying that such a proof exists) can be something like a weak fragment of arithmetic + consistency (or $\Sigma_1$-soundness, depending on the formulation) of ZF. – Emil Jeřábek Feb 20 '21 at 10:25
  • Though, the statement that “any proof in object theory is much longer than the proof in meta-theory saying that such a proof exists” is a true $\Sigma_1$ sentence, and as such it is provable already in Robinson’s $Q$. So the meta-meta-theory can be just $Q$. Which begs the question what is the meta-meta-meta-theory, where you establish that the $\Sigma_1$-sentence is true indeed. It’s turtles all the way down, I guess. You know, I’m not a big fan of these “object theory or meta-theory” discussions; with theories capable of self-reference, the distinction is often quite blurred or meaningless. – Emil Jeřábek Feb 20 '21 at 10:42
0

[This is more an overly long comment than a proper answer.]

There is a formal ZF-proof for a theorem $T$, if and only if the algorithm that generates all potential ZF-proofs, checks whether they are for $T$ and halts if the answer is ever "yes" terminates. Thus, as long as we use the usual standards for "proof" in mathematics, the distinction from the question doesn't really make sense.

Since we hardly ever write down formal ZF-proofs for stuff, the answer quite certainly is "no" if we read "known proof" as "someone has explicitly written down a formal ZF-proof" - but for boring reasons.

To get somewhere interesting, we might ask whether there is an instance of a theorem $T$ where the shortest explicit formal ZF-proof is signficantly longer than the combination of a program and a formal ZF-proof that the program would halt and output a formal ZF-proof of $T$.

If we only count the length of the program and the proof that it terminates, but keep the proof that the output indeed is a formal ZF-proof of $T$ separate, then the answer is clearly "yes", and we can do this for almost all theorems. Here, we just add to our exhaustive proof search algorithm from above a sufficiently big length cutoff. The termination proof is trivial, and the program itself has size constant + Kolmogorov complexity of $T$ + Kolmogorov complexity of the size of the shortest proof of $T$, which generally be less than the size of the shortest proof itself.

Arno
  • 4,471
  • But to make sure that your cutoff works you need to a priori have a proof of $T$ (there is no computable bound on the length of the shortest proof in terms of the length of the theorem). So I think it still makes sense to ask if there is a situation where no direct proof of $T$ has ever been written down yet an algorithm was written down that produces a proof and the proof of halting was given. – metameme Feb 18 '21 at 19:51
  • @metameme Hence the distinction between the case where we measure program+correctness proof+halting proof. and the case where we just measure program+halting proof, and keep our correctness proof separate. And sure, the natural way for the correctness proof would be "here is a ZF proof of T a certain size, hence the program will find one". – Arno Feb 18 '21 at 19:54
  • @metameme Maybe you could clarify which of the four interpretations of your question you have in mind? Or whether you mean something else entirely? – Arno Feb 18 '21 at 19:57
  • Thank you for your remarks. I rewrote the question. I hope it's clearer now. – metameme Feb 18 '21 at 20:07
  • @metameme This could either be my first reading or my second, depending whether you are talking formal or informal proofs. Either way, the answer will be boring. – Arno Feb 18 '21 at 20:09
  • I meant formal proofs. I don't think the answer is boring in that case is it? – metameme Feb 18 '21 at 20:11
  • @metameme Well, as said in my second paragraph, it is extremely uncommon to ever write down formal ZF proofs for stuff. So the answer then is quite certainly going to be "no", because noone ever bothered. One the other hand, you could find a theorem that hasn't had a formal ZF proof written, and write the termination/correctness proof of an algorithm, and then the answer is "yes". Either case, this is just about accidents, not about meaningful stuff. Hence the proof length ideas in the third and fourth paragraph. But we need to stop discussing in the comments now, I think. – Arno Feb 18 '21 at 20:15
  • I see your point. But then one can't just take the Kolmogorov complexities because it imposes no limit on the running time. Maybe it would be more reasonable to consider polynomially bounded Kolmogorov complexities. – metameme Feb 18 '21 at 20:21
0

Not really my area of expertise, but I think that the answer to your question is no.

If you could prove the existence of an algorithm for proving $P$ and prove that the algorithm terminates and that the proof it produces is valid, then you have proven that $P$ is true, i.e., is a theorem of ZFC. Even if the proof is meta-theoretic, it could be formalized in ZFC to produce a proof of $P$ that is shorter than the one produced by its algorithm.

The problems referenced above (by @Wojowu) are ones for which we can prove that either $P$ or $\lnot P$ is a ZFC theorem, so they are not independent statements like CH. For any such statement, there is an algorithm for deciding $P$: just write a program that enumerates all the theorems of ZFC and wait for either $P$ or $\lnot P$ to appear. The problem, of course, is that the time required might be intractable.

On the other hand, there certainly exist theorems of ZFC for which the shortest possible proof requires an intractably large number of steps, say $10^{110}$. This number exceeds the number of nanoseconds in 14 billion years multiplied by the number of atoms in the universe. So, if you could convert every atom of the universe to a Gigahertz computing device, then travel back to the beginning of time and start this computing system, it would not yet have completed $10^{110}$ operations.

It is entirely possible that, for example, $P\ne NP$ is such a theorem. If so, the Clay Institute's million dollars is safe :-).

LSpice
  • 11,423
Jeff Norden
  • 553
  • What is 'it' in "shorter than the one produced by its algorithm"? – LSpice Feb 18 '21 at 21:29
  • I.e., If you formalize a proof of the existence and correctness of an algorithm that produces a proof of $P$, you could wind up with a proof of $P$ that is shorter than the one that algorithm produces. Of course, this requires a choice of a specific framework for formalizing proofs and measuring their lengths. – Jeff Norden Feb 18 '21 at 21:54