選言と存在特性

ラートジェン （2005）は、理論が持ちうる5つの特性を挙げている。これらには、選言特性（DP）、存在特性（EP）、および3つの追加特性が含まれる。

• 数値存在性（NEP）は、理論が証明すれば${\displaystyle (\exists x\in \mathbb {N} )\varphi (x)}$φに他の自由変数がない場合、理論は以下を証明する。${\displaystyle \varphi ({\bar {n}})}$一部の人にとって${\displaystyle n\in \mathbb {N} {\text{.}}}$ここ${\displaystyle {\bar {n}}}$は用語です${\displaystyle T}$nという数を表す。
• チャーチの規則（ CR）は、理論が証明すれば${\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)}$すると、自然数eが存在し、${\displaystyle f_{e}}$指数eを持つ計算可能な関数とすると、理論は次のように証明する。${\displaystyle (\forall x)\varphi (x,f_{e}(x))}$。
• チャーチの規則の変形であるCR ₁は、理論が証明すれば${\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)}$すると、理論が証明するような自然数eが存在する。${\displaystyle f_{e}}$完全であり証明する$\displaystyle \psi (f_{e})$。

これらの性質は、自然数に対して定量化できる理論、および CR ₁の場合、関数に対して定量化できる理論に対してのみ直接表現できます。${\displaystyle \mathbb {N} }$に${\displaystyle \mathbb {N} }$実際には、理論の定義的拡張が上記の特性を持つ場合、その理論はこれらの特性のいずれかを持つと言える（Rathjen  2005）。

定義上、排中律を許容しつつ独立命題を持つ理論は、選言性質を持たない。したがって、ロビンソン算術を表現する古典理論はすべて選言性質を持たない。ペアノ算術やZFCなどの古典理論のほとんどは、最小数原理の存在主張を検証するため、存在性質も検証しない。しかし、ZFCに構成可能性の公理を加えたような古典理論の中には、より弱い形式の存在性質を持つものもある（Rathjen  2005）。

ハイティング算術は、選言の性質と（数値的な）存在の性質を持つことでよく知られている。

初期の成果は算術の構成理論に関するものでしたが、構成的集合論に関する成果も数多く知られています（Rathjen 2005）。John Myhill （1973）は、集合公理を置換公理に置き換えたIZFが、選言性質、数的存在性質、および存在性質を持つこと を示しました。Michael Rathjen（2005）は、 CZFが選言性質と数的存在性質を持つことを証明しました。 

フレイドとスセドロフ（1990）は、自由ヘイティング代数と自由トポス において選言性質が成り立つことを観察した。圏論的に言えば、自由トポスにおいて、それは終端対象、${\displaystyle \mathbf {1} }$は、2 つの適切なサブオブジェクトの結合ではありません。存在プロパティと組み合わせると、次の主張になります。${\displaystyle \mathbf {1} }$は分解不可能な射影オブジェクトであり、それが表すファンクター（グローバルセクションファンクター）は全射準同型と余積を保存します。

上記で述べた5つの特性の間には、いくつかの関連性がある。

算術の枠組みでは、数値存在性は選言性を意味する。証明では、選言は自然数上の量化を表す存在式として書き換えることができるという事実を用いる。

${\displaystyle A\vee B\equiv (\exists n)[(n=0\to A)\wedge (n\neq 0\to B)]}$。

したがって、もし

${\displaystyle A\vee B}$は定理である${\displaystyle T}$なので${\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}$。

したがって、数値存在特性を仮定すると、${\displaystyle s}$そのため

${\displaystyle ({\bar {s}}=0\to A)\wedge ({\bar {s}}\neq 0\to B)}$

これは定理です。${\displaystyle {\bar {s}}}$は数値なので、具体的にその値を確認できます。${\displaystyle s}$： もし${\displaystyle s=0}$それから${\displaystyle A}$これは定理であり、もし$s ≠ 0$それから${\displaystyle B}$これは定理である。

ハーヴェイ・フリードマン（1974）は、直観主義算術の任意の再帰的に列挙可能な拡張において、選言の性質が数値存在性を意味することを証明した。この証明は、ゲーデルの不完全性定理の証明と同様の方法で自己参照文を使用する。重要なステップは、式 (∃ x )A( x )における存在量化子の境界を見つけ、有界存在式 (∃ x < n )A( x ) を生成することである。有界式は、有限選言 A(1) ∨ A(2) ∨ ... ∨ A(n)として記述できる。最後に、選言消去法を用いて、選言のうちの 1 つが証明可能であることを示すことができる。