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.
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 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 as an axiom, but declare that this axiom takes symbols to invoke. This could be done by changing the notion of length of a proof, or by taking axioms and with very long.
See comments. This is a rediscovery of a result from the 1980's that allow concluding ϕ from □n(ϕ) via a O(n)-length proof, and even the statement that the theory has no disproof of length n or less has a single O(n)-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 g(k), f(k), and h(k) be such that f(k)≥g(k)+h(k)+log(k), Eg(k)<h(k), and log(f(k))<g(k), asymptotically.
As a specific example, this can be done by g(k)=k, h(k)=k2, and f(k)=k3.
If it takes a constant number of steps to derive a specific proof regardless of k, the number on it will be suppressed for readability. Also, technically, the original proof has Olog(k) instead of log(k), but this change doesn't alter much.
G(⌈ψ⌉,k):=□g(k)ψ(k)→⊥ ⊢∀k:ψ(k)↔G(⌈ψ⌉,k) (Parametric Diagonal Lemma) ⊢□∀k:ψ(k)↔G(⌈ψ⌉,k) (Bounded Necessitation) ⊢∀k:□log(k)(ψ(k)→G(⌈ψ⌉,k)) (Quantifier Distribution) ⊢∀k,a:□aψ(k)→□a+log(k)G(⌈ψ⌉,k) (Implication Distribution) ⊢∀k,a,b:□aψ(k)→(□b□g(k)ψ(k)→□a+b+log(k)⊥) (Implication Distribution) Now specialize to a=g(k), b=h(k). Also, f(k)≥g(k)+h(k)+log(k) for sufficiently large k above k1. ⊢∀k>k1:□g(k)ψ(k)→(□h(k)□g(k)ψ(k)→□f(k)⊥) ⊢∀k,a:□aψ(k)→□Ea□aψ(k) (Bounded Inner Necessitation) Now, Specializing to a=g(k), we get ⊢∀k:□g(k)ψ(k)→□Eg(k)□g(k)ψ(k) Now, since Eg(k)<h(k) after some time k2, ⊢∀k>k2:□g(k)ψ(k)→□f(k)⊥ Pick a specific value of k, k′, which is sufficiently large. ⊢□g(k′)ψ(k′)→□f(k′)⊥ By the soundness schema, □f(k′)⊥→⊥. The length of this proof isn't constant, because f(k′) might be really big, so then it'd take about log(f(k′)) characters to write down the single application of the soundness schema. ⊢log(f(k′))□g(k′)ψ(k′)→⊥ ⊢log(f(k′))ψ(k′) (By the definition of ψ(k′)) ⊢Elog(f(k′))□log(f(k′))ψ(k′) log(f(k))<g(k) eventually. Since k′ was previously selected to be sufficiently big, ⊢Elog(f(k′))□g(k′)ψ(k′) Now we no longer care about log(f(k′))'s size, because k′ 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 g(k), 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 □nϕ→ϕ can only ever be proved by a proof of n 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 □nϕ→□n−1ϕ for each individual n and ϕ seperately, but I'm not entirely sure of that.EDIT: Doesn't work, see comments.Regardless, assume that any proof of □nϕ→ϕ via iterated soundness axioms will always take c or more steps. EDIT: You don't need to assume this, there's an explicit O(n) proof of that statement.
Then, if we go through the proof again, something interesting happens. Instead of log(f(k)) making its way to the length of the proof, we get f(k) (or more). f(k)≥g(k) in order to get an earlier step of the proof to go through, but then the resulting proof of ψ(k) takes at least f(k) steps to work, so that proof cannot be used with the definition of ψ(k) 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 n-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, □nϕ. 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.