# SamEisenstat comments on A Loophole for Self-Applicative Soundness

• As you say, this isn’t a proof, but it wouldn’t be too surprising if this were consistent. There is some such that has a proof of length 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 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 will not depend on , as long as we only ask for the weaker property that will only be provable in length for sentences of length at most .

• I found an improved version by Pavel, that gives a way to construct a proof of from that has a length of . 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 to instantiating a such that . 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 , if the maximum quantifier depth in the proof is 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 .

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 ( is the formula laying out Tarski’s conditions for something to be a truth predicate). Also, if quantifier depth of , there’s a proof of ( is the sentence with its free variables substituted for the elements enumerated in the list ) Also, there’s a proof that is preserved under inference rules and logical axioms, as long as everything stays below a quantifier depth of .

All these proofs can be done in lines. One factor of comes from the formula abbreviated as getting longer at a linear rate, and the other factor comes from having to prove for each seperately as an ingredient for the next proof.

Combining the two parts, the bound on the quantifier depth and the bound on how long it takes to prove stuff about the truth predicate, make it take 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 apply to it, and we’ve proved this is equivalent to the statement itself”

As a further bonus, a single -length proof can establish the consistency of the theory itself for all -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.