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

Question

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?

Answer 1

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.