Are there any simple explicit examples of formal systems which prove their own consistency?

Godel's first incompleteness theorem states roughly that you can't write down a finite list of axioms that can decide all statements about arithmetic: any such formal system is incomplete. I feel like I have a pretty good understanding of what this means concretely, but that's because there are concrete examples of formal systems that are complete.

Godel's second incompleteness theorem states that no formal system that can talk about arithmetic can prove its own consistency. I don't really appreciate this one as much on a gut level because I sort of feel like, well, duh - how could any formal system possibly prove its own consistency? Of course I know about Godel numbering and what not, but still, what I'd really like is an explicit example of a simple formal system, with a proof in that system of the system's own consistency. Does such a thing exist?

• See wikipedia on "self-verifying theories." Dan Willard has done a lot of research on this, and on trying to figure out sharp limits on how powerful a theory can be before running into the second incompleteness theorem. These theories have just enough arithmetic to talk about Godel numbers and provability internally without being able to perform the diagonalization. These theories are to an extent "not natural" and are specifically made for this purpose. – penguin_surprise Sep 14 '18 at 8:26
• An inconsistent system will easily prove its own consistency (as well as everything else), so take PA and add the axiom $1=0$. – Henning Makholm Sep 14 '18 at 8:37
• Presburg-Arithmetic is known to be consistent, but I do not know whether it can prove its own consistency. – Peter Sep 14 '18 at 8:38
• @HenningMakholm Let's say we're looking for systems with consistency proofs which we're inclined philosophically to actually believe. Maybe only systems that have an explicit model? – Jack M Sep 14 '18 at 8:39
• @JackM: You could use the diagonalization lemma to produce an arithmetic sentence saying "The theory that has me as its only axiom is consistent". Then take that sentence as the only axiom of a theory. Since the theory doesn't have any of the usual axioms that restrict how the $+$ and $\times$ symbols can behave, it will most likely be a simple task to produce a finite model for it -- but the details will depend on exactly how you've chosen to formalize statements about provability and consistency. – Henning Makholm Sep 14 '18 at 8:49