Disjunction and existence properties

From Wikipedia, the free encyclopedia

In mathematical logic, the disjunction property is satisfied by a logic if whenever a sentence

\phi\vee\psi

is a theorem, then either φ is a theorem, or ψ is a theorem.

The existence property is satisfied by a logic if whenever a sentence

\exists x\colon \phi(x)

is a theorem, then there is some term t for which φ(t) is a theorem.

The disjunction and existence properties are validated by intuitionistic logic and invalid for classical logic; they are key criteria used in assessing whether a logic is constructive. In particular, the existence property is fundamental to understanding in what sense proofs can be considered to have content: the essence of the discussion of existence theorems. The disjunction property is a finitary analogue, in an evident sense. Namely given two or finitely many propositions φi, whose disjunction is true, we want to have an explicit value of the index i such that we have a proof of that particular φi. There are quite concrete examples in number theory where this has a major effect.

Peter Freyd observed that it is a (meta)theorem that in free Heyting algebras and free topoi (and all sorts of variations thereon) that the disjunction property holds. In categorical terms, in the free topos, that translates to the statement that the terminator, \mathbf{1}, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that \mathbf{1} is an indecomposable projective object – the functor it represents (i.e., the global-section functor) preserves epis and coproducts (Freyd and Scedrov 1990).

[edit] References

  • P. Freyd and A. Scedrov, 1990. Categories, Allegories. North Holland.