by Sam Eisenstat 293 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 286 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

[Note: This comment is three
 by Ryan Carey on A brief note on factoring out certain variables | 0 likes

There should be a chat icon
 by Alex Mennen on Meta: IAFF vs LessWrong | 0 likes

Apparently "You must be
 by Jessica Taylor on Meta: IAFF vs LessWrong | 1 like

There is a replacement for
 by Alex Mennen on Meta: IAFF vs LessWrong | 1 like

Regarding the physical
 by Vadim Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

I think that we should expect
 by Vadim Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

I think I understand your
 by Jessica Taylor on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

This seems like a hack. The
 by Jessica Taylor on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

After thinking some more,
 by Vadim Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

Yes, I think that we're
 by Vadim Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

My intuition is that it must
 by Vadim Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

To first approximation, a
 by Vadim Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

Actually, I *am* including
 by Vadim Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

Yeah, when I went back and
 by Alex Appel on Optimal and Causal Counterfactual Worlds | 0 likes

> Well, we could give up on
 by Jessica Taylor on The Learning-Theoretic AI Alignment Research Agend... | 0 likes