nLab reflection principle

Idea

A reflection principle is roughly a statement or formula (scheme) that expresses the idea that a certain logical object contains copies of itself. They play an important role in different guises in several fields of mathematical logic e.g. in set theory, proof theory, type theory and, recently, constructive analysis.

Gödel’s encoding of an unprovability predicate into Peano arithmetic $PA$ can be viewed as an ‘anti-reflection’ principle for $PA$. Conversely, this suggests that the validity of reflection principles for some theory $T$ can be informally understood as expressing or approximating the (internal) consistency and completeness of $T$.

Set-theoretic reflection principles

A reflection principle in set theory states that it is possible to find sets that resemble the class of all sets that are constructed in some ways; in other words, any statement true of the universe $V$ already holds at some initial segment $V_\alpha$. This can be interpreted as saying that no first-order property can distinguish the set-theoretic universe from the extensions of all its member sets thereby suggesting the expansiveness or strong infinity of the universe: $V$ gets ‘arbitrarily large’.

The first reflection principles go back to R. Montague and A. Lévy around 1960. It emerged from their work that reflection principles can supplant the traditional axioms of Zermelo-Fraenkel set theory, e.g. the axiom of replacement (cf. Bell-Machover 1977, p.495). This capacity and the intuition that they express ‘completeness’ make them interesting candidates in the quest for new axioms of set theory (cf. Koellner 2009).

Universes in type theory

In type theory this principle is embodied by a type of types (Martin-Löf 74, p. 6).

Related entries

• universe

• Russell universe, Coquand universe

• cumulative hierarchy

• continuous truth

Related page

• Wikipedia, Reflection principle .

References

• John Lane Bell, M. Machover, A Course in Mathematical Logic, North-Holland Amsterdam 1977. (ch. 10,§5) (ISBN:9780720428445)

• M. P. Fourman, Continuous Truth II: Reflections , LNCS 8071 (2013) pp.153-167. (preprint)

• P. Koellner, On Reflection Principles , APAL 157 (2009) pp.209-219. (preprint)

• Georg Kreisel, Mathematical Logic , pp. 95-195 in Saaty (ed.) , Lectures on Modern Mathematics III , Wiley New York 1965.

• Georg Kreisel, A. Lévy, Reflection Principles and their Use for Establishing the Complexity of Axiomatic Systems, Mathematical Logic Quarterly 14 (7-12) pp.97–142, 1968.

• A. Lévy, Axiom Schemata of Strong Infinity in Axiomatic Set Theory , Pacific J. Math. 10 (1960) pp.223-238. (pdf)

• Per Martin-Löf, section 1.9, p. 7 of An intuitionistic theory of types: predicative part, In Logic Colloquium (1973), ed. H. E. Rose and J. C. Shepherdson (North-Holland, 1974), pp.73-118. (web)