[FOM] Zahidi's question on consistency
cfranks at nd.edu
Mon Nov 6 16:55:04 EST 2006
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.
More information about the FOM