Disjunction and existence properties

<h2 id="definitions">Definitions</h2>
<ul><li>The disjunction property is satisfied by a theory if, whenever a <a href="/facts/Sentence_(mathematical_logic)/lnsLzvTx">sentence</a> A ∨ B is a <a href="/facts/Theorem/f2Pe1FMD">theorem</a>, then either A is a theorem, or B is a theorem.</li>
<li>The existence property or witness property is satisfied by a theory if, whenever a sentence (∃x)A(x) is a theorem, where A(x) has no other free variables, then there is some <a href="/facts/First-order_logic/lcISqWIg">term</a> t such that the theory proves A(t).</li></ul>
<h3>Related properties</h3>
Rathjen (2005) lists five properties that a theory may possess. These include the disjunction property (DP), the existence property (EP), and three additional properties:

<ul><li>The numerical existence property (NEP) states that if the theory proves 
 
 
 
 (
 ∃
 x
 ∈
 
 N
 
 )
 φ
 (
 x
 )
 
 
 {\displaystyle (\exists x\in \mathbb {N} )\varphi (x)}
 
, where φ has no other free variables, then the theory proves 
 
 
 
 φ
 (
 
 
 
 n
 ¯
 
 
 
 )
 
 
 {\displaystyle \varphi ({\bar {n}})}
 
 for some 
 
 
 
 n
 ∈
 
 N
 
 
 .
 
 
 
 {\displaystyle n\in \mathbb {N} {\text{.}}}
 
 Here 
 
 
 
 
 
 
 n
 ¯
 
 
 
 
 
 {\displaystyle {\bar {n}}}
 
 is a term in 
 
 
 
 T
 
 
 {\displaystyle T}
 
 representing the number n.</li>
<li><a href="/facts/Church%2527s_thesis_(constructive_mathematics)/XYp1WSCt">Church's rule</a> (CR) states that if the theory proves 
 
 
 
 (
 ∀
 x
 ∈
 
 N
 
 )
 (
 ∃
 y
 ∈
 
 N
 
 )
 φ
 (
 x
 ,
 y
 )
 
 
 {\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)}
 
 then there is a natural number e such that, letting 
 
 
 
 
 f
 
 e
 
 
 
 
 {\displaystyle f_{e}}
 
 be the computable function with index e, the theory proves 
 
 
 
 (
 ∀
 x
 )
 φ
 (
 x
 ,
 
 f
 
 e
 
 
 (
 x
 )
 )
 
 
 {\displaystyle (\forall x)\varphi (x,f_{e}(x))}
 
.</li>
<li>A variant of Church's rule, CR1, states that if the theory proves 
 
 
 
 (
 ∃
 f
 :
 
 N
 
 →
 
 N
 
 )
 ψ
 (
 f
 )
 
 
 {\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)}
 
 then there is a natural number e such that the theory proves 
 
 
 
 
 f
 
 e
 
 
 
 
 {\displaystyle f_{e}}
 
 is total and proves 
 
 
 
 ψ
 (
 
 f
 
 e
 
 
 )
 
 
 {\displaystyle \psi (f_{e})}
 
.</li></ul>
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 
 
 
 
 
 N
 
 
 
 {\displaystyle \mathbb {N} }
 
 to 
 
 
 
 
 N
 
 
 
 {\displaystyle \mathbb {N} }
 
. In practice, one may say that a theory has one of these properties if a <a href="/facts/Definitional_extension/f5w7X1l4">definitional extension</a> of the theory has the property stated above (Rathjen 2005).

<h2 id="results">Results</h2>
<h3>Non-examples and examples</h3>
Almost by definition, a theory that accepts <a href="/facts/Excluded_middle/tDhbugCN">excluded middle</a> while having independent statements does not have the disjunction property. So all classical theories expressing <a href="/facts/Robinson_arithmetic/FAFPDus0">Robinson arithmetic</a> do not have it. Most classical theories, such as <a href="/facts/Peano_arithmetic/DhhDnNug">Peano arithmetic</a> and <a href="/facts/Zermelo-Frankel_set_theory/UYIsPbXw">ZFC</a> in turn do not validate the existence property either, e.g. because they validate the <a href="/facts/Least_number_principle/5b52w9w3">least number principle</a> existence claim. But some classical theories, such as ZFC plus the <a href="/facts/Axiom_of_constructibility/9x9pTqq8">axiom of constructibility</a>, do have a weaker form of the existence property (Rathjen 2005).
<a href="/facts/Heyting_arithmetic/aBfjC0zg">Heyting arithmetic</a> is well known for having the disjunction property and the (numerical) existence property.
While the earliest results were for constructive theories of arithmetic, many results are also known for constructive set theories (Rathjen 2005). <a href="/facts/John_Myhill/Ct2fUk07">John Myhill</a> (1973) showed that <a href="/facts/IZF/myLo3Mjt">IZF</a> with the <a href="/facts/Axiom_of_replacement/dmJn0BaS">axiom of replacement</a> 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 <a href="/facts/CZF/myLo3Mjt">CZF</a> has the disjunction property and the numerical existence property.
<a href="/facts/Peter_J._Freyd/jbQAncXD">Freyd</a> and Scedrov (1990) observed that the disjunction property holds in free <a href="/facts/Heyting_algebra/Rrny2LRq">Heyting algebras</a> and free <a href="/facts/Topoi/zzttCIwC">topoi</a>. In <a href="/facts/Category_theory/6zS3DXPa">categorical terms</a>, in the free topos, that corresponds to the fact that the <a href="/facts/Terminal_object/oeckvXRj">terminal object</a>, 
 
 
 
 
 1
 
 
 
 {\displaystyle \mathbf {1} }
 
, is not the join of two proper subobjects. Together with the existence property it translates to the assertion that 
 
 
 
 
 1
 
 
 
 {\displaystyle \mathbf {1} }
 
 is an indecomposable <a href="/facts/Projective_object/sKWPFB6u">projective object</a>—the <a href="/facts/Functor/l2u3rIBE">functor</a> it represents (the global-section functor) preserves <a href="/facts/Epimorphism/IrzonI01">epimorphisms</a> and <a href="/facts/Coproduct/0bJ8SCdu">coproducts</a>.

<h3>Relationship between properties</h3>
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
 ∨
 B
 ≡
 (
 ∃
 n
 )
 [
 (
 n
 =
 0
 →
 A
 )
 ∧
 (
 n
 ≠
 0
 →
 B
 )
 ]
 
 
 {\displaystyle A\vee B\equiv (\exists n)[(n=0\to A)\wedge (n\neq 0\to B)]}
 
.
Therefore, if

A
 ∨
 B
 
 
 {\displaystyle A\vee B}
 
 is a theorem of 
 
 
 
 T
 
 
 {\displaystyle T}
 
, so is 
 
 
 
 ∃
 n
 :
 (
 n
 =
 0
 →
 A
 )
 ∧
 (
 n
 ≠
 0
 →
 B
 )
 
 
 {\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}
 
.
Thus, assuming the numerical existence property, there exists some 
 
 
 
 s
 
 
 {\displaystyle s}
 
 such that

(
        
          
            
              s
              ¯
            
          
        
        =
        0
        →
        A
        )
        ∧
        (
        
          
            
              s
              ¯
            
          
        
        ≠
        0
        →
        B
        )
      
    
    {\displaystyle ({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)}

is a theorem. Since 
 
 
 
 
 
 
 s
 ¯
 
 
 
 
 
 {\displaystyle {\bar {s}}}
 
 is a numeral, one may concretely check the value of 
 
 
 
 s
 
 
 {\displaystyle s}
 
: if 
 
 
 
 s
 =
 0
 
 
 {\displaystyle s=0}
 
 then 
 
 
 
 A
 
 
 {\displaystyle A}
 
 is a theorem and if 
 
 
 
 s
 ≠
 0
 
 
 {\displaystyle s\neq 0}
 
 then 
 
 
 
 B
 
 
 {\displaystyle B}
 
 is a theorem.
<a href="/facts/Harvey_Friedman_(mathematician)/Yq10dMrt">Harvey Friedman</a> (1974) proved that in any <a href="/facts/Recursively_enumerable_set/lpzr8jHn">recursively enumerable</a> extension of <a href="/facts/Intuitionistic_arithmetic/aBfjC0zg">intuitionistic arithmetic</a>, the disjunction property implies the numerical existence property. The proof uses self-referential sentences in way similar to the proof of <a href="/facts/G%25C3%25B6del%2527s_incompleteness_theorems/du8PRu8g">Gödel's incompleteness theorems</a>. The key step is to find a bound on the existential quantifier in a formula (∃x)A(x), producing a <a href="/facts/Bounded_quantifier/Q0Y7aTkG">bounded existential formula</a>
(∃x<n)A(x). The bounded formula may then be written as a finite disjunction A(1)∨A(2)∨...∨A(n). Finally, <a href="/facts/Disjunction_elimination/vode1DSs">disjunction elimination</a> may be used to show that one of the disjuncts is provable.

<h2 id="history">History</h2>
<a href="/facts/Kurt_G%25C3%25B6del/P14DqKqK">Kurt Gödel</a> (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 <a href="/facts/Gerhard_Gentzen/9ujN0ssI">Gerhard Gentzen</a> (1934, 1935). <a href="/facts/Stephen_Cole_Kleene/sKSax2se">Stephen Cole Kleene</a> (1945) proved that Heyting arithmetic has the disjunction property and the existence property. Kleene's method introduced the technique of <a href="/facts/Realizability/nheEHzf9">realizability</a>, which is now one of the main methods in the study of constructive theories (Kohlenbach 2008; Troelstra 1973).

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Constructive_set_theory/myLo3Mjt">Constructive set theory</a></li>
<li><a href="/facts/Heyting_arithmetic/aBfjC0zg">Heyting arithmetic</a></li>
<li><a href="/facts/Law_of_excluded_middle/tDhbugCN">Law of excluded middle</a></li>
<li><a href="/facts/Realizability/nheEHzf9">Realizability</a></li>
<li><a href="/facts/Existential_quantifier/hHveaBYo">Existential quantifier</a></li></ul>

<ul><li>Peter J. Freyd and Andre Scedrov, 1990, Categories, Allegories. North-Holland.</li>
<li><a href="/facts/Harvey_Friedman_(mathematician)/Yq10dMrt">Harvey Friedman</a>, 1975, The disjunction property implies the numerical existence property, State University of New York at Buffalo.</li>
<li><a href="/facts/Gerhard_Gentzen/9ujN0ssI">Gerhard Gentzen</a>, 1934, "Untersuchungen über das logische Schließen. I", Mathematische Zeitschrift v. 39 n. 2, pp. 176–210.</li>
<li><a href="/facts/Gerhard_Gentzen/9ujN0ssI">Gerhard Gentzen</a>, 1935, "Untersuchungen über das logische Schließen. II", Mathematische Zeitschrift v. 39 n. 3, pp. 405–431.</li>
<li><a href="/facts/Kurt_G%25C3%25B6del/P14DqKqK">Kurt Gödel</a>, 1932, "Zum intuitionistischen Aussagenkalkül", Anzeiger der Akademie der Wissenschaftischen in Wien, v. 69, pp. 65–66.</li>
<li>Stephen Cole Kleene, 1945, "On the interpretation of intuitionistic number theory," Journal of Symbolic Logic, v. 10, pp. 109–124.</li>
<li><a href="/facts/Ulrich_Kohlenbach/v1sbHgsb">Ulrich Kohlenbach</a>, 2008, Applied proof theory, Springer.</li>
<li><a href="/facts/John_Myhill/Ct2fUk07">John Myhill</a>, 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.</li>
<li>Michael Rathjen, 2005, "<a href="https://www.jstor.org/stable/27588423">The Disjunction and Related Properties for Constructive Zermelo-Fraenkel Set Theory</a>", Journal of Symbolic Logic, v. 70 n. 4, pp. 1233–1254.</li>
<li><a href="/facts/Anne_S._Troelstra/94dULETx">Anne S. Troelstra</a>, ed. (1973), Metamathematical investigation of intuitionistic arithmetic and analysis, Springer.</li></ul>
<h2 id="external-links">External links</h2>
<ul><li>Moschovakis, Joan (16 December 2022). <a href="https://plato.stanford.edu/entries/logic-intuitionistic/">"Intuitionistic Logic"</a>. In <a href="/facts/Edward_N._Zalta/U8JxHaaA">Zalta, Edward N.</a> (ed.). <a href="/facts/Stanford_Encyclopedia_of_Philosophy/LDuL5HW4">Stanford Encyclopedia of Philosophy</a>.</li></ul>

Disjunction and existence properties open-in-new

Disjunction and existence properties