チャーチのテーゼ（構成的数学）

構成的数学において、チャーチのテーゼは、すべての全関数は 計算可能な関数であるという原理を述べています。 ${\displaystyle {\mathrm {CT} }}$

同様の名前を持つチャーチ＝チューリングのテーゼは、すべての実質的に計算可能な関数は計算可能関数であると述べており、前者の概念は後者の概念に折り畳まれています。 は、それがあればすべての関数が計算可能になるという意味でより強力です。しかし、構成主義原理は、様々な理論や形態において、完全に形式的な公理としても与えられています。形式化は、対象となる理論における「関数」と「計算可能」の定義に依存します。共通の文脈は、1930年代以降に確立された 再帰理論です。${\displaystyle {\mathrm {CT} }}$

を原理として採用すると、存在主張の族（例えば以下）の形の述語が計算可能な方法ですべてに対して検証されないことが証明されている場合、公理の逆否定は、これがどの全体関数によっても検証されない（つまり、 に対応する写像がない）ことを意味します。したがって、基礎理論と比較して関数の概念の可能な範囲が縮小され、計算可能関数の定義された概念に制限されます。次に、公理は、計算不可能であることが証明されている全関数値の関連付けと評価を検証するシステムとは互換性がありません。より具体的には、いくつかの一般的な古典的に証明可能な命題 の否定を証明可能にする方法で証明計算に影響を与えます。${\displaystyle {\mathrm {CT} }}$ ${\displaystyle \exists !y.\varphi (x,y)}$ ${\displaystyle x}$ ${\displaystyle x\mapsto y}$

例えば、ペアノ算術は そのような体系である。その代わりに、自然数間の関連に関する追加の公理として、その第一階定式化におけるテーゼを備えたハイティング算術の構成理論を考えることもできる。この理論は、排中律 の例の普遍的に閉じた変種のいくつかを反証する。このようにして、公理は と両立しないことが示される。しかし、 はと の両方と等価であり、 と によって与えられた理論とも等価である。つまり、排中律とチャーチのテーゼのどちらかを追加してもハイティング算術は矛盾しないが、両方を追加すると矛盾する。 ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {CT} }_{0}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {CT} }_{0}}$

正式な声明

この原理は様々な数学的枠組みで形式化されている。KleeneのT述語を と表記すると、例えば述語 の妥当性は、が全計算可能関数のインデックスであることを表す。また、や の値抽出 のバリエーションも、戻り値を持つ関数として存在することに注意されたい。ここでは、これらは原始的再帰述語として表現されている。 は、値が原理の定式化において役割を果たすため、と略記する。したがって、インデックス を持つ計算可能関数は、 の場合に限り、値 で で終了する。この三項式 の述語は、算術的等式に既に使用されている符号を含む省略記法を導入するという代償を払って、と表現することができる。関係 や を直接量化できないなどの一階理論では、は、有効な存在主張 の族を構成する任意の定義可能な全関係 に対して、後者は の意味で計算可能であるという公理スキーマとして述べられる。2変数の各式について、スキーマには次の公理が含まれる 。${\displaystyle T_{1}}$ ${\displaystyle \forall x\,\exists w\,T_{1}(e,x,w)}$ ${\displaystyle e}$ ${\displaystyle T_{1}}$ ${\displaystyle U}$ ${\displaystyle TU(e,x,w,y)}$ ${\displaystyle T_{1}(e,x,w)\land U(w,y)}$ ${\displaystyle y}$ ${\displaystyle e}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle \exists w\,TU(e,x,w,y)}$ ${\displaystyle \Sigma _{1}^{0}}$ ${\displaystyle e,x,y}$ ${\displaystyle \{e\}(x)=y}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {CT} }}$ ${\displaystyle \exists y}$ ${\displaystyle TU}$ ${\displaystyle \varphi (x,y)}$ ${\displaystyle {\mathrm {CT} }_{0}}$

${\displaystyle {\big (}\forall x\;\exists y\;\varphi (x,y){\big )}\;\to \;\exists e\,{\big (}\forall x\;\exists y\;\exists w\;TU(e,x,w,y)\wedge \varphi (x,y){\big )}}$

言葉で言うと、任意の に対してを満たす が存在する場合、実際に が存在し、これは部分再帰関数のゲーデル数であり、任意の に対して、式 を満たす を生成します。また、いくつかは、が実際に におけるその関数の値であるという事実を証明する検証可能な計算をエンコードするゲーデル数です。 ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle \varphi }$ ${\displaystyle e}$ ${\displaystyle x}$ ${\displaystyle y}$ ${\displaystyle w}$ ${\displaystyle y}$ ${\displaystyle x}$

関連して、この形式の含意は、理論の構成的メタ理論的性質として確立されることもある。すなわち、理論は必ずしも含意（ を含む式）を証明する必要はないが、 の存在はメタ論理的に検証される。この場合、理論は 規則の下で閉じていると言われる。 ${\displaystyle \to }$ ${\displaystyle e}$

変種

拡張されたチャーチの論文

このステートメントは、特定の種類のドメイン上で定義され、かつ全体的である関係にまで主張を拡張します。これは、全称量化子のスコープを狭めることを許容することで実現でき、したがって、スキーマによって形式的に記述できます。 ${\displaystyle {\mathrm {ECT_{0}} }}$

${\displaystyle {\big (}\forall x\;\psi (x)\to \exists y\;\varphi (x,y){\big )}\;\to \;\exists e\,{\big (}\forall x\;\psi (x)\to \exists y\;\exists w\;TU(e,x,w,y)\wedge \varphi (x,y){\big )}}$

上記において、はほぼ負に制限されています。一階算術（スキーマが と指定されている場合）の場合、これは がいかなる選言も含まないことを意味し、存在量指定子は（決定可能な）式の前でのみ使用できます。マルコフ原理が存在する場合、構文上の制約はいくらか緩和される可能性があります。^[1]${\displaystyle \psi }$ ${\displaystyle {\mathrm {ECT_{0}} }}$ ${\displaystyle \psi }$ ${\displaystyle \Delta _{0}^{0}}$ ${\displaystyle {\mathrm {MP} }}$

すべての数の領域を考慮すると（たとえば、を自明な とするとき）、上記はチャーチのテーゼの以前の形式に簡約されます。 ${\displaystyle \psi (x)}$ ${\displaystyle x=x}$

これらの 1 階の定式化は、関数選択の形式も構成するという点で、かなり強力です。つまり、全関係には全再帰関数が含まれます。

拡張されたチャーチのテーゼは、アンドレイ・マルコフによって設立された構成的数学の学派によって使用されています。

機能的前提

${\displaystyle {\mathrm {CT} }_{0}!}$ は、前提が（ の）一意の存在を要求する、つまり戻り値がすでに決定されている必要があるという 原理の弱い変形を表します。${\displaystyle y}$

高次の定式化

上記の命題の最初の定式化は、数に対する量化子のみが登場するため、原理の算術的形式とも呼ばれます。この定式化では、前件部に一般関係が用いられています。再帰理論のような枠組みでは、関数は関数関係として表現でき、入力ごとに一意の出力値を与えることができます。 ${\displaystyle \varphi }$

（全）関数を直接量化できる高階システムにおいては、自然数から自然数へのあらゆる関数は計算可能であるという単一の公理として、 の形を述べることができる。原始的な再帰述語を用いると、 ${\displaystyle {\mathrm {CT} }}$

${\displaystyle \forall f\;\exists e\,{\big (}\forall x\;\exists w\;TU(e,x,w,f(x)){\big )}}$

これは、すべての関数が理論上の添え字を用いてクリーネの意味で計算可能であることを仮定する。したがって、すべての値 も同様である。外延的等式を表すために と書くこともできる。 ${\displaystyle f}$ ${\displaystyle e}$ ${\displaystyle y=f(x)}$ ${\displaystyle \forall f\;\exists e\,f\cong \{e\}}$ ${\displaystyle f\cong g}$ ${\displaystyle \forall x.f(x)=g(x)}$

例えば、集合論において関数は定義により関数空間の要素であり、全関数です。全関数は、その定義域内のすべての入力に対して一意の戻り値を持ちます。集合論は関数を集合として扱うため、関数全体にわたる量指定子を持ちます。

この原理は、空間を全帰納的関数の集合と同一視するものとみなすことができる。実現可能性トポイにおいては、この自然数オブジェクトの指数オブジェクトは、より制約の少ない写像の集合と同一視することもできる。 ${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$

弱い発言

テーゼには、さまざまな名前で呼ばれる、より弱い形式もあります。 ${\displaystyle {\mathrm {WCT} }}$

高階版では、インデックスの存在主張の前に 二重否定を挿入することで、非再帰関数は存在しないと主張されます。これは関数選択公理を構成しませんが、関数の空間を依然として制限します。

関連する記述は、自然数の任意の決定可能な部分集合は、以下の意味で計算可能であると否定できないということである。

${\displaystyle {\big (}\forall x\ \chi (x)\lor \neg \chi (x){\big )}\;\to \;\neg \neg \exists e\,{\big (}\forall x\,{\big (}\exists w\;T_{1}(e,x,w){\big )}\leftrightarrow \chi (x){\big )}}$

この逆否定は、任意の計算不可能な述語を排中律に違反させるため、これは依然として一般に反古典的である。とは異なり、原理的にはこれは扇形定理の定式化と両立する。 ${\displaystyle \mathrm {CT} _{0}}$

関連する前提のバリエーションを定義することもできます。例えば、ある離散二項集合への全帰納的関数の存在を常に認め、その関数が選言の1つを成立させるという原理などです。二重否定を除けば、これは と表記できます。 ${\displaystyle \forall x\ \psi _{\mathrm {left} }(x)\lor \psi _{\mathrm {right} }(x)}$ ${\displaystyle {\mathbb {N} }\to \{\mathrm {left} ,\mathrm {right} \}}$ ${\displaystyle \mathrm {CT} _{0}^{\lor }}$

古典論理との関係

スキーマ は、 などの構成的システムに追加されると、一部の述語について排中律の普遍量化バージョンの否定を意味します。 例として、停止性問題は計算可能決定可能ではないことが証明されていますが、古典論理を想定すると、すべてのチューリングマシンは与えられた入力に対して停止するか停止しないかのどちらかであるというトートロジーです。 さらにチャーチのテーゼを想定すると、今度はこれが計算可能であるという結論に達しますが、これは矛盾です。 もう少し詳しく説明すると、 などの十分に強いシステムでは、停止性の問題に関連付けられた関係、つまりチューリングマシンの列挙からの任意のコードと からの値を関連付ける関係を表現することが可能です。 上記の古典的なトートロジーを想定すると、この関係は完全であることが証明できます。つまり、マシンが停止する場合は を返し、停止しない場合は を返す関数を構成します。 しかし、たとえば、 plus は排中律のこの帰結を反証します。 ${\displaystyle {\mathrm {CT} }_{0}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle h}$ ${\displaystyle \{0,1\}}$ ${\displaystyle 1}$ ${\displaystyle 0}$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {CT} }_{0}}$

二重否定シフト（二重否定を持つ全称量化の可換性）のような原理もこの原理によって拒否されます。

上記の の単一公理形式は、前段落の関数のような関数を形成する力を持たないいくつかの弱い古典的体系と整合している。例えば、 はすべての関数が計算可能なモデルを持つため、古典的な弱い二階算術はこの単一公理と整合している。しかし、 のような関数の存在を証明するのに十分な公理を持つ体系では、単一公理形式は排中律と整合しない。例えば、数値量指定子に対する 一意の選択など、可算選択の変種の採用は、${\displaystyle {\mathrm {CT} }}$ ${\displaystyle \forall f}$ ${\displaystyle {\mathsf {RCA_{0}}}}$ ${\displaystyle {\mathsf {RCA_{0}}}}$ ${\displaystyle h}$

${\displaystyle \forall n\;\exists !m\;\phi (n,m)\to \exists a\;\forall k\;\phi (k,a_{k}),}$

がシーケンスを表す 場合、この一貫性が損なわれます。${\displaystyle a}$

一次定式化では、列挙された関数を介して、このような関数理解原理の力がすでに組み込まれています。 ${\displaystyle {\mathrm {CT} }_{0}}$

の構成的に定式化された部分理論は、典型的にはチャーチの規則の下で閉じていることが示され、対応する原理はしたがって両立する。しかし、その帰結として（）はそのような理論によって証明することはできない。なぜなら、証明すれば、より強力な古典的理論が矛盾することになるからだ。 ${\displaystyle {\mathsf {ZF}}}$ ${\displaystyle \to }$

実現者とメタロジック

上記の命題は、「文が真であるためには、それが計算可能実現可能である必要がある」と述べていると特徴付けられます。これは、以下のメタ理論的同値性によって捉えられます。^[2]

${\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }\vdash \varphi \leftrightarrow \exists n\,(n\Vdash \varphi )}$

そして

${\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }\vdash \varphi \;\iff \;{\mathsf {HA}}\vdash \exists n\,(n\Vdash \varphi )}$

ここで「」は算術理論における同値性を表すものであり、「」はメタ理論的同値性を表します。 が与えられた場合、述語は「 」と読みます。言葉で言えば、上記の最初の結果は、文が真であることは、それが実現可能である場合に限り、プラスで証明可能であることを示しています。また、上記の2番目の結果は、 が プラスで証明可能であることは、 が だけで証明可能に実現可能である場合に限り、プラスで証明可能であることを示しています。 ${\displaystyle \leftrightarrow }$ ${\displaystyle \iff }$ ${\displaystyle \varphi }$ ${\displaystyle n\Vdash \varphi }$ ${\displaystyle n{\text{ realises }}\varphi }$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {ECT_{0}} }}$ ${\displaystyle \varphi }$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {ECT_{0}} }}$ ${\displaystyle \varphi }$ ${\displaystyle {\mathsf {HA}}}$

次のメタ論理定理については、が非構成的であり存在特性を欠いていることを思い出してください。一方、Heyting 算術ではそれが示されます。 ${\displaystyle {\mathsf {PA}}}$

${\displaystyle {\mathsf {HA}}\vdash \exists n.\phi (n)\implies {\text{exists}}\;{\mathrm {n} }\ {\mathsf {HA}}\vdash \phi ({\underline {\mathrm {n} }})}$

上記の 2 番目の同等性は、次のように拡張できます。 ${\displaystyle {\mathrm {MP} }}$

${\displaystyle {\mathsf {HA}}+{\mathrm {ECT_{0}} }+{\mathrm {MP} }\vdash \varphi \;\iff \;{\text{exists}}\;{\mathrm {n} }\ {\mathsf {PA}}\vdash ({\underline {\mathrm {n} }}\Vdash \varphi )}$

この場合、存在量化子は外側に置く必要があります。言い換えれば、が と の両方において証明可能であるためには、 で表される に対応する標準数が を証明可能に実現するような数が存在することがメタ理論的に証明できる必要があります。チャーチのテーゼの別の変種と併せて仮定することで、このようなメタ論理的存在命題がさらに得られています。 ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle \varphi }$ ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {ECT_{0}} }}$ ${\displaystyle {\mathrm {MP} }}$ ${\displaystyle {\mathrm {n} }}$ ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\underline {\mathrm {n} }}}$ ${\displaystyle \varphi }$ ${\displaystyle {\mathrm {MP} }}$

参照

• 計算可能な関数
• 選言と存在の性質
• 実現可能性

参考文献

1. Troelstra, AS, van Dalen D.,数学における構成主義：入門1 ; 論理学と数学の基礎研究; Springer, 1988; p. 206
2. Troelstra, AS 「直観主義的算術と解析のメタ数学的研究」数学講義ノート第344巻、Springer、1973年

• エリオット・メンデルソン（1990）「チャーチのテーゼと数学的証明についての再考」『哲学ジャーナル』 87（5）：225–233。