HOME

TheInfoList



OR:

In
mathematical logic Mathematical logic is the study of formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of forma ...
, the disjunction and existence properties are the "hallmarks" of
constructive Although the general English usage of the adjective constructive is "helping to develop or improve something; helpful to someone, instead of upsetting and negative," as in the phrase "constructive criticism," in legal writing ''constructive'' has ...
theories such as
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano ar ...
and constructive set theories (Rathjen 2005).


Disjunction property

The disjunction property is satisfied by a theory if, whenever a sentence ''A'' ∨ ''B'' is a
theorem In mathematics, a theorem is a statement that has been proved, or can be proved. The ''proof'' of a theorem is a logical argument that uses the inference rules of a deductive system to establish that the theorem is a logical consequence of t ...
, then either ''A'' is a theorem, or ''B'' is a theorem.


Existence property

The existence property or witness property is satisfied by a theory if, whenever a sentence is a theorem, where ''A''(''x'') has no other free variables, then there is some
term Term may refer to: * Terminology, or term, a noun or compound word used in a specific context, in particular: **Technical term, part of the specialized vocabulary of a particular field, specifically: ***Scientific terminology, terms used by scient ...
''t'' such that the theory proves .


Related properties

Rathjen (2005) lists five properties that a theory may possess. These include the disjunction property (DP), the existence property (EP), and three additional properties: * The numerical existence property (NEP) states that if the theory proves (\exists x \in \mathbb)\varphi(x), where ''φ'' has no other free variables, then the theory proves \varphi(\bar) for some n \in \mathbb\text Here \bar is a term in T representing the number ''n''. * Church's rule (CR) states that if the theory proves (\forall x \in \mathbb)(\exists y \in \mathbb)\varphi(x,y) then there is a natural number ''e'' such that, letting f_e be the computable function with index ''e'', the theory proves (\forall x)\varphi(x,f_e(x)). * A variant of Church's rule, CR1, states that if the theory proves (\exists f \colon \mathbb\to\mathbb) \psi(f) then there is a natural number ''e'' such that the theory proves f_e is total and proves \psi(f_e). These properties can only be directly expressed for theories that have the ability to quantify over natural numbers and, for CR1, quantify over functions from \mathbb to \mathbb. In practice, one may say that a theory has one of these properties if a
definitional extension In mathematical logic, more specifically in the proof theory of first-order theories, extensions by definitions formalize the introduction of new symbols by means of a definition. For example, it is common in naive set theory to introduce a symbol ...
of the theory has the property stated above (Rathjen 2005).


Background and history

Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imm ...
 (1932) stated without proof that intuitionistic propositional logic (with no additional axioms) has the disjunction property; this result was proven and extended to intuitionistic predicate logic by
Gerhard Gentzen Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...
 (1934, 1935).
Stephen Cole Kleene Stephen Cole Kleene ( ; January 5, 1909 – January 25, 1994) was an American mathematician. One of the students of Alonzo Church, Kleene, along with Rózsa Péter, Alan Turing, Emil Post, and others, is best known as a founder of the branch of ...
 (1945) proved that
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano ar ...
has the disjunction property and the existence property. Kleene's method introduced the technique of
realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way ...
, which is now one of the main methods in the study of constructive theories (Kohlenbach 2008; Troelstra 1973). While the earliest results were for constructive theories of arithmetic, many results are also known for constructive set theories (Rathjen 2005).
John Myhill John R. Myhill Sr. (11 August 1923 – 15 February 1987) was a British mathematician. Education Myhill received his Ph.D. from Harvard University under Willard Van Orman Quine in 1949. He was professor at SUNY Buffalo from 1966 until his death ...
 (1973) showed that IZF with the
axiom of replacement In set theory, the axiom schema of replacement is a schema of axioms in Zermelo–Fraenkel set theory (ZF) that asserts that the image of any set under any definable mapping is also a set. It is necessary for the construction of certain infinite ...
eliminated in favor of the axiom of collection has the disjunction property, the numerical existence property, and the existence property. Michael Rathjen (2005) proved that CZF has the disjunction property and the numerical existence property. Most classical theories, such as
Peano arithmetic In mathematical logic, the Peano axioms, also known as the Dedekind–Peano axioms or the Peano postulates, are axioms for the natural numbers presented by the 19th century Italian mathematician Giuseppe Peano. These axioms have been used nearl ...
and ZFC do not have the existence or disjunction property. Some classical theories, such as ZFC plus the
axiom of constructibility The axiom of constructibility is a possible axiom for set theory in mathematics that asserts that every set is constructible. The axiom is usually written as ''V'' = ''L'', where ''V'' and ''L'' denote the von Neumann universe and the construc ...
, do have a weaker form of the existence property (Rathjen 2005).


In topoi

Freyd and Scedrov (1990) observed that the disjunction property holds in free
Heyting algebra In mathematics, a Heyting algebra (also known as pseudo-Boolean algebra) is a bounded lattice (with join and meet operations written ∨ and ∧ and with least element 0 and greatest element 1) equipped with a binary operation ''a'' → ''b'' of '' ...
s and free
topoi In mathematics, a topos (, ; plural topoi or , or toposes) is a category that behaves like the category of sheaves of sets on a topological space (or more generally: on a site). Topoi behave much like the category of sets and possess a noti ...
. In categorical terms, in the
free topos Free may refer to: Concept * Freedom, having the ability to do something, without having to obey anyone/anything * Freethought, a position that beliefs should be formed only on the basis of logic, reason, and empiricism * Emancipate, to procure ...
, that corresponds to the fact that the
terminal object In category theory, a branch of mathematics, an initial object of a category is an object in such that for every object in , there exists precisely one morphism . The dual notion is that of a terminal object (also called terminal element): ...
, \mathbf, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that \mathbf is an indecomposable
projective object In category theory, the notion of a projective object generalizes the notion of a projective module. Projective objects in abelian categories are used in homological algebra. The dual notion of a projective object is that of an injective object. ...
—the
functor In mathematics, specifically category theory, a functor is a mapping between categories. Functors were first considered in algebraic topology, where algebraic objects (such as the fundamental group) are associated to topological spaces, and m ...
it represents (the global-section functor) preserves
epimorphism In category theory, an epimorphism (also called an epic morphism or, colloquially, an epi) is a morphism ''f'' : ''X'' → ''Y'' that is right-cancellative in the sense that, for all objects ''Z'' and all morphisms , : g_1 \circ f = g_2 \circ f ...
s and
coproduct In category theory, the coproduct, or categorical sum, is a construction which includes as examples the disjoint union of sets and of topological spaces, the free product of groups, and the direct sum of modules and vector spaces. The coproduc ...
s.


Relationships

There are several relationship between the five properties discussed above. In the setting of arithmetic, the numerical existence property implies the disjunction property. The proof uses the fact that a disjunction can be rewritten as an existential formula quantifying over natural numbers: : A \vee B \equiv (\exists n) (n=0 \to A) \wedge (n \neq 0 \to B)/math>. Therefore, if : A \vee B is a theorem of T , so is \exists n\colon (n=0 \to A) \wedge (n \neq 0 \to B) . Thus, assuming the numerical existence property, there exists some s such that : (\bar=0 \to A) \wedge (\bar \neq 0 \to B) is a theorem. Since \bar{s} is a numeral, one may concretely check the value of s: if s=0 then A is a theorem and if s \neq 0 then B is a theorem.
Harvey Friedman __NOTOC__ Harvey Friedman (born 23 September 1948)Handbook of Philosophical Logic, , p. 38 is an American mathematical logician at Ohio State University in Columbus, Ohio. He has worked on reverse mathematics, a project intended to derive the axi ...
(1974) proved that in any
recursively enumerable In computability theory, a set ''S'' of natural numbers is called computably enumerable (c.e.), recursively enumerable (r.e.), semidecidable, partially decidable, listable, provable or Turing-recognizable if: *There is an algorithm such that the ...
extension of
intuitionistic arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano ...
, the disjunction property implies the numerical existence property. The proof uses self-referential sentences in way similar to the proof of
Gödel's incompleteness theorems Gödel's incompleteness theorems are two theorems of mathematical logic that are concerned with the limits of in formal axiomatic theories. These results, published by Kurt Gödel in 1931, are important both in mathematical logic and in the phil ...
. The key step is to find a bound on the existential quantifier in a formula (∃''x'')A(''x''), producing a bounded existential formula (∃''x''<''n'')A(''x''). The bounded formula may then be written as a finite disjunction A(1)∨A(2)∨...∨A(n). Finally,
disjunction elimination In propositional logic, disjunction elimination (sometimes named proof by cases, case analysis, or or elimination), is the valid argument form and rule of inference that allows one to eliminate a disjunctive statement from a logical proof. It ...
may be used to show that one of the disjuncts is provable.


See also

*
Constructive set theory Constructive set theory is an approach to mathematical constructivism following the program of axiomatic set theory. The same first-order language with "=" and "\in" of classical set theory is usually used, so this is not to be confused with a con ...
*
Heyting arithmetic In mathematical logic, Heyting arithmetic is an axiomatization of arithmetic in accordance with the philosophy of intuitionism.Troelstra 1973:18 It is named after Arend Heyting, who first proposed it. Axiomatization As with first-order Peano ar ...
*
Law of excluded middle In logic, the law of excluded middle (or the principle of excluded middle) states that for every proposition, either this proposition or its negation is true. It is one of the so-called three laws of thought, along with the law of noncontradi ...
*
Realizability In mathematical logic, realizability is a collection of methods in proof theory used to study constructive proofs and extract additional information from them. Formulas from a formal theory are "realized" by objects, known as "realizers", in a way ...
*
Existential quantifier In predicate logic, an existential quantification is a type of quantifier, a logical constant which is interpreted as "there exists", "there is at least one", or "for some". It is usually denoted by the logical operator symbol ∃, which, w ...


References

* Peter J. Freyd and Andre Scedrov, 1990, ''Categories, Allegories''. North-Holland. *
Harvey Friedman __NOTOC__ Harvey Friedman (born 23 September 1948)Handbook of Philosophical Logic, , p. 38 is an American mathematical logician at Ohio State University in Columbus, Ohio. He has worked on reverse mathematics, a project intended to derive the axi ...
, 1975, ''The disjunction property implies the numerical existence property'', State University of New York at Buffalo. *
Gerhard Gentzen Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...
, 1934, "Untersuchungen über das logische Schließen. I", ''Mathematische Zeitschrift'' v. 39 n. 2, pp. 176–210. *
Gerhard Gentzen Gerhard Karl Erich Gentzen (24 November 1909 – 4 August 1945) was a German mathematician and logician. He made major contributions to the foundations of mathematics, proof theory, especially on natural deduction and sequent calculus. He died ...
, 1935, "Untersuchungen über das logische Schließen. II", ''Mathematische Zeitschrift'' v. 39 n. 3, pp. 405–431. *
Kurt Gödel Kurt Friedrich Gödel ( , ; April 28, 1906 – January 14, 1978) was a logician, mathematician, and philosopher. Considered along with Aristotle and Gottlob Frege to be one of the most significant logicians in history, Gödel had an imm ...
, 1932, "Zum intuitionistischen Aussagenkalkül", ''Anzeiger der Akademie der Wissenschaftischen in Wien'', v. 69, pp. 65–66. * Stephen Cole Kleene, 1945, "On the interpretation of intuitionistic number theory," ''Journal of Symbolic Logic'', v. 10, pp. 109–124. *
Ulrich Kohlenbach Ulrich Wilhelm Kohlenbach (born 27 July 1962 in Frankfurt am Main) is a German mathematician and professor of algebra and logic at the Technische Universität Darmstadt. His research interests lie in the field of proof mining. Kohlenbach was pr ...
, 2008, ''Applied proof theory'', Springer. *
John Myhill John R. Myhill Sr. (11 August 1923 – 15 February 1987) was a British mathematician. Education Myhill received his Ph.D. from Harvard University under Willard Van Orman Quine in 1949. He was professor at SUNY Buffalo from 1966 until his death ...
, 1973, "Some properties of Intuitionistic Zermelo-Fraenkel set theory", in A. Mathias and H. Rogers, ''Cambridge Summer School in Mathematical Logic'', Lectures Notes in Mathematics v. 337, pp. 206–231, Springer. * Michael Rathjen, 2005,
The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory
, ''Journal of Symbolic Logic'', v. 70 n. 4, pp. 1233–1254. * Anne S. Troelstra, ed. (1973), ''Metamathematical investigation of intuitionistic arithmetic and analysis'', Springer.


External links


Intuitionistic Logic
by Joan Moschovakis,
Stanford Encyclopedia of Philosophy The ''Stanford Encyclopedia of Philosophy'' (''SEP'') combines an online encyclopedia of philosophy with peer-reviewed publication of original papers in philosophy, freely accessible to Internet users. It is maintained by Stanford University. E ...
Proof theory Constructivism (mathematics)