Iterated Reflection

Iterated reflection is a procedure in proof theory whereby a formal system is strengthened by adding, as a new axiom, a statement that the original system cannot derive: typically a consistency statement or a reflection principle asserting that everything provable in the original system is true. This process can then be repeated — the extended system is itself strengthened by adding its own consistency — and the iteration can be continued transfinitely through ordinal-indexed sequences of stronger and stronger systems.

The procedure is directly connected to Gödel's second incompleteness theorem, which shows that no sufficiently expressive formal system can prove its own consistency. Iterated reflection is the systematic response to this limitation: rather than proving consistency from within, one adds consistency from without, and then asks how far this process can be extended. The answer — measured by the proof-theoretic ordinal of the resulting system — is the central object of study in ordinal analysis.

Iterated reflection dissolves the apparent asymmetry in the Penrose-Lucas Argument: both human mathematicians and machine theorem provers can perform iterated reflection, each recognizing that a consistent system cannot prove its own consistency and adding the consistency statement as a new axiom. The process is equally mechanical and equally open-ended for both.