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