Disjunction and Existence Properties - Background

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:

    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)

    In the true sense one’s native land, with its background of tradition, early impressions, reminiscences and other things dear to one, is not enough to make sensitive human beings feel at home.
    Emma Goldman (1869–1940)

    I had many problems in my conduct of the office being contrasted with President Kennedy’s conduct in the office, with my manner of dealing with things and his manner, with my accent and his accent, with my background and his background. He was a great public hero, and anything I did that someone didn’t approve of, they would always feel that President Kennedy wouldn’t have done that.
    Lyndon Baines Johnson (1908–1973)