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

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

同様の名前を持つチャーチ＝チューリングのテーゼは、すべての効果的に計算可能な関数は計算可能な関数であると述べており、前者の概念は後者の概念に集約されます。 は、すべての関数が計算可能であるという意味でより強力です。ただし、構成主義の原理は、さまざまな理論や形態で、完全に形式的な公理としても与えられています。形式化は、理論の「関数」と「計算可能」の定義によって異なります。共通のコンテキストは、1930 年代以降に確立された 再帰理論です。${\displaystyle {\mathrm {CT} }}$

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

たとえば、ペアノ算術 はそのようなシステムです。その代わりに、自然数間の関連に関する追加の公理として、その第 1 階定式化におけるテーゼを備えたヘイティング算術の構成的理論を検討することができます。この理論は、排中律 の例の普遍的に閉じた変種のいくつかを反証します。このようにして、公理は と矛盾することが示されます。しかし、 はと の両方と等価であり、と を加算することによって与えられる理論とも等価です。つまり、排中律またはチャーチのテーゼのいずれかを追加してもヘイティング算術は矛盾しませんが、両方を追加すると矛盾します。 ${\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 述語とすると、例えば述語 の妥当性は、が全計算可能関数のインデックスであることを表す。また、のバリエーションや、 の値を抽出する関数も、戻り値を持つ関数として存在することに注意する。ここでは、それらは原始的な再帰述語として表現されている。は、値が原理の定式化で役割を果たすため、 と省略して書く。したがって、インデックスを持つ計算可能関数は、の場合に限り、値でで終了する。トリプル上の のこの-述語は、算術等式にすでに使用されている符号を含む省略表記を導入するコストをかけて、で表現できる。 などの第 1 階理論では、関係や関数を直接定量化できないが、 は、有効な存在主張 の族を含む任意の定義可能な全関係に対して、後者は の意味で計算可能であるという公理スキーマとして記述できる。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階算術（スキーマが と指定されている）の場合、これは がいかなる選言も含むことができないことを意味し、存在量指定子は（決定可能な）式の前でのみ使用できます。マルコフの原理が存在する場合、構文上の制限はいくらか緩和される可能性があります。^[1]${\displaystyle \psi}$${\displaystyle {\mathrm {ECT_{0}} }}$${\displaystyle \psi}$${\displaystyle \Delta _{0}^{0}}$ ${\displaystyle {\mathrm {MP} }}$

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

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

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

${\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 xf(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 {左} ,\mathrm {右} \}}$${\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}}$

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

上記のの単一公理形式は、前の段落の関数のような関数を形成する力を持たないいくつかの弱い古典的システムと整合している。例えば、 はすべての関数が計算可能なモデルを持つため、古典的な弱い2階算術はこの単一公理と整合している。しかし、関数 のような関数の存在を証明するのに十分な公理を持つシステムでは、単一公理形式は排中律と整合しなくなる。例えば、数値量指定子に対する 一意の選択など、可算選択の変形の採用、${\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 )}$

この場合、存在量指定子は外側にある必要があります。つまり、が と の両方で証明可能であるためには、 で示される対応する標準数が を実現することがメタ理論的に確立できる必要があります。を Church のテーゼの別の変形とともに仮定すると、そのようなメタ論理的存在ステートメントがさらに得られています。 ${\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} }}$

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

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