# Are there any interesting examples of a formal system that can prove its own consistency?

Because of Godels 1st incompleteness theorem it will need to be weaker than PA (Peano Arithmatic), (or perhaps uncomparable to it?).

In fact it needs to be weaker than Robinsons Arithmatic which is Peano arithmatic without induction. The one example that I've found is Presburger Arithmatic which is PA minus multiplication (which means you cannot define primes in it!).

Are there any others?

-

There is a very closely related post on MathOverflow to this topic, which I was pointed to recently in the context of Gödel's Second Incompleteness theorem. The following is a paraphrase of a response there, and some of the comments to it.

Presburger arithmetic does not capture enough of arithmetic to prove its own consistency. Its only function symbols are addition and successor, which are not sufficient to represent Gödel encodings of propositions. However, there are axiom systems which are self-verifying, and which are consistent if and only if Peano Arithmetic is consistent. To do so, one must include enough arithmetic to make Gödel codings work (i.e. so that the system can encode a wide variety of recursive functions), but not enough to allow the incompleteness theorem to apply.

Such an axiom system is presented in Dan Willard's Self-Verifying Axiom Systems, the Incompleteness Theorem and Related Reflection Principles (disclaimer: I have not had the chance to read it yet), which replaces addition and multiplication with subtraction and division. This is just enough to allow the system to represent itself using arithmetic, but not enough to allow it to prove that multiplication is a total function, presumably because division and subtraction aren't total functions on the non-negative numbers. This would seem to prevent Gödel's Fixed Point theorem (c.f. the Stanford Encyclopedia's entry on Gödel, Theorem 2) from being provable about the theory:

Gödel's Fixed Point Theorem. If φ(x) is a formula of number theory, then there is a sentence ψ such that P ⊢ ψ ⇔ φ(⌈ψ⌉), where ⌈ψ⌉ denotes the numeral of the Gödel encoding of ψ.

As Gödel's incompleteness theorems both rely on this theorem, they do not apply to this particular self-asserting formal system.

-
Some clarifications: (1) the point about Willard's "Goedel through the looking glass" encoding, is that expressing addition needs not just subtraction but also an existential quantifier, so totality becomes a Pi-0-2 sentence that need not be true - essentially addition is a relation but not a function. As function symbols, subtraction and division are total functions. – Charles Stewart Jun 25 '13 at 14:23
And (2) without addition or multiplication as total functions, the encoding of substitution into variable positions of encoded formulae cannot be expressed as a total function (but we can express it as a relation), which is why the fixed point theorem can't be proven in Willard's theorem. – Charles Stewart Jun 25 '13 at 14:24
^ "in Willard's system". And yes, you should edit to correct the error that @CharlesStewart pointed out. – user21820 Nov 20 '15 at 7:47