A Loophole for Self-Applicative Soundness
See comments. This is a rediscovery of a result from the 1980′s that allow concluding from via a -length proof, and even the statement that the theory has no disproof of length or less has a single -length proof. This is not vulnerable to Critch’s Bounded Parametric Lob proof, and was created by looking for ways to make it fail.
This result is just an idea developed very recently, and I’d put ~2:1 odds on it having a fatal flaw, but it looks extremely promising if it works out. EDIT: It works. None of the proof theory checks have been done yet, but it does causes both Lob’s theorem, and Critch’s Bounded Parametric Lob result to fail.
So, to begin with, if a theory thinks it is sound, then it is inconsistent. Proof by Lob’s theorem.
Well that didn’t work.
What if we give the theory a soundness schema over any proof which is of bounded length? Maybe the “there exists a proof” in the standard provability predicate is causing problems.
Well then Critch’s Bounded Parametric Lob comes in to ruin our day. The entire proof will be reproduced below.
Let , , and be such that , , and , asymptotically.
As a specific example, this can be done by , , and .
If it takes a constant number of steps to derive a specific proof regardless of , the number on it will be suppressed for readability. Also, technically, the original proof has instead of , but this change doesn’t alter much.
(Parametric Diagonal Lemma) (Bounded Necessitation) (Quantifier Distribution) (Implication Distribution) (Implication Distribution) Now specialize to a=g(k), b=h(k). Also, for sufficiently large k above . (Bounded Inner Necessitation) Now, Specializing to a=g(k), we get Now, since after some time , Pick a specific value of k, , which is sufficiently large. By the soundness schema, . The length of this proof isn’t constant, because might be really big, so then it’d take about characters to write down the single application of the soundness schema. (By the definition of ) eventually. Since was previously selected to be sufficiently big, Now we no longer care about ’s size, because has been fixed, so
However, not all is lost. If you look carefully at this, you see that the introduction of the soundness scheme lead to a minor proof blowup. Sure, it’s not enough of a blowup to surpass , so the proof of still goes through, but this seems like it might be exploitable....
So then the next step is to make sure that can only ever be proved by a proof of steps or more. The agent can conclude its own soundness for bounded proofs, but it may take a while. I’m pretty sure this is doable by having an axiom schema of the form for each individual and seperately, but I’m not entirely sure of that. EDIT: Doesn’t work, see comments.
Regardless, assume that any proof of via iterated soundness axioms will always take or more steps. EDIT: You don’t need to assume this, there’s an explicit proof of that statement.
Then, if we go through the proof again, something interesting happens. Instead of making its way to the length of the proof, we get (or more). in order to get an earlier step of the proof to go through, but then the resulting proof of takes at least steps to work, so that proof cannot be used with the definition of to conclude .
I’d suspect there’s some more subtle argument that can conclude inconsistency, but breaking the proof of Lob’s theorem is promising.
What’s the use of this, though, if it doesn’t shorten proofs?
Well, there’s a lot of -length proofs, but the “royal road” of abstractly establishing soundness or consistency would allow concluding the sentence directly without having to embark on an exhaustive search for the original proof.
If you spent a while proving something, and then wrote down the result in your notebook, and forgot about it, then, upon observing the notebook page, you can conclude and, since you can bound how good you are at math, you can establish an upper bound on the length of the proof, . This provides a way to establish without having to reprove the thing from scratch, by just thinking for a while about “Do I trust my own bounded proofs? Yes I do.”
This solves the Notebook Problem in Vingean Reflection.
As you say, this isn’t a proof, but it wouldn’t be too surprising if this were consistent. There is some k∈N such that □nϕ→ϕ has a proof of length nk by a result of Pavel Pudlák (On the length of proofs of finitistic consistency statements in first order theories). Here I’m making the dependence on n explicit, but not the dependence on ϕ. I haven’t looked at it closely, but the proof strategy in Theorems 5.4 and 5.5 suggests that k will not depend on ϕ, as long as we only ask for the weaker property that □nϕ→ϕ will only be provable in length nk for sentences ϕ of length at most k.
I found an improved version by Pavel, that gives a way to construct a proof of ϕ from □nϕ that has a length of O(n). The improved version is here.
There are restrictions to this result, though. One is that the C-rule must apply to the logic. This is just the ability to go from ∃x:ϕ(x) to instantiating a c such that ϕ(c). Pretty much all reasonable theorem provers have this.
The second restriction is that the theory must be finitely axiomatizable. No axiom schemas allowed. Again, this isn’t much of a restriction in practice, because NBG set theory, which proves the consistency of ZFC, is finitely axiomatizable.
The proof strategy is basically as follows. It’s shown that the shortest proof of a statement with quantifier depth n must have a length of Ω(n2), if the maximum quantifier depth in the proof is 2n or greater.
This can be flipped around to conclude that if there’s a length-n proof of ϕ, the maximum quantifier depth in the proof can be at most O(√n).
The second part of the proof involves constructing a bounded-quantifier version of a truth predicate. By Tarski’s undefinability of truth, a full truth predicate cannot be constructed, but it’s possible to exhibit a formula for which it’s provable that qd(¯¯¯¯ψ)≤n→(Satn(¯¯¯¯ψ,x)↔Σ(Satn,¯¯¯¯ψ,x)) (Σ is the formula laying out Tarski’s conditions for something to be a truth predicate). Also, if n≥ quantifier depth of ψ, there’s a proof of Satn(¯¯¯¯ψ,x)↔ψ[x] (ψ[x] is the sentence ψ with its free variables substituted for the elements enumerated in the list x) Also, there’s a proof that Satn is preserved under inference rules and logical axioms, as long as everything stays below a quantifier depth of n.
All these proofs can be done in O(n2) lines. One factor of n comes from the formula abbreviated as Satn(x,y) getting longer at a linear rate, and the other factor comes from having to prove Satn for each n seperately as an ingredient for the next proof.
Combining the two parts, the O(√n) bound on the quantifier depth and the O(n2) bound on how long it takes to prove stuff about the truth predicate, make it take O(n) steps to prove all the relevant theorems about a sufficiently large bounded quantifier depth truth predicate, and then you can just go “the statement that we are claiming to have been proved must have Satn apply to it, and we’ve proved this is equivalent to the statement itself”
As a further bonus, a single O(n)-length proof can establish the consistency of the theory itself for all n-length proofs.
It seems like a useful project to develop a program that will automatically write a proof of this form, to assess whether abstract unpacking of bounded proofs is usable in practice, but it will require digging into a bunch of finicky details of exactly how to encode a math theory inside itself.
Caught a flaw with this proposal in the currently stated form, though it is probably patchable.
When unpacking a proof, at some point the sentence □1ϕ will be reached as a conclusion, which is a false statement.
I misunderstood your proposal, but you don’t need to do this work to get what you want. You can just take each sentence □nϕ→ϕ as an axiom, but declare that this axiom takes n symbols to invoke. This could be done by changing the notion of length of a proof, or by taking axioms ψϕ,n→(□nϕ→ϕ) and ψϕ,n with ψϕ,n very long.