# Are there alternative formalizations of consistency that bypass the Second Incompleteness Theorem?

Gödel's Second Incompleteness Theorem expresses the consistency of a formal system within the system itself using a rather carefully designed proof checking predicate. The conclusion of Gödel's argument is that this formalization of consistency can't be proven in the system.

But what about other proof checking predicates? There's presumably an infinite variety of predicates which correctly check proofs. Any of which could be used to express consistency. But Gödel's argument no longer seems to apply to all of these predicates. After all, Gödel had to reason quite significantly about the internal operations of his predicate. But here the predicates are effectively black boxes.

Is it conceivable that one could prove the consistency of the system using such an alternative proof checking predicate? (Obviously it wouldn't be possible to prove that these formalizations of consistency are equivalent within the system.)

• I do not quite get what exactly you ask. Do you want to know whether there is a system "outside" which can prove the consistency of a given system ? – Peter Feb 13 at 21:21
• What is your definition of consistency? – Alberto Takase Feb 13 at 21:33
• I'm asking whether the Second Incompleteness Theorem applies to every predicate $P$ with the property "The sentence $S$ is provable $\iff \exists p: P(\langle S \rangle, p)$" where $\langle S \rangle$ is the Gödel number of $S$. Gödel's argument seems to only apply if one focuses on a very particular such predicate. – Sebastian Oberhoff Feb 13 at 21:35
• My definition of consistency is, given a predicate $P$ with the above property: $\forall s: (\exists p: P(s, p) \implies \neg \exists p: P($not$(s), p))$ (where "not" performs negation on Gödel numbers). – Sebastian Oberhoff Feb 13 at 21:39

Fix an appropriate theory $$T$$ we're interested in (like PA). Ignoring Godel numbering issues for simplicity, consider the predicate $$P_T(S,\pi)\equiv\mbox{ \pi is a T-proof of S shorter than any T-proof of \neg S}.$$ As long as $$T$$ is consistent, $$P_T$$ is indeed a proof predicate in the sense you give. Meanwhile, the corresponding consistency principle as you've defined it is trivially true, the point being that even if both $$S$$ and $$\neg S$$ are provable, one of them has to have a proof shorter than any proof of the other.
So with this broad a notion of proof predicate and consistency principle, the answer to your question is yes - however, I think the real takeaway is that the conditions you've written down don't successfully capture what you want them to. In particular, note that any system $$T$$ is consistent in the sense of the corresponding $$P_T$$. For example, PA proves "PA is $$P_{PA}$$-consistent," and (assuming PA is indeed consistent) $$P_{PA}$$ is an appropriate proof predicate. But this clearly is silly.