+-- {: .rightHandSide} +-- {: .toc .clickDown tabindex="0"} ### Context #### Universes +-- {: .hide} [[!include universe - contents]] =-- #### Foundations +-- {: .hide} [[!include foundations - contents]] =-- =-- =-- #Contents# * table of contents {:toc} ## 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 [[Richard Montague|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](#BellMach77), 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](#Koell09)). ### Universes in type theory In [[type theory]] this principle is embodied by a [[type of types]] ([Martin-Löf 74, p. 6](#MartinLoef74)). ## Related entries * [[universe]] * [[Russell universe]], [[Coquand universe]] * [[cumulative hierarchy]] * [[continuous truth]] ## Related page * Wikipedia, _[Reflection principle](http://en.wikipedia.org/wiki/Reflection_principle)_ . ## References * {#BellMach77} [[John Lane Bell]], M. Machover, _A Course in Mathematical Logic_, North-Holland Amsterdam 1977. (ch. 10,§5) ([ISBN:9780720428445](https://www.elsevier.com/books/a-course-in-mathematical-logic/bell/978-0-7204-2844-5)) * [[Michael Fourman|M. P. Fourman]], _Continuous Truth II: Reflections_ , LNCS **8071** (2013) pp.153-167. ([preprint](http://homepages.inf.ed.ac.uk/mfourman/research/publications/pdf/fourman2013-continuous-truth-II.pdf)) * {#Koell09}P. Koellner, _On Reflection Principles_ , APAL **157** (2009) pp.209-219. ([preprint](http://logic.harvard.edu/koellner/ORP_final.pdf)) * [[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](http://projecteuclid.org/download/pdf_1/euclid.pjm/1103038638)) * {#MartinLoef74} [[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](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.131.926))