Consistent theories that proves their own consistence

Question

Restrict the whole question to first order logic only. Gödel second incompleteness theorem tell us that, if, for example, we are working with Peano language, every T (recursively axiomatized, consistent) extension of PA is unable to prove Con(T). But the expressive power offered by PA deprived of the induction scheme (sometimes called the Tarski-Robinson arithmetic Q) is however enough to code the syntax and so to formulate the sentence Con(Q). At this point my question is: is there any (recursively axiomatized, consistent) theory between Q and PA capable of prove its own consistence?

Answer 1

In Robinson arithmetic $Q$ you can formulate the sentence $Con(Q)$ stating that $Q$ is coherent, but you cannot prove it, because Gödel's second incompleteness theorem also holds for $Q$: no consistent recursively axiomatized extension of $Q$ can prove its own consistency.

Actually, there exist self-verifying theories that are consistent first-order systems of arithmetic much weaker than $\textit{PA}$ (Peano arithmetic) and even $Q$, but that are capable of proving their own consistency. Dan Willard was the first to investigate their properties, and he has described a family of such systems. His idea is to formalise enough of the Gödel machinery to talk about provability internally without being able to formalise diagonalisation, to prevent Gödel's incompleteness theorems from applying to such formal systems.