by Sam Eisenstat 18 days ago | Alex Appel likes this | link | parent As you say, this isn’t a proof, but it wouldn’t be too surprising if this were consistent. There is some $$k \in \mathbb{N}$$ such that $$\square_n \phi \to \phi$$ has a proof of length $$n^k$$ 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 $$\phi$$. 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 $$\phi$$, as long as we only ask for the weaker property that $$\square_n \phi \to \phi$$ will only be provable in length $$n^k$$ for sentences $$\phi$$ of length at most $$k$$.

 by Alex Appel 12 days ago | link I found an improved version by Pavel, that gives a way to construct a proof of $$\phi$$ from $$\Box_{n}\phi$$ that has a length of $$\mathcal{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 $$\exists x:\phi(x)$$ to instantiating a $$c$$ such that $$\phi(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 $$\Omega(n^2)$$, 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 $$\phi$$, the maximum quantifier depth in the proof can be at most $$\mathcal{O}(\sqrt{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(\overline{\psi})\le n\to(Sat_{n}(\overline{\psi},x)\leftrightarrow\Sigma(Sat_{n},\overline{\psi},x))$ ($$\Sigma$$ is the formula laying out Tarski’s conditions for something to be a truth predicate). Also, if $$n\ge$$ quantifier depth of $$\psi$$, there’s a proof of $Sat_{n}(\overline{\psi},x)\leftrightarrow\psi[x]$ ($$\psi[x]$$ is the sentence $$\psi$$ with its free variables substituted for the elements enumerated in the list $$x$$) Also, there’s a proof that $$Sat_{n}$$ 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 $$\mathcal{O}(n^2)$$ lines. One factor of $$n$$ comes from the formula abbreviated as $$Sat_{n}(x,y)$$ getting longer at a linear rate, and the other factor comes from having to prove $$Sat_{n}$$ for each $$n$$ seperately as an ingredient for the next proof. Combining the two parts, the $$\mathcal{O}(\sqrt{n})$$ bound on the quantifier depth and the $$\mathcal{O}(n^2)$$ bound on how long it takes to prove stuff about the truth predicate, make it take $$\mathcal{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 $$Sat_{n}$$ apply to it, and we’ve proved this is equivalent to the statement itself” As a further bonus, a single $$\mathcal{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. reply

NEW DISCUSSION POSTS

I found an improved version
 by Alex Appel on A Loophole for Self-Applicative Soundness | 0 likes

I misunderstood your
 by Sam Eisenstat on A Loophole for Self-Applicative Soundness | 0 likes

Caught a flaw with this
 by Alex Appel on A Loophole for Self-Applicative Soundness | 0 likes

As you say, this isn't a
 by Sam Eisenstat on A Loophole for Self-Applicative Soundness | 1 like

Note: I currently think that
 by Jessica Taylor on Predicting HCH using expert advice | 0 likes

Counterfactual mugging
 by Jessica Taylor on Doubts about Updatelessness | 0 likes

What do you mean by "in full
 by David Krueger on Doubts about Updatelessness | 0 likes

It seems relatively plausible
 by Paul Christiano on Maximally efficient agents will probably have an a... | 1 like

I think that in that case,
 by Alex Appel on Smoking Lesion Steelman | 1 like

 by Sam Eisenstat on No Constant Distribution Can be a Logical Inductor | 1 like

A: While that is a really
 by Alex Appel on Musings on Exploration | 0 likes

> The true reason to do
 by Jessica Taylor on Musings on Exploration | 0 likes