Self-verifying axiom systems, the incompleteness theorem and related reflection principles (Q2747704)

In the paper several weak axiom systems that use the subtraction and division primitives (rather than addition and multiplication) to formally encode the theorems of arithmetic are studied. It is shown that under appropriate assumptions it is feasible for such systems to verify their semantic tableaux, Herbrand, and cut-free consistencies and that they are capable of recognizing the consistency of their Hilbert-style deductive proofs as well as some forms of the reflection principle.