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!
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:
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$.
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$.
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.