词条 | Disjunction and existence properties |
释义 |
In mathematical logic, the disjunction and existence properties are the "hallmarks" of constructive theories such as Heyting arithmetic and constructive set theories (Rathjen 2005). Disjunction propertyThe disjunction property is satisfied by a theory if, whenever a sentence A ∨ B is a theorem, then either A is a theorem, or B is a theorem. Existence propertyThe existence property or witness property is satisfied by a theory if, whenever a sentence {{nowrap|1=(∃x)A(x)}} is a theorem, where A(x) has no other free variables, then there is some term t such that the theory proves {{nowrap|1=A(t)}}. Related propertiesRathjen (2005) lists five properties that a theory may possess. These include the disjunction property (DP), the existence property (EP), and three additional properties:
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 to . In practice, one may say that a theory has one of these properties if a definitional extension of the theory has the property stated above (Rathjen 2005). Background and historyKurt Gödel (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 (1934, 1935). Stephen Cole Kleene (1945) proved that Heyting arithmetic has the disjunction property and the existence property. Kleene's method introduced the technique of realizability, 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 (1973) showed that IZF with the axiom of Replacement 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 and ZFC do not have the existence or disjunction property. Some classical theories, such as ZFC plus the axiom of constructibility, do have a weaker form of the existence property (Rathjen 2005). In topoiFreyd and Scedrov (1990) observed that the disjunction property holds in free Heyting algebras and free topoi. In categorical terms, in the free topos, that corresponds to the fact that the terminal object, , 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 (the global-section functor) preserves epimorphisms and coproducts. RelationshipsThere 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: . Therefore, if is a theorem of , so is . Thus, assuming the numerical existence property, there exists some such that is a theorem. Since is a numeral, one may concretely check the value of : if then is a theorem and if then is a theorem. Harvey Friedman (1974) proved that in any recursively enumerable extension of intuitionistic arithmetic, 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. The key step is to find a bound on the existential quantifier in a formula (∃x)A(x), producing a because 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 may be used to show that one of the disjuncts is provable. References
External links
2 : Proof theory|Constructivism (mathematics) |
随便看 |
|
开放百科全书收录14589846条英语、德语、日语等多语种百科知识,基本涵盖了大多数领域的百科知识,是一部内容自由、开放的电子版国际百科全书。