[FOM] Zahidi's question on consistency

[Curtis Franks]

Karim Zahidi asked if there are any formal systems that prove their own 
consistency, presumably intending consistent such theories.

This question came up on this list in the Spring of 2005. The answers 
proposed then involved reformulations either of the theory's own 
representation of its own axioms or of the provability predicate used.

Michael Detlefsen mentioned a weak extension of Robinson Arithmetic and 
the self-consistency proof Jeroslow gave for that theory in Fundamenta 
Mathematica 72 (1971). Andrew Boucher (in his June 1 2005 post) 
mentioned his own self-consistency proof for a subsystem of second order 
arithmetic. I mentioned some similar results. The discussion then was 
sensitive to the following question: Since these examples all seem 
somewhat contrived, which representations of a system's consistency are 
"intensionally adequate?" This question was first raised by Georg 
Kreisel and first studied systematically by Solomon Feferman.

Curtis