選言と存在特性

数理論理学において、選言と存在性は、ハイティング算術や構成的集合論（Rathjen 2005） などの構成的理論の「特徴」です。

定義

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

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

  • 数値的存在性質 (NEP)は、理論が（ただしφに他の自由変数がない場合）を証明する場合、理論は何らかの に対してを証明することを述べています。ここに、数nを表す項があります ( ∃ x ∈ N ) φ ( x ) {\displaystyle (\exists x\in \mathbb {N} )\varphi (x)} φ ( n ¯ ) {\displaystyle \varphi ({\bar {n}})} n ∈ N . {\displaystyle n\in \mathbb {N} {\text{.}}} n ¯ {\displaystyle {\bar {n}}} T {\displaystyle T}
  • チャーチの法則（CR）は、理論が を証明するならば、自然数eが存在し、指数eを持つ計算可能関数を とすると、理論は を証明する。 ( ∀ x ∈ N ) ( ∃ y ∈ N ) φ ( x , y ) {\displaystyle (\forall x\in \mathbb {N} )(\exists y\in \mathbb {N} )\varphi (x,y)} f e {\displaystyle f_{e}} ( ∀ x ) φ ( x , f e ( x ) ) {\displaystyle (\forall x)\varphi (x,f_{e}(x))}
  • チャーチの法則の変形であるCR 1は、理論が を証明するならば、自然数eが存在し、理論はが全であり が証明されると述べている。 ( ∃ f : N → N ) ψ ( f ) {\displaystyle (\exists f\colon \mathbb {N} \to \mathbb {N} )\psi (f)} f e {\displaystyle f_{e}} ψ ( f e ) {\displaystyle \psi (f_{e})}

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

結果

非例と例

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

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

最も初期の結果は構成的算術理論に関するものでしたが、構成的集合論に関する多くの結果も知られています（Rathjen 2005）。ジョン・マイヒル （1973）は、置換公理を除外し収集公理を採用したIZFは、選言特性、数値的存在特性、および存在特性を持つことを示しました。マイケル・ラスジェン（2005）は、CZFが選言特性と数値的存在特性を持つ ことを証明しました

FreydとScedrov（1990）は、選言特性が自由Heyting代数と自由トポスにおいて成り立つことを観察しました。圏論的に言えば、自由トポスにおいて、これは終端オブジェクトであるが2つの適切な部分オブジェクトの結合ではないという事実に対応します。存在特性と合わせて、は分解不可能な射影オブジェクトであるという主張につながります。つまり、それが表す関数（大域セクション関数）は、エピモーフィズムと余積を保存し ます 1 {\displaystyle \mathbf {1} } 1 {\displaystyle \mathbf {1} }

特性間の関係

上記の5つの特性の間にはいくつかの関係がある。

算術の設定では、数値的存在特性は選言特性を意味する。証明では、選言が自然数上の量化存在式として書き直すことができるという事実を用いる。

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)]} 。

したがって、もし

A ∨ B {\displaystyle A\vee B} が の定理であるならば、 も の定理である。 T {\displaystyle T} ∃ n : ( n = 0 → A ) ∧ ( n ≠ 0 → B ) {\displaystyle \exists n\colon (n=0\to A)\wedge (n\neq 0\to B)}

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

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

は定理です。が数値なので、の値を具体的に確認できます。つまり、ならばは定理であり、 ならばは定理です。 s ¯ {\displaystyle {\bar {s}}} s {\displaystyle s} s = 0 {\displaystyle s=0} A {\displaystyle A} s ≠ 0 {\displaystyle s\neq 0} B {\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 and Andre Scedrov, 1990, Categories, Allegories . North-Holland
  • ハーヴェイ・フリードマン、1975年、「選言の性質は数値的存在の性質を示唆する」、ニューヨーク州立大学バッファロー校
  • ゲルハルト・ゲンツェン、1934年、「論理的閉ざされた数に関する考察。I」、Mathematische Zeitschrift v. 39 n. 2、pp. 176–210
  • ゲルハルト・ゲンツェン、1935年、「論理的閉ざされた数に関する考察。II」、Mathematische Zeitschrift v. 39 n. 3、pp. 405–431
  • クルト・ゲーデル、1932年、「直観主義的展開法について」、ウィーン科学アカデミー広告、v. 69、pp. 65–66
  • スティーブン・コール・クリーネ、1945年、「直観主義的数論の解釈について」『記号論理学ジャーナル』第10巻、109～124ページ
  • ウルリッヒ・コーレンバッハ、2008年、『応用証明理論』、シュプリンガー
  • ジョン・マイヒル、1973年、「直観主義ツェルメロ＝フランケル集合論のいくつかの性質」、A. マティアスとH. ロジャース著、『ケンブリッジ数理論理学サマースクール』、数学講義ノート第337巻、206～231ページ、シュプリンガー
  • 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編 (1973), Metamathematical research of intuitionistic arithmetic and analysis , Springer.
  • Moschovakis, Joan (2022年12月16日). "Intuitionistic Logic". Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .
Retrieved from "https://en.wikipedia.org/w/index.php?title=Disjunction_and_existence_properties&oldid=1276258992"