選言と存在の性質

数理論理学では、選言と存在の特性は、ヘイティング算術や構成的集合論などの構成的理論の「特徴」です(Rathjen 2005)。

• 文A ∨ Bが定理 である場合、常にAが定理であるか、またはBが定理である場合、理論は選言特性を満たします。
• 存在特性または証拠特性が理論によって満たされるのは、文(∃ x ) A ( x )が定理であり、A ( x ) が他の自由変数を持たない場合、理論がA ( t )を証明する何らかの項 tが存在する場合です。

Rathjen (2005) は、理論が持つ可能性のある 5 つの特性を挙げています。これには、選言特性 ( DP )、存在特性 ( EP )、および 3 つの追加特性が含まれます。

• 数値的存在性 (NEP) は、φに他の自由変数がない場合に、理論が を証明すると、ある に対してが証明されると述べています。ここでは、数nを表す項が使用されています。${\displaystyle (\exists x\in \mathbb {N} )\varphi (x)}$${\displaystyle \varphi ({\bar {n}})}$${\displaystyle n\in \mathbb {N} {\text{.}}}$${\displaystyle {\bar {n}}}$${\displaystyle T}$
• チャーチの法則(CR) は、理論が を証明する場合、 をインデックスeを持つ計算可能な関数とすると、理論が を証明する自然数eが存在すること。${\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)}$${\displaystyle f_{e}}$${\displaystyle (\forall x)\varphi (x,f_{e}(x))}$
• チャーチの法則の変形であるCR ₁は、理論が を証明する場合、理論がが完全であり を証明するような自然数eが存在すると述べています。${\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)}$${\displaystyle f_{e}}$${\displaystyle \psi (f_{e})}$

これらの特性は、自然数に対して量化能力を持ち、CR ₁に対して からへの関数に対して量化能力を持つ理論に対してのみ直接表現できます。実際には、理論の定義拡張が上記の性質を持つ場合、理論はこれらの特性の 1 つを持つと言えます(Rathjen 2005)。 ${\displaystyle \mathbb {N} }$${\displaystyle \mathbb {N} }$

ほぼ定義により、排中律を受け入れながら独立な命題を持つ理論は、選言特性を持たない。したがって、ロビンソン算術を表現するすべての古典的理論は、この特性を持たない。ペアノ算術やZFCなどのほとんどの古典的理論は、最小数原理の存在主張を検証するなど、存在特性も検証しない。しかし、ZFC と構成可能性公理を組み合わせたものなど、一部の古典的理論は、存在特性の弱い形式を持つ (Rathjen 2005)。

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

最も初期の結果は算術の構成理論に関するものでしたが、構成集合論に関する結果も数多く知られています (Rathjen 2005)。John Myhill  (1973)は、置換公理をなくして収集公理を採用したIZFには、選言特性、数値存在特性、および存在特性があることを示しました。Michael Rathjen (2005) は、 CZF には選言特性と数値存在特性がある ことを証明しました。

Freydと Scedrov (1990) は、自由Heyting 代数と自由トポスで選言特性が成り立つことを観察しました。自由トポスにおけるカテゴリカルな用語で言えば、これは終端オブジェクトが2 つの適切なサブオブジェクトの結合ではないという事実に対応します。 存在特性と合わせて、これは分解不可能な射影オブジェクトである、つまりそれが表す関数(大域セクション関数) がエピモーフィズムと余積を保存するという主張に変換されます。 ${\displaystyle \mathbf {1} }$${\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}$${\displaystyle s\neq 0}$${\displaystyle B}$

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

クルト・ゲーデル (1932) は、証明なしに直観主義命題論理 (追加の公理なし) には選言特性があると述べた。この結果はゲルハルト・ゲンツェン (1934、1935) によって証明され、直観主義述語論理に拡張された。スティーブン・コール・クリーネ(1945) は、ハイティング算術には選言特性と存在特性があることを証明した。クリーネの方法論は実現可能性 の手法を導入し、これは現在では構成理論の研究における主要な方法の 1 つとなっている (Kohlenbach 2008; Troelstra 1973)。

• 構成的集合論
• ヘイティング算術
• 排中律
• 実現可能性
• 存在量指定子

• Peter J. Freyd と Andre Scedrov、1990 年、「Categories, Allegories」、North-Holland。
• Harvey Friedman、1975 年、「選言特性は数値存在特性を意味する」、ニューヨーク州立大学バッファロー校。
• ゲルハルト ゲンツェン、 1934 年、「Untersuhungen über das logische Schließen. I」、Mathematische Zeitschrift v. 39 n. 2、176–210ページ。
• ゲルハルト ゲンツェン、1935 年、「Untersuhungen über das logische Schließen. II」、Mathematische Zeitschrift v. 39 n. 3、405–431ページ。
• Kurt Gödel、1932 年、「Zum intuitionistischen Aussagenkalkül」、ウィーンのAnzeiger der Akademie der Wissenschaftischen、v. 69、65 ～ 66 ページ。
• スティーブン・コール・クリーネ、1945 年、「直観主義的数論の解釈について」、Journal of Symbolic Logic、v. 10、pp. 109-124。
• Ulrich Kohlenbach、2008 年、「応用証明理論」、Springer。
• John Myhill、1973、「直観主義ツェルメロ-フランケル集合論のいくつかの特性」、A. Mathias および H. Rogers 著、Cambridge Summer School in Mathematical Logic、Lectures Notes in Mathematics v. 337、pp. 206-231、Springer。
• Michael Rathjen、2005、「構成的ツェルメロ-フランケル集合論の選言と関連特性」、Journal of Symbolic Logic、v. 70 n. 4、pp. 1233–1254。
• Anne S. Troelstra編 (1973)、『直観主義算術および解析のメタ数学的調査』、Springer。

• モスコヴァキス、ジョアン（2022年12月16日）。「直観主義論理」。ザルタ、エドワードN.（編）スタンフォード哲学百科事典。