ハイティング算術

ハイティング算術（はいてぃんぐさんじゅつ、テンプレート:Lang-en-short）$𝖧𝖠$ は、数理論理学において直観主義の哲学に基づく算術の公理化である。これを最初に提唱したアレン・ハイティングにちなんで命名された。

公理化

ハイティング算術は、一階の理論であるペアノ算術 $𝖯𝖠$ と同様に特徴づけることができるが、推論に直観主義述語計算 $𝖨𝖰𝖢$ を用いる点が異なる。特に、二重否定除去原理および排中律 $\mathrm{P}\mathrm{E}\mathrm{M}$ は成立しない。$\mathrm{P}\mathrm{E}\mathrm{M}$ が成立しないとは、すべての命題に対して排中律の命題が自動的に証明可能ではないことを意味する——実際、そのような命題の多くは $𝖧𝖠$ においても証明可能であり、そのような論理和の否定は矛盾している。$𝖯𝖠$ は $𝖧𝖠$ より真に強く、すべての $𝖧𝖠$-定理は $𝖯𝖠$-定理でもある。

ハイティング算術はペアノ算術の公理を含み、想定モデルは自然数の集まり $\mathbb{N}$ である。シグネチャにはゼロ "$0$" と後続者 "$S$" が含まれ、理論は加法と乗法を特徴づける。これは論理に影響を与える：$1:=S0$ とすると、$\mathrm{\perp }$ は $0=1$ として定義でき、したがってすべての命題 $P$ に対して $\mathrm{\neg }P$ は $P\to \mathrm{\perp }$ であるというメタ定理が成立する。$\mathrm{\perp }$ の否定は $P\to P$ の形であり、自明な命題である。

項については、$s\ne t$ を $\mathrm{\neg }(s=t)$ の略記として使用する。固定された項 $t$ に対して、等号 $t=t$ は反射律により真であり、命題 $P$ は $(t=t)\to P$ と同値である。$P\vee Q$ は $\mathrm{\exists }n.(n=0\to P)\wedge (n\ne 0\to Q)$ として定義できることを示すことができる。この論理和の形式的消去は、量化子を持たない原始帰納的算術 $𝖯𝖱𝖠$ では不可能であった。この理論は任意の原始再帰関数の関数記号によって拡張でき、$𝖯𝖱𝖠$ もこの理論の断片となる。全域関数 $f$ に対して、$f(n)=0$ の形の述語がしばしば考察される。

定理

二重否定

爆発律が任意の直観主義的理論において有効であることから、ある $P$ に対して $\mathrm{\neg }\mathrm{\neg }P$ が定理であれば、定義より $\mathrm{\neg }P$ が証明可能であることは理論が矛盾していることと同値である。実際、ハイティング算術において二重否定は明示的に $\mathrm{\neg }P\to 0=1$ を表す。述語 $Q$ に対して、$\mathrm{\neg }\mathrm{\neg }\mathrm{\exists }n.Q(n)$ の形の定理は、ある $t$ に対して $\mathrm{\neg }Q(t)$ が検証できるという可能性を排除することが矛盾していることを表す。構成的には、これはそのような $t$ の存在主張より弱い。メタ理論的議論の大部分は、古典的に証明可能な存在主張に関するものである。

二重否定 $\mathrm{\neg }\mathrm{\neg }P$ は $(\alpha \to \mathrm{\neg }P)\to (\alpha \to 0=1)$ を含意する。したがって $\mathrm{\neg }\mathrm{\neg }P$ の形の定理は、（正の）命題 $\alpha$ を決定的に否定する新たな手段を常に与える。

古典的に同値な命題の証明

$𝖧𝖠⊢\alpha \to \mathrm{\neg }\mathrm{\neg }\alpha$ における含意はテンプレート:仮リンクにより古典的には逆転でき、同様に $𝖧𝖠⊢(\mathrm{\exists }n.\mathrm{\neg }\psi (n))\to \mathrm{\neg }\mathrm{\forall }n.\psi (n)$ における含意も逆転できる。ここでの区別は、数値的反例の存在と、すべての数について妥当性を仮定したときの矛盾的結論との間にある。二重否定を挿入することで $𝖯𝖠$-定理を $𝖧𝖠$-定理に変換できる。より正確には、$𝖯𝖠$ において証明可能な任意の論理式に対して、その論理式の古典的に同値な二重否定翻訳（ゲーデル–ゲンツェン否定翻訳）はすでに $𝖧𝖠$ において証明可能である。ある定式化では、翻訳手続きには $(\mathrm{\exists }n.Q(n){)}^N$ を $\mathrm{\neg }\mathrm{\forall }n.\mathrm{\neg }{Q}^N(n)$ に書き換えることが含まれる。この結果は、すべてのペアノ算術の定理が、構成的証明とその後の古典的論理的書き換えからなる証明を持つことを意味する。おおよそ言えば、最終ステップは二重否定除去の適用に相当する。

特に、原子命題が決定不能でない場合、存在量化子や論理和を一切含まない任意の命題 $\psi$ に対して、$𝖯𝖠⊢\psi ⟺𝖧𝖠⊢\psi$ が成立する。

有効な原理と規則

最小論理は否定された論理式に対する二重否定除去 $\mathrm{\neg }\mathrm{\neg }(\mathrm{\neg }\alpha )\leftrightarrow (\mathrm{\neg }\alpha )$ を証明する。より一般的に、ハイティング算術は任意のテンプレート:仮リンクに対してこの古典的同値を証明する。

また ${\mathrm{\Sigma }}_1^0$-結果も良好な振る舞いを示す：算術的階層の最低レベルにおけるマルコフ規則はテンプレート:仮リンクの推論規則であり、$n$ を自由変数とする $\phi$ に対して

$𝖧𝖠⊢\mathrm{\neg }\mathrm{\neg }\mathrm{\exists }m.\phi (n,m)⟺𝖧𝖠⊢\mathrm{\exists }m.\phi (n,m)$

量化子なし述語の代わりに、原始再帰述語やテンプレート:仮リンクに対しても同等に定式化でき、それぞれ ${\mathrm{M}\mathrm{R}}_{\mathrm{Q}\mathrm{F}}$、${\mathrm{M}\mathrm{R}}_{\mathrm{P}\mathrm{R}}$、${\mathrm{M}\mathrm{R}}_0$ と呼ばれる。関連する規則 ${\mathrm{M}\mathrm{R}}_{\mathrm{D}\mathrm{e}\mathrm{c}}$ も許容的である。これは $\phi$ の扱いやすさが構文的条件に基づくのではなく、左辺が $⊢\mathrm{\forall }m.\phi (n,m)\vee \mathrm{\neg }\phi (n,m)$ を要求する場合である。

命題をその構文的形式に基づいて分類する際には、古典的にのみ有効な同値に基づいて複雑さをより低く割り当てないよう注意が必要である。

排中律

直観主義論理上の他の理論と同様に、この構成的算術においても $\mathrm{P}\mathrm{E}\mathrm{M}$ のさまざまな例が証明できる。論理和の導入により、命題 $P$ または $\mathrm{\neg }P$ のいずれかが証明されれば、$P\vee \mathrm{\neg }P$ も証明される。たとえば、公理から $0=0$ と $\mathrm{\forall }n.Sn\ne 0$ を用いれば、述語 $n=0$ に対する排中律の帰納法の前提を検証できる。このとき、ゼロとの等号は決定可能であると言う。実際、$𝖧𝖠$ はすべての数に対して等号 "$=$" が決定可能であること、すなわち $\mathrm{\forall }n.\mathrm{\forall }m.(n=m\vee n\ne m)$ を証明する。さらに強く、等号がハイティング算術における唯一の述語記号であることから、$n,\dots ,m$ を自由変数とする任意の量化子なし論理式 $\varphi$ に対して、理論は以下の規則の下で閉じている：

$𝖧𝖠⊢\mathrm{\forall }n.\cdots \mathrm{\forall }m.\varphi (n,\dots ,m)\vee \mathrm{\neg }\varphi (n,\dots ,m)$

最小論理上の任意の理論は、すべての命題に対して $\mathrm{\neg }\mathrm{\neg }(P\vee \mathrm{\neg }P)$ を証明する。したがって、理論が無矛盾であれば、排中律の命題の否定を証明することはない。

実用的に言えば、$𝖧𝖠$ のような保守的な構成的枠組みにおいては、アルゴリズム的に決定可能な命題の種類が理解されているとき、排中律の論理和の証明不可能性の結果は $P$ のアルゴリズム的決定不可能性を表す。

保存性

単純な命題については、この理論は $\varphi (n,\dots )\vee \mathrm{\neg }\varphi (n,\dots )$ のような古典的に有効な二値的二分法を単に検証するだけではない。テンプレート:仮リンクを用いることで、$𝖯𝖠$ の ${\mathrm{\Pi }}_2^0$-定理がすべて $𝖧𝖠$ によって証明されることを示すことができる：任意の $n$ と量化子なし $\phi$ に対して、

$𝖯𝖠⊢\mathrm{\exists }m.\phi (n,m)⟺𝖧𝖠⊢\mathrm{\exists }m.\phi (n,m)$

この結果は、明示的な全称閉包 $\mathrm{\forall }n$ を使っても表現できる。おおよそ言えば、古典的に証明可能な計算可能関係についての単純な命題は、すでに構成的に証明可能である。ただし停止性問題では、量化子なし命題だけでなく ${\mathrm{\Pi }}_1^0$-命題も重要な役割を果たし、これらは古典的にも独立となりうる。同様に、無限領域における一意存在 $\mathrm{\exists }!n.Q(n)$、すなわち $\mathrm{\exists }n.\mathrm{\forall }w.(n=w\leftrightarrow Q(w))$ も形式的には特に単純ではない。

したがって $𝖯𝖠$ は $𝖧𝖠$ 上で ${\mathrm{\Pi }}_2^0$-保存的である。これはロビンソン算術 $𝖰$（帰納法を欠くより弱い理論）の状況と対比できる。古典的 $𝖰$ はすべての ${\mathrm{\Sigma }}_1^0$-$𝖯𝖠$-定理を証明するが、単純な ${\mathrm{\Pi }}_1^0$-$𝖯𝖠$-定理の中にはすでに独立なものがある。テンプレート:仮リンクの結果において帰納法が重要な役割を果たすことがわかる。$𝖰$ を順序に関する公理（オプションとして決定可能な等号）で強化した、より扱いやすい理論は、その直観主義的対応物より多くの ${\mathrm{\Pi }}_2^0$-命題を証明する。

ここでの議論は決して網羅的ではない。古典的定理がすでに構成的理論に含意される場合についてさまざまな結果がある。また、メタ論理的結果を得るために用いられた論理が何であるかが関連することもある。たとえば、実現可能性に関する多くの結果は構成的メタ論理で得られている。しかし、特定の文脈が与えられていない場合、記述された結果は古典的であると仮定する必要がある。

証明不可能な命題

独立性の結果は、理論において命題もその否定も証明できないような命題に関するものである。古典的理論が無矛盾（$\mathrm{\perp }$ を証明しない）であり、構成的対応物がその古典的定理 $P$ の一つを証明しない場合、その $P$ は後者から独立している。いくつかの独立命題が与えられると、特に構成的枠組みでは、そこからさらに多くを定義することが容易である。

ハイティング算術はテンプレート:仮リンク（論理和性質） $\mathrm{D}\mathrm{P}$ を持つ：すべての命題 $\alpha$ と $\beta$ に対して、

$𝖧𝖠⊢\alpha \vee \beta ⟺𝖧𝖠⊢\alpha \text{ または }𝖧𝖠⊢\beta$

実際、これとその数値的一般化は、構成的二階算術およびテンプレート:仮リンク $𝖢𝖹𝖥$ や $𝖨𝖹𝖥$ においても成立する。これは構成的理論という非形式的概念の一般的な必要条件である。$\mathrm{D}\mathrm{P}$ を持つ理論において、命題 $P$ が独立であれば、古典的に自明な $P\vee \mathrm{\neg }P$ も別の独立命題であり、逆も成立する。スキーマは、証明できない例が少なくとも一つ存在するときに有効でないとされ、これが $\mathrm{P}\mathrm{E}\mathrm{M}$ が失敗する理由である。$\mathrm{D}\mathrm{P}$ は、どちらの論理和も検証せずに排中律の命題を公理として採用することで破ることができ、$𝖯𝖠$ の場合がこれにあたる。

さらに言えば：$P$ が古典的に独立であれば、その否定 $\mathrm{\neg }P$ も独立である——これは $\mathrm{\neg }\mathrm{\neg }P$ が $P$ と同値かどうかに関わらず成立する。したがって構成的には、弱排中律 $\mathrm{W}\mathrm{P}\mathrm{E}\mathrm{M}$ は成立しない、すなわちすべての命題に対して $\mathrm{\neg }\alpha \vee \mathrm{\neg }\mathrm{\neg }\alpha$ が成立するという原理は有効でない。そのような $P$ が ${\mathrm{\Sigma }}_1^0$ であれば、論理和の証明不可能性は ${\mathrm{\Pi }}_1^0$-$\mathrm{P}\mathrm{E}\mathrm{M}$ の崩壊、あるいは原始再帰関数に対するテンプレート:仮リンク $\mathrm{W}\mathrm{L}\mathrm{P}\mathrm{O}$ の例として現れる。

古典的に独立な命題

ゲーデルの不完全性定理の知識は、$𝖯𝖠$ では証明可能だが $𝖧𝖠$ では証明不可能な命題の種類を理解するのに役立つ。

ヒルベルトの第10問題の解決により、解を持つという主張がアルゴリズム的に決定不能であるような具体的な多項式 $f$ と対応する多項式方程式が得られた。その命題は以下のように表せる：

$\mathrm{\exists }{w}_1.\cdots \mathrm{\exists }{w}_n.f(w_1,\dots ,w_n)=0$

このようなゼロ値存在主張の中には特定の解釈を持つものがある：$𝖯𝖠$ や $𝖹𝖥𝖢$ のような理論は、これらの命題が理論自身の矛盾性の算術化された主張と同値であることを証明する。したがって、そのような命題は強い古典的集合論に対しても書き下すことができる。

無矛盾で健全な算術理論において、そのような存在主張 ${\mathrm{I}}_f$ は独立した ${\mathrm{\Sigma }}_1^0$-命題である。その場合、否定を量化子を通じて押し込むことで、${\mathrm{C}}_f:=\mathrm{\neg }{\mathrm{I}}_f$ は独立したゴールドバッハ型——すなわち ${\mathrm{\Pi }}_1^0$-命題——であることがわかる。明示的に言えば、二重否定 $\mathrm{\neg }\mathrm{\neg }{\mathrm{I}}_f$（または $\mathrm{\neg }{\mathrm{C}}_f$）も独立している。また三重否定は直観主義的に一重否定と同値である。

PAがDPに違反する

以下は、そのような独立命題が関与する意味を明らかにする。理論のすべての証明の列挙におけるインデックスが与えられると、それがどの命題の証明であるかを調べることができる。$𝖯𝖠$ は、この手続きを正しく表現できるという意味で適切である：$\mathrm{F}(w):=\mathrm{P}\mathrm{r}\mathrm{f}(w,⌜0=1⌝)$ は矛盾命題 $0=1$ の証明であることを表す原始再帰述語である。これは上述の、多項式の返り値がゼロであることに関するより明示的な算術的述語と関連する。$𝖯𝖠$ が無矛盾であれば、個々のインデックス $\mathrm{w}$ に対して $\mathrm{\neg }\mathrm{F}(\underset{\_}{\mathrm{w}})$ を証明することが、メタ論理的に確認できる。

有効に公理化された理論では、各証明を順次検査することができる。理論が実際に無矛盾であれば、矛盾の証明は存在せず、これは「矛盾探索」が決して停止しないことに対応する。形式的には、矛盾性の算術化主張を否定する $\mathrm{\neg }\mathrm{\exists }w.\mathrm{F}(w)$ がこれを表す。等価な ${\mathrm{\Pi }}_1^0$-命題 $\mathrm{\forall }w.\mathrm{\neg }\mathrm{F}(w)$ は、すべての証明が矛盾の証明でないことを述べることで探索の不停止を形式化する。そして実際、可証性を正確に表現できるΩ無矛盾な理論においては、ゲーデルによって示されたように、矛盾探索が停止によって終わるという証明も（明示的矛盾は導出不可）、矛盾探索が決して停止しないという証明も（無矛盾性は導出不可）存在しない。言い換えれば、矛盾探索が決して停止しないことの証明も（無矛盾性は導出不可）、矛盾探索が決して停止しないことではないことの証明も（無矛盾性は否定不可）存在しない。これら二つの論理和はいずれも $𝖯𝖠$-証明可能でないが、その論理和は自明に $𝖯𝖠$-証明可能である。したがって $𝖯𝖠$ が無矛盾であれば、$\mathrm{D}\mathrm{P}$ に違反する。

$0=1$ の証明の存在を表す ${\mathrm{\Sigma }}_1^0$-命題は論理的に肯定的な命題である。しかし歴史的には $\mathrm{\neg }{\mathrm{C}\mathrm{o}\mathrm{n}}_{𝖯𝖠}$ と表記され、その否定は ${\mathrm{C}\mathrm{o}\mathrm{n}}_{𝖯𝖠}$ と表記される ${\mathrm{\Pi }}_1^0$-命題である。構成的文脈においては、この否定記号の使用は誤解を招く命名かもしれない。

フリードマンは別の興味深い証明不可能な命題も確立した。すなわち、無矛盾かつ適切な理論は、その算術化された論理和性質を決して証明しない。

証明不可能な古典的原理

最小論理はすでにすべての非矛盾律の主張を論理的に証明し、特に $\mathrm{\neg }({\mathrm{I}}_f\wedge \mathrm{\neg }{\mathrm{I}}_f)$ と $\mathrm{\neg }({\mathrm{C}}_f\wedge \mathrm{\neg }{\mathrm{C}}_f)$ を証明する。また $({\mathrm{C}}_f\wedge \mathrm{\neg }{\mathrm{C}}_f)\leftrightarrow \mathrm{\neg }({\mathrm{I}}_f\vee \mathrm{\neg }{\mathrm{I}}_f)$ であるから、定理 $\mathrm{\neg }({\mathrm{C}}_f\wedge \mathrm{\neg }{\mathrm{C}}_f)$ は証明可能な二重否定された排中律の論理和（あるいは存在主張）として読むことができる。しかし論理和性質に照らせば、平易な排中律 ${\mathrm{C}}_f\vee \mathrm{\neg }{\mathrm{C}}_f$ は $𝖧𝖠$-証明可能ではありえない。したがってド・モルガンの法則の一つも直観主義的には一般に成立しない。

$\mathrm{W}\mathrm{P}\mathrm{E}\mathrm{M}$ と $\mathrm{W}\mathrm{L}\mathrm{P}\mathrm{O}$ の原理の崩壊については説明した。$𝖯𝖠$ においては、最小数原理 $\mathrm{L}\mathrm{N}\mathrm{P}$ は帰納法原理と同値な多くの命題の一つに過ぎない。以下の証明は $\mathrm{L}\mathrm{N}\mathrm{P}$ が $\mathrm{P}\mathrm{E}\mathrm{M}$ を含意することを示し、したがってこの原理も $𝖧𝖠$ において一般に有効ではありえない理由を示す。しかし、すべての非自明な述語に対して二重否定された最小数存在を認めるスキーマ（$\mathrm{\neg }\mathrm{\neg }\mathrm{L}\mathrm{N}\mathrm{P}$ と表記される）は一般に有効である。ゲーデルの証明に照らせば、これら三つの原理の崩壊は、ハイティング算術がテンプレート:仮リンクの証明可能性読みと無矛盾であることとして理解できる。

原始再帰述語に対するマルコフの原理 ${\mathrm{M}\mathrm{P}}_{\mathrm{P}\mathrm{R}}$ は $𝖧𝖠$ の含意スキーマとしてはすでに成立せず、より強い ${\mathrm{M}\mathrm{P}}_{\mathrm{D}\mathrm{e}\mathrm{c}}$ はなおさらである。ただし対応する規則の形では、前述のとおり許容的である。同様に、この理論は否定された述語に対するテンプレート:仮リンク原理 $\mathrm{I}\mathrm{P}$ を証明しないが、すべての否定命題に対する規則の下では閉じている。すなわち $\mathrm{\neg }P\to \mathrm{\exists }n.Q(n)$ において存在量化子を引き出すことができる。存在命題を単なる論理和に置き換えた版についても同様である。

有効な含意 $\mathrm{\neg }\mathrm{\neg }(\alpha \to \beta )\to (\alpha \to \mathrm{\neg }\mathrm{\neg }\beta )$ は選言三段論法を用いることでその逆形式でも成立することが証明できる。しかし、二重否定シフト $\mathrm{D}\mathrm{N}\mathrm{S}$、すなわちすべての数に対する全称量化との "$\mathrm{\neg }\mathrm{\neg }$" の可換性のスキーマは直観主義的には証明不可能である。これはチャーチのテーゼの節で論じるように、ある $M$ に対する $\mathrm{\neg }{\mathrm{D}\mathrm{e}\mathrm{c}}_M$ の無矛盾性によって説明される興味深い崩壊である。

最小数原理

自然数上の順序関係を用いると、強帰納法原理は以下のように書ける：

$\mathrm{\forall }n.\left(\right(\mathrm{\forall }(k<n).\varphi (k))\to \varphi (n))\to \mathrm{\forall }m.\varphi (m)$

集合論で馴染みのあるクラス記法では、算術的命題 $Q(n)$ は $n\in B$（ここで $B:=\{m\in \mathbb{N}\mid Q(m)\}$）と表される。否定形の述語、すなわち $\varphi (n):=\mathrm{\neg }(n\in B)$ に対して、帰納法と論理的に同値なのは以下である：

$\mathrm{\neg }\mathrm{\exists }(n\in B).\mathrm{\neg }\mathrm{\exists }(k\in B).k<n\leftrightarrow B=\{\}$

洞察は、$B\subseteq \mathbb{N}$ の部分クラスの中で、（証明可能に）最小元を持たないという性質は空クラスであることと同値だということである。対偶を取ると、空でない部分クラスに対して、$B$ の元 $n\in B$ で $n$ より小さい $B$ の元が存在しないものの存在を一貫して排除できないことを表す定理が得られる：

$B\ne \{\}\to \mathrm{\neg }\mathrm{\neg }\mathrm{\exists }(n\in B).\mathrm{\neg }\mathrm{\exists }(k\in B).k<n$

二重否定除去が常に有効なペアノ算術では、これは一般的な定式化における最小数原理を証明する。古典的読みでは、空でないことはある最小元によって（証明可能に）充足されることと同値である。

上の形で強帰納法スキーマを検証する二項関係 "$<$" は常に非反射的でもある：固定された数 $c$ に対して ${\varphi }_c(n):=(n\ne c)$、あるいは同値的に

$Q_c(n):=(n=c)$

を考えると、上の式は $B=\{c\}$ の元 $k$ が $k<c$ を満たさないという命題に簡約される、すなわち $\mathrm{\neg }(c<c)$ である（この論理的推論は二項関係の他の性質を使っていない）。より一般的に、$B$ が空でなく、関連する（古典的）最小数原理を用いて否定形の命題を証明できるなら、これを完全に構成的な証明に拡張できる。含意 $\alpha \to \mathrm{\neg }\beta$ は常に直観主義的に形式的に強い $(\mathrm{\neg }\mathrm{\neg }\alpha )\to \mathrm{\neg }\beta$ と同値だからである。

しかし一般に、構成的論理上では最小数原理の弱化を持ち上げることはできない。次の例がこれを示す：ある命題 $P$（たとえば上の ${\mathrm{C}}_f$）に対して、述語

$Q_P(n):=(n=0\wedge P)\vee (n=1)$

を考える。この $Q_P$ は自然数の部分クラス $b_P:=\{z\in \{0\}\mid P\}\cup \{1\}$ に対応する。このクラスの元であることが証明または仮定されたすべての数は $0$ または $1$ に等しいことが証明でき、すなわち $b_P\subseteq \{0,1\}$ である。$1=1$ であるから、命題 $Q_P(1)$（すなわち $1\in b_P$）は自明に真であり、クラスはテンプレート:仮リンク（非空）である。さらに、等号の決定可能性と選言三段論法を用いることで、同値 $Q_P(0)\leftrightarrow P$ が証明できる。言い換えれば、$0$ がクラスの元であるかは $P$ と同じ困難さを持つ。基礎命題 $P$ が独立であれば、述語も理論において決定不能である。

クラス $b_P$ の最小元が何であるかを問うことができる。クラスが充足されているので、最小数存在を否定することはできない。実際、$Q_P(1)$ との連言が自明であることから、$Q_P$ を満たす最小数の存在主張は $P$ に対する排中律の命題に翻訳される。その数の値を知ることは、$P$ が成立するかどうかを決定する。したがって独立な $P$ に対して、$Q_P$ を持つ最小数原理の例も $𝖧𝖠$ から独立している。

集合論の記法では、$P$ は $b_P=\{0,1\}$ とも同値であり、その否定は $b_P=\{1\}$ と同値である。これは難解な述語が難解な部分集合を定義できることを示す。したがってテンプレート:仮リンクにおいても、自然数のクラス上の標準的な順序は決定可能であるが、自然数は整列していない。しかし、実現不可能な存在主張を構成的に含意しない強帰納法原理は依然として利用可能である。

反古典的拡張

計算可能な文脈において、述語 $M$ に対して古典的に自明な無限論理和

$\mathrm{\forall }n.(M(n)\vee \mathrm{\neg }M(n))$

（${\mathrm{D}\mathrm{e}\mathrm{c}}_M$ とも書かれる）は、決定問題の決定可能性の検証として読むことができる。クラス記法では、$M(n)$ は $n\in M$ とも書かれる。

$𝖧𝖠$ は $𝖯𝖠$ で証明されない命題は証明しないので、特に古典理論の定理を否定しない。しかし、$𝖧𝖠+\mathrm{\neg }{\mathrm{D}\mathrm{e}\mathrm{c}}_M$ の公理系が無矛盾であるような述語 $M$ も存在する。構成的には、そのような否定は $M(t)$ に対する排中律の特定の数値的反例 $t$ の存在と同値でない。実際、最小論理はすでにすべての命題に対して二重否定された排中律を証明し、したがって任意の述語 $Q$ に対して $\mathrm{\forall }n.\mathrm{\neg }\mathrm{\neg }(Q(n)\vee \mathrm{\neg }Q(n))$（これは $\mathrm{\neg }\mathrm{\exists }n.\mathrm{\neg }(Q(n)\vee \mathrm{\neg }Q(n))$ と同値）が成立する。

チャーチのテーゼ

チャーチ規則は $𝖧𝖠$ において許容規則である。テンプレート:仮リンク原理 ${\mathrm{C}\mathrm{T}}_0$ は $𝖧𝖠$ において採用できるが、$𝖯𝖠$ はこれを否定する：この原理は先述したような否定を含意する。

この原理を、論理の意味で上述のように決定可能な述語はすべて計算可能関数によっても決定可能であると述べる形で考える。これが排中律と矛盾することを見るには、計算可能に決定不能な述語を定義するだけでよい。このために、テンプレート:仮リンクから定義される述語に対して ${\mathrm{\Delta }}_e(w):=T_1(e,e,w)$ と書く。計算可能な全域関数のインデックス $e$ は $\mathrm{\forall }x.\mathrm{\exists }w.T_1(e,x,w)$ を満たす。$T_1$ は原始再帰的な様式で実現できるが、$e$ における述語 $\mathrm{\exists }w.{\mathrm{\Delta }}_e(w)$、すなわち対角線上での停止を記述する証拠を持つ部分計算可能関数のインデックスのクラス $H:=\{e\mid \mathrm{\exists }w.{\mathrm{\Delta }}_e(w)\}$ は計算可能に列挙可能だが計算可能ではない。$\mathrm{\neg }\mathrm{\exists }w.{\mathrm{\Delta }}_e(w)$ を用いて定義された古典的補集合 $M$ は計算可能に列挙さえできない（停止性問題を参照）。この証明可能に決定不能な問題 $e\in M$ が違反例を与える。任意のインデックス $e$ に対して、同値形 $\mathrm{\forall }w.\mathrm{\neg }{\mathrm{\Delta }}_e(w)$ は対応する関数が（$e$ において）評価されるとき、すべての考えうる評価履歴の記述（$w$）が問題の評価を記述しないことを表す。特に、関数に対してこれが決定不能であることは、$\mathrm{W}\mathrm{L}\mathrm{P}\mathrm{O}$ に相当するものの否定を確立する。

形式的なチャーチ原理は自然に再帰学派と結びついている。マルコフの原理 ${\mathrm{M}\mathrm{P}}_{\mathrm{D}\mathrm{e}\mathrm{c}}$ は、その学派によっても、より広く構成的数学によっても一般に採用されている。チャーチ原理の存在下では、${\mathrm{M}\mathrm{P}}_{\mathrm{D}\mathrm{e}\mathrm{c}}$ はその弱形 ${\mathrm{M}\mathrm{P}}_{\mathrm{P}\mathrm{R}}$ と同値である。後者は一般に $\mathrm{\neg }\mathrm{\neg }\mathrm{\exists }w.T_1(e,x,w)$ に対する二重否定除去として単一公理で表現できる。${\mathrm{M}\mathrm{P}}_{\mathrm{D}\mathrm{e}\mathrm{c}}$+${\mathrm{E}\mathrm{C}\mathrm{T}}_0$ の両方を持つハイティング算術は、決定可能述語に対する前提の独立性 ${\mathrm{I}\mathrm{P}}_0$ を証明する。しかし、$\mathrm{I}\mathrm{P}$ とは無矛盾に共存しない。${\mathrm{C}\mathrm{T}}_0$ は $\mathrm{D}\mathrm{N}\mathrm{S}$ も否定する。ライツェン・エヒベルトゥス・ヤン・ブラウワーの直観主義学派は、$\mathrm{P}\mathrm{E}\mathrm{M}$ と ${\mathrm{C}\mathrm{T}}_0$ の両方を否定する原理の集まりによってハイティング算術を拡張する。

モデル

実現可能性

メタ理論における数 $\mathrm{n}$ に対して、研究対象の対象理論における数詞を $\underset{\_}{\mathrm{n}}$ と表記する。

直観主義的算術では、論理和性質 $\mathrm{D}\mathrm{P}$ が典型的に有効である。そして、それが成立する算術の任意の帰納的可算な拡張は数値的存在性質 $\mathrm{N}\mathrm{E}\mathrm{P}$ も持つという定理がある：

$𝖧𝖠⊢\mathrm{\exists }n.\psi (n)⟺\text{ある }\mathrm{n}\text{ が存在して }𝖧𝖠⊢\psi (\underset{\_}{\mathrm{n}})$

したがって、これらの性質はハイティング算術においてメタ論理的に同値である。存在性質と論理和性質は実際、テンプレート:仮リンク $\alpha$ によって存在主張を相対化した場合、すなわち証明可能な $\alpha \to \mathrm{\exists }n.\psi (n)$ に対しても成立する。

クリーネはチャーチの学生であり、ハイティング算術の重要な実現可能性モデルを導入した。その弟子テンプレート:仮リンクは（$𝖧𝖠$ の拡張において）、$𝖧𝖠$ のすべての閉じた定理（すべての変数が束縛されているという意味で）が実現可能であることを確立した。ハイティング算術における推論は実現可能性を保存する。さらに、$𝖧𝖠⊢\mathrm{\forall }n.\mathrm{\exists }m.\phi (n,m)$ であれば、その関数が $\mathrm{n}$ で評価されて $\mathrm{m}$ を結果とするとき $𝖧𝖠⊢\phi (\underset{\_}{\mathrm{n}},\underset{\_}{\mathrm{m}})$ となる意味で $\phi$ を実現する部分再帰関数が存在する。これは任意有限個の関数引数 $\mathrm{n}$ に対して拡張できる。また、$𝖧𝖠$-証明不可能だが実現を持つ古典的定理も存在する。

型付き実現可能性はゲオルク・クライゼルによって導入された。これを用いて彼は、直観主義的理論に対して古典的に有効なマルコフの原理の独立性を示した。

テンプレート:仮リンクとテンプレート:仮リンクも参照せよ。

テンプレート:仮リンクにおいて、帰納法を ${\mathrm{\Sigma }}_1$ に制限したハイティング算術の有限公理化可能な部分体系はすでにテンプレート:仮リンクである。ここでの圏論性はテンプレート:仮リンクを連想させる。このモデルは $𝖧𝖠$ を検証するが $𝖯𝖠$ は検証しないため、この文脈では完全性が失敗する。

無矛盾性と健全性

理論が無矛盾であれば、矛盾の証明は存在しない。クルト・ゲーデルは否定翻訳を導入し、ハイティング算術が無矛盾であればペアノ算術も無矛盾であることを証明した。すなわち、$𝖯𝖠$ の無矛盾性の課題を $𝖧𝖠$ の課題に帰着させた。しかし、特定の理論が自身の無矛盾性を証明できないことについてのゲーデルの不完全性定理は、ハイティング算術自身にも適用される。

$𝖧𝖠$ または数値的存在性質 $\mathrm{N}\mathrm{E}\mathrm{P}$ を持つその任意の無矛盾拡張は自動的に ${\mathrm{\Sigma }}_1^0$-健全でもある（逆に、この性質は健全性を要求する。たとえば、$𝖯𝖠+\mathrm{\neg }{\mathrm{C}\mathrm{o}\mathrm{n}}_{𝖯𝖠}$ は実際には $𝖯𝖠$ と等無矛盾だが、$𝖧𝖠$ を使った対応物はすでに不健全であり、したがって $\mathrm{N}\mathrm{E}\mathrm{P}$ を持たない）。

古典的一階理論 $𝖯𝖠$ の標準モデルおよびそのテンプレート:仮リンクのいずれも、ハイティング算術 $𝖧𝖠$ のモデルでもある。

集合論

完全な $𝖧𝖠$ とその想定された意味論に対するテンプレート:仮リンクのモデルも存在する。比較的弱い集合論で十分である：無限公理を採用して $\omega$ における算術論理式の帰納法を証明し、テンプレート:仮リンクと再帰的定義のための有限域上の関数空間の存在を採用する。特に、これらの理論は $\mathrm{P}\mathrm{E}\mathrm{M}$、完全な分出公理やテンプレート:仮リンク（ましてや正則性公理）、一般的な関数空間（ましてや完全な冪集合公理）を必要としない。

$𝖧𝖠$ はさらに、順序数のクラスが $\omega$ であるような弱い構成的集合論と双解釈可能であり、そのため von Neumann 自然数のコレクションはその理論において集合として存在しない。メタ理論的には、その理論の領域はその順序数のクラスと同じ大きさであり、本質的に自然数 $n\in \omega$ と全単射になれるすべての集合のクラス $\mathrm{F}\mathrm{i}\mathrm{n}$ によって与えられる。公理としてはこれは $V=\mathrm{F}\mathrm{i}\mathrm{n}$ と呼ばれ、他の公理は集合代数と順序に関連するもの：合併と二項共通部分（述語的分離図式と密接に関連する）、外延性、対集合、および集合帰納法図式である。この理論は、強無限公理なしの $𝖢𝖹𝖥$ に有限性公理を加えた理論と同一である。この集合論における $𝖧𝖠$ の議論はモデル理論と同様である。逆方向では、集合論的公理は原始再帰的関係

$x\in y⟺\mathrm{\exists }(r<2^x).\mathrm{\exists }(s<y).(2^x(2s+1)+r=y)$

について証明される。この小さな集合の宇宙は、互いの所属関係を符号化する有限2進列の順序付きコレクションとして理解できる。たとえば、$100_2$番目の集合は一つの別の集合を含み、$110101_2$番目の集合は四つの別の集合を含む。テンプレート:仮リンクを参照せよ。

型理論

型理論的な実現は、推論規則に基づく論理的形式化を反映しており、テンプレート:仮リンクで実装されている。

拡張

ハイティング算術は、原始再帰関数に対する潜在的な関数記号を追加した形で議論されてきた。その理論はアッカーマン関数の全域性を証明する。

これを超えて、公理と形式主義の選択は構成主義的な枠組みの中でさえも常に議論の的であった。$𝖧𝖠$ の多くの型付き拡張が証明論で広く研究されてきた。たとえば、数から数への関数の型、さらにその間の関数の型などを含む。形式的側面は当然複雑になり、関数の適用を支配するさまざまな可能な公理が存在する。全域となる関数のクラスをこの方法で豊かにすることができる。有限型を持つ理論 ${𝖧𝖠}^{\omega }$ は、関数の外延性公理と ${\mathbb{N}}^{\mathbb{N}}$ における選択公理を組み合わせても、$𝖧𝖠$ と同じ算術論理式を証明し、型論理的解釈を持つ。しかし、その理論は ${\mathbb{N}}^{\mathbb{N}}$ に対するチャーチのテーゼを否定し、${\mathbb{N}}^{\mathbb{N}}\to \mathbb{N}$ のすべての関数が連続であるという主張も否定する。しかし、異なる外延性規則、選択公理、マルコフの原理、前提の独立性原理、さらにはケーニヒの補題を——それぞれ特定の強さやレベルで——すべて組み合わせて採用することで、それでもなお ${\mathrm{\Pi }}_1^0$-論理式のレベルで排中律を証明できないような非常に「詰め込まれた」算術を定義することができる。早期には、内包的等号とテンプレート:仮リンクを持つ変形も研究された。

逆数学による構成的二階算術の研究も行われている。

歴史

この理論の形式的公理化はアレン・ハイティング（1930年）、エルブラン、クリーネに遡る。ゲーデルは1933年に $𝖯𝖠$ に関する無矛盾性の結果を証明した。

関連概念

ハイティング算術はハイティング代数と混同すべきでない。ハイティング代数はブール代数の直観主義的類似物である。

関連項目

• テンプレート:仮リンク
• テンプレート:仮リンク
• テンプレート:仮リンク
• テンプレート:仮リンク
• 実現可能性 (論理学)

脚注

• ウルリッヒ・コーレンバッハ（2008年）、Applied proof theory、Springer。
• アンヌ・S・トロエルストラ編（1973年）、Metamathematical investigation of intuitionistic arithmetic and analysis、Springer。

外部リンク

• スタンフォード哲学百科事典: "Intuitionistic Number Theory" by Joan Moschovakis。
• Fragments of Heyting Arithmetic by Wolfgang Burr