# Dan Willard's self-verifying theories can escape Gödel's second incompleteness theorem. But can they escape the first?

I know that Willard's self-verifying theories can escape Gödel's second incompleteness theorem, so that they can be consistent and actually prove their own consistency. But I also heard that they can't escape Gödel's first incompleteness theorem, and so they can't be simultaneously consistent and complete (and computably axiomatizable).

But how is that to be understood? I am not familiar with Willard's proofs, but I know that for a common formal system F (non self-verifying), it is a theorem of F that Con(F) implies G(F). And since, in our particular case of self-verifying theories, F could prove Con(F), then it follows that F could also prove G(F). So I am not sure how Gödel's first incompleteness theorem would hold here.. Can someone explain to me that point?

Also, and with regard to computability, is the set of provable theorems of a self-verifying theory recursively enumerable but non recursive? (like the more common and stronger formal systems)

Thanks for feedback!

• See Dan Willard, Self-Verifying Axiom Systems and the Incompleteness Theorem: "We will study several weak axiom systems that use the Subtraction and Division primitives (rather than Addition and Multiplication) to formally encode the theorems of Arithmetic. Provided such axiom systems do not recognize Multiplication as a total function, we will show that it is feasible for them to verify their Semantic Tableaux, Herbrand, and Cut-Free consistencies". Commented May 5, 2023 at 6:24
• Thus, the "self-Justifying" axioms systems introduced by Willard are consistent but they cannot "express" all facts about arithmetic. Commented May 5, 2023 at 6:24
• @MauroALLEGRANZA would a self-verifiable theory then have a Gödel sentence? (a sentence it can express but not prove) Commented May 5, 2023 at 6:34

The first incompleteness theorem is extremely broadly applicable, and in particular it applies to Willard's systems. All you need for the construction and usual analysis of a theory $$T$$'s Godel-Rosser sentence $$G_T$$ (= "For every $$T$$-proof of me, there is a shorter $$T$$-disproof of me") is that $$T$$ be c.e., consistent, and $$\Sigma_1$$-complete; in particular, it does not need to prove that multiplication is total or anything similar.

There are other ways to prove GIT1 - see this MO thread - but for our purposes the classical approach is best.

To see why an "applicability gap" appears between GIT1 and GIT2, think about how we normally get GIT2 from GIT1 for a "reasonable" theory $$T$$. The point is that if $$T\vdash Con(T)$$ then we can reason inside $$T$$ as follows:

1. If $$\pi$$ were a $$T$$-disproof of $$G_T$$, then since $$T$$ is consistent there must be no $$T$$-proof of $$G_T$$. In particular, no string of symbols shorter than $$\pi$$ can be a $$T$$-proof of $$G_T$$.

2. We can then write a single proof $$\rho$$ which "searches through" all strings of symbols shorter than $$\pi$$ and verifies that none is a $$T$$-proof of $$G_T$$.

3. But this $$\rho$$, together with $$\pi$$, yields a proof of $$G_T$$ (this is where we use what $$G_T$$ actualy says - the rest of the argument makes no reference to the details of $$G_T$$). And so we have a contradiction.

Step $$2$$ does not go through if $$T$$ is one of Willard's theories! The reason is that $$\rho$$ is really long, and Willard's theories can't prove the totality results needed to show that $$\rho$$ actually exists if $$\pi$$ does.

• Thanks @NoahSchweber! So if GIT1 applies to Willard's theories as you described, is the Gödel sentence of such theories a $Π_1$ statement too (e.g., halting of Turing Machines, Diophantine Equations, ...)? I'm asking because I want to make sure whether they have a similar Gödel sentence as the standard theories. Also, since GIT1 applies and GIT2 does not, I assume that the following sentence Con(T) -> G(T) is not a theorem of Willard's theories? (unlike the standard theories) Commented Jan 10 at 5:41