nLab
reflection principle

Context

Universes

Foundations

Contents

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 PAPA can be viewed as an ‘anti-reflection’ principle for PAPA. This conversely suggests to understand the validity of reflection principles for some theory TT informally as expressing or approximating the (internal) consistency and completeness of TT.

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 VV already holds at some intial segment V α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: VV 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).

References

  • J. L. Bell, M. Machover, A Course in Mathematical Logic , North-Holland Amsterdam 1977. (ch. 10,§5)

  • 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)

Revised on August 2, 2015 15:07:18 by Thomas Holder (89.204.137.14)