by Benja Fallenstein 1465 days ago | Patrick LaVictoire likes this | link | parent I would suggest changing this system by defining $$\psi(n)$$ to mean that no $$m\le n$$ is the Gödel number of a proof of an inconsistency in ZFC (instead of just asserting that $$n$$ isn’t). The purpose of this is to make it so that if ZFC were inconsistent, then we only end up talking about a finite number of levels of truth predicate. More specifically, I’d define $$T_n$$ to be PA plus the axiom schema $\forall m\ge n.\;\psi(m)\to\forall x.\;\mathrm{Tr}_m(\ulcorner\varphi(\overline x)\urcorner)\leftrightarrow\varphi(x).$ Then, it seems that Jacob Hilton’s proof that the waterfalls are consistent goes through for this waterfall: Work in ZFC and assume that ZFC is inconsistent. Let $$n$$ be the lowest Gödel number of a proof of an inconsistency. Let $$M$$ be the following model of our language: Start with the standard model of PA; it remains to give interpretations of the truth predicates. If $$m\ge n$$, then $$\mathrm{Tr}_m(k)$$ is false for all $$k$$. If $$mm$$. Then, it’s clear that $$T_0$$, and hence all $$T_m$$ (since $$T_0$$ is the strongest of the systems) is sound on $$M$$, and therefore consistent. Thus, we have proven in ZFC that if ZFC is inconsistent, then $$T_0$$ is consistent; or equivalently, that if $$T_0$$ is inconsistent, then ZFC is consistent. Stepping out of ZFC, we can see that if $$T_0$$ is inconsistent, then ZFC proves this, and therefore in this case ZFC proves its own consistency, implying that it is inconsistent. Hence, if ZFC is consistent, then so is $$T_0$$. (Moreover, we can formalize this reasoning in ZFC. Hence, we can prove in ZFC (i) that if ZFC is inconsistent, then $$T_0$$ is consistent, and (ii) that if ZFC is consistent, then $$T_0$$ is consistent. By the law of the excluded middle, ZFC proves that $$T_0$$ is consistent.)

 by Benja Fallenstein 1465 days ago | link We should be more careful, though, about what we mean by saying that $$\varphi(x)$$ only depends on $$\mathrm{Tr}_{m}$$ for $$m>n$$, though, since this cannot be a purely syntactic criterion if we allow quantification over the subscript (as I did here). I’m pretty sure that something can be worked out, but I’ll leave it for the moment. 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 Vanessa Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

I think that we should expect
 by Vanessa 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 Vanessa Kosoy on The Learning-Theoretic AI Alignment Research Agend... | 0 likes

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

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

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

Actually, I *am* including
 by Vanessa 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