Background
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, whose disjunction is true, we want to have an explicit value of the index such that we have a proof of that particular . 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, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that is an indecomposable projective object – the functor it represents (i.e., the global-section functor) preserves epis and coproducts (Freyd and Scedrov 1990).
Read more about this topic: Disjunction And Existence Properties
Famous quotes containing the word background:
“They were more than hostile. In the first place, I was a south Georgian and I was looked upon as a fiscal conservative, and the Atlanta newspapers quite erroneously, because they didn’t know anything about me or my background here in Plains, decided that I was also a racial conservative.”
—Jimmy Carter (James Earl Carter, Jr.)
“... every experience in life enriches one’s background and should teach valuable lessons.”
—Mary Barnett Gilson (1877–?)
“Silence is the universal refuge, the sequel to all dull discourses and all foolish acts, a balm to our every chagrin, as welcome after satiety as after disappointment; that background which the painter may not daub, be he master or bungler, and which, however awkward a figure we may have made in the foreground, remains ever our inviolable asylum, where no indignity can assail, no personality can disturb us.”
—Henry David Thoreau (1817–1862)