ヘイティング算術

数理論理学において、ハイティング算術は 直観主義の哲学に従った算術の公理化である。^{[1]最初にそれを提案した}アーレント・ハイティング にちなんで名付けられた。 ${\displaystyle {\mathsf {HA}}}$

ハイティング算術は、推論に直観主義述語計算を使用する点を除いて、ペアノ算術の第一階 理論とまったく同じように特徴付けることができます。特に、これは二重否定除去原理と排中律原理が成り立たないことを意味します。が正確に成り立たないと言うことは、排中律の命題がすべての命題に対して自動的に証明できるわけではないことを意味していることに注意してください。実際、そのような命題の多くは でまだ証明可能であり、そのような選言の否定は矛盾しています。 は、すべての-定理が - 定理でもあるという意味で、よりも厳密に強いです。 ${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathsf {IQC}}}$ ${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {PA}}}$

ハイティング算術はペアノ算術の公理から成り、意図されたモデルは自然数 の集合です。署名にはゼロ「」と後続の「」が含まれ、理論は加算と乗算を特徴付けます。これはロジックに影響します。 の場合、これはとして定義できるメタ定理であり、したがって はすべての命題 に対してです。 の否定はの形式であり、したがって自明な命題です。 ${\displaystyle {\mathbb {N} }}$${\displaystyle 0}$${\displaystyle S}$${\displaystyle 1:=S0}$${\displaystyle \bot }$${\displaystyle 0=1}$${\displaystyle \neg P}$${\displaystyle P\to \bot }$${\displaystyle P}$${\displaystyle \bot }$${\displaystyle P\to P}$

項については、について と書きます。固定された項 については、等式は反射性により真であり、命題はと同等です。は として定義できることを示すことができます。この形式的な選言の除去は、量指定子のない原始再帰算術では不可能でした。理論は、任意の原始再帰関数の関数記号を使用して拡張することができ、この理論の一部を形成することもできます。全関数 については、 という形式の述語がしばしば考慮されます。 ${\displaystyle s\neq t}$${\displaystyle \neg (s=t)}$${\displaystyle t}$${\displaystyle t=t}$${\displaystyle P}$${\displaystyle (t=t)\to P}$${\displaystyle P\lor Q}$${\displaystyle \exists n.(n=0\to P)\land (n\neq 0\to Q)}$ ${\displaystyle {\mathsf {PRA}}}$${\displaystyle {\mathsf {PRA}}}$${\displaystyle f}$${\displaystyle f(n)=0}$

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

二重否定はを伴います。したがって、 の形式の定理は、（肯定的な）ステートメント を決定的に拒否するための新しい手段も常に提供します。 ${\displaystyle \neg \neg P}$${\displaystyle (\alpha \to \neg P)\to (\alpha \to 0=1)}$${\displaystyle \neg \neg P}$${\displaystyle \alpha }$

における含意は古典的には逆にすることができ、それとともに における含意も逆にすることができることを思い出してください。ここでの区別は、すべての数に対して有効であると仮定した場合の数値的な反例の存在と不合理な結論との間です。二重否定を挿入すると、-定理は-定理になります。より正確には、 で証明可能な任意の式について、その式の古典的に同等なゲーデル–ゲンツェンの否定変換は、 で既に証明可能です。1 つの定式化では、変換手順には をに書き直すことが含まれます。結果は、すべてのペアノ算術定理が、構成的証明とそれに続く古典的な論理的書き直しからなる証明を持つことを意味します。大まかに言えば、最後のステップは二重否定の除去の応用に相当します。 ${\displaystyle {\mathsf {HA}}\vdash \alpha \to \neg \neg \alpha }$ ${\displaystyle {\mathsf {HA}}\vdash {\big (}\exists n.\neg \psi (n){\big )}\to \neg \forall n.\psi (n)}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\big (}\exists n.Q(n){\big )}^{N}}$${\displaystyle \neg \forall n.\neg Q^{N}(n).}$

特に、決定不可能な原子命題が存在しないため、存在量化や選言をまったく含まない任意の命題に対して、 が成り立ちます。 ${\displaystyle \psi }$${\displaystyle {\mathsf {PA}}\vdash \psi \iff {\mathsf {HA}}\vdash \psi }$

最小論理は、否定された式 の二重否定消去を証明します。より一般的には、ヘイティング算術は、任意のハロップ式のこの古典的な同値性を証明します。 ${\displaystyle \neg \neg (\neg \alpha )\leftrightarrow (\neg \alpha )}$

そして、結果も適切に処理されます。算術階層の最下層におけるマルコフ則は、推論の許容規則です。つまり、自由の場合、 ${\displaystyle \Sigma _{1}^{0}}$${\displaystyle \varphi }$${\displaystyle n}$

${\displaystyle {\mathsf {HA}}\vdash \neg \neg \exists m.\varphi (n,m)\iff {\mathsf {HA}}\vdash \exists m.\varphi (n,m)}$

量指定子のない述語について語る代わりに、これを、それぞれ およびと呼ばれる原始再帰述語 またはKleene の T 述語に対して同等に定式化することができます。 の扱いやすさの側面が、例えば構文条件に基づくのではなく、左辺でも を必要とするような関連規則も許容されます。 ${\displaystyle {\mathrm {MR} }_{\mathrm {QF} }}$${\displaystyle {\mathrm {MR} _{\mathrm {PR} }}}$${\displaystyle {\mathrm {MR} _{0}}}$${\displaystyle {\mathrm {MR} }_{\mathrm {Dec} }}$${\displaystyle \varphi }$${\displaystyle \vdash \forall m.\varphi (n,m)\lor \neg \varphi (n,m)}$

命題をその統語形式に基づいて分類する際には、単に古典的な有効な同等性に基づいて、誤って低い複雑性を割り当てないように注意してください。

直観主義論理の他の理論と同様に、この構成的算術では のさまざまな例を証明できます。選言導入により、命題または のいずれかが証明されるときはいつでも、も証明されます。 したがって、たとえば、と を公理から装備すると、述語 に対する排中律の帰納法の前提を検証できます。 このとき、ゼロへの等号は決定可能であると言えます。 実際、 は、すべての数、つまり に対して等号 " " が決定可能であることを証明します。 さらに強力に、等号は Heyting 算術における唯一の述語記号であるため、が自由変数である任意の量指定子のない式に対して、理論は次の規則の下で閉じていること が分かります。${\displaystyle {\mathrm {PEM} }}$${\displaystyle P}$${\displaystyle \neg P}$${\displaystyle P\lor \neg P}$${\displaystyle 0=0}$${\displaystyle \forall n.Sn\neq 0}$${\displaystyle n=0}$${\displaystyle {\mathsf {HA}}}$${\displaystyle =}$${\displaystyle \forall n.\forall m.(n=m\lor n\neq m)}$${\displaystyle \phi }$${\displaystyle n,\dots ,m}$

${\displaystyle {\mathsf {HA}}\vdash \forall n.\cdots \forall m.\,\phi (n,\dots ,m)\lor \neg \phi (n,\dots ,m)}$

最小論理に関する理論は、すべての命題に対して証明されます。したがって、理論が一貫している場合、排中律の否定を証明することは決してありません。 ${\displaystyle \neg \neg (P\lor \neg P)}$

実際には、 などのかなり保守的な構成的フレームワークでは、どのようなタイプのステートメントがアルゴリズム的に決定可能であるかが理解されている場合、排中選言の証明不可能性の結果は のアルゴリズム的決定不可能性を表します。 ${\displaystyle {\mathsf {HA}}}$${\displaystyle P}$

単純なステートメントの場合、理論はそのような古典的に有効な二分法を単に検証するだけではありません。フリードマン変換を使用すると、の定理はすべて によって証明されます。任意の および量指定子のないに対して、 ${\displaystyle \phi (n,\dots )\lor \neg \phi (n,\dots )}$${\displaystyle {\mathsf {PA}}}$${\displaystyle \Pi _{2}^{0}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle n}$${\displaystyle \varphi }$

${\displaystyle {\mathsf {PA}}\vdash \exists m.\varphi (n,m)\iff {\mathsf {HA}}\vdash \exists m.\varphi (n,m)}$

この結果は、もちろん明示的な普遍閉包 で表現することもできます。大まかに言えば、古典的に証明可能な計算可能な関係についての単純なステートメントは、すでに構成的に証明可能です。停止問題では、量指定子のない命題だけでなく -命題も重要な役割を果たしますが、後述するように、これらは古典的に独立している場合もあります。同様に、無限領域におけるすでに唯一の存在、つまり は、形式的には特に単純ではありません。 ${\displaystyle \forall n}$${\displaystyle \Pi _{1}^{0}}$${\displaystyle \exists !n.Q(n)}$${\displaystyle \exists n.\forall w.{\big (}n=w\leftrightarrow Q(w){\big )}}$

は に対して-保存的である。対照的に、ロビンソン算術の古典理論はすべての-定理を証明しているが、いくつかの単純な-定理はそれに依存しない。帰納法はフリードマンの結果でも重要な役割を果たしている。例えば、順序付けとオプションで決定可能な等式に関する公理で強化することで得られるより実用的な理論は、その直観主義的な対応物よりも多くの - 文を証明している。 ${\displaystyle {\mathsf {PA}}}$${\displaystyle \Pi _{2}^{0}}$${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathsf {Q}}}$${\displaystyle \Sigma _{1}^{0}}$${\displaystyle {\mathsf {PA}}}$${\displaystyle \Pi _{1}^{0}}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {Q}}}$${\displaystyle \Pi _{2}^{0}}$

ここでの議論は決して網羅的ではありません。古典的な定理が構成的理論によってすでに導かれる場合、さまざまな結果があります。また、メタ論理的結果を得るためにどのロジックが使用されたかが関係する場合があることに注意してください。たとえば、実現可能性に関する多くの結果は、確かに構成的メタ論理で得られました。ただし、特定のコンテキストが指定されていない場合は、述べられた結果は古典的なものであると想定する必要があります。

独立性の結果は、理論ではその命題もその否定も証明できない命題に関係します。古典理論が矛盾せず（つまり、 を証明しない）、構成的対応物がその古典定理の 1 つを証明しない場合、それは後者から独立しています。いくつかの独立した命題が与えられれば、特に構成的フレームワークでは、それらからさらに定義することは簡単です。 ${\displaystyle \bot }$${\displaystyle P}$${\displaystyle P}$

ヘイティング算術は選言性質 を持つ：すべての命題とに対して、^[2]${\displaystyle {\mathrm {DP} }}$${\displaystyle \alpha }$${\displaystyle \beta }$

${\displaystyle {\mathsf {HA}}\vdash \alpha \lor \beta \iff {\mathsf {HA}}\vdash \alpha {\text{ or }}{\mathsf {HA}}\vdash \beta }$

実際、これとその数値的一般化は、構成的2階算術や、やなどの一般的な集合論によっても示されます。これは、構成的理論という非公式な概念に対する共通の要望です。 さて、 を持つ理論では、命題が独立 である場合、古典的に自明な は別の独立した命題であり、その逆も同様です。証明できないインスタンスが少なくとも1つある場合、スキーマは有効ではありません。これが、 が失敗する理由です。 の場合のように、どちらの選言も検証せずに排中律を公理的に採用することで、スキーマを破ることができます。 ${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {IZF}}}$${\displaystyle {\mathrm {DP} }}$${\displaystyle P}$${\displaystyle P\lor \neg P}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathrm {DP} }}$${\displaystyle {\mathsf {PA}}}$

さらに、が古典的に独立している場合、否定も独立しています。これは、 が と同等であるかどうかに関係なく当てはまります。すると、構成的に、弱い排中律は成立しません。つまり、すべての命題に当てはまる原理は有効ではありません。そのような の場合、選言の証明不可能性は、 -の破綻、つまり原始再帰関数 の の例 に相当します。${\displaystyle P}$${\displaystyle \neg P}$${\displaystyle \neg \neg P}$${\displaystyle P}$${\displaystyle {\mathrm {WPEM} }}$${\displaystyle \neg \alpha \lor \neg \neg \alpha }$${\displaystyle P}$${\displaystyle \Sigma _{1}^{0}}$${\displaystyle \Pi _{1}^{0}}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathrm {WLPO} }}$

ゲーデルの不完全性定理の知識は、 -証明可能だが-証明可能ではないタイプのステートメントを理解するのに役立ちます。 ${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {HA}}}$

ヒルベルトの第10問題の解決により、いくつかの具体的な多項式とそれに対応する多項式方程式が提示され、後者が解を持つという主張はアルゴリズム的に決定不可能である。この命題は次のように表現できる。 ${\displaystyle f}$

${\displaystyle \exists w_{1}.\cdots \exists w_{n}.f(w_{1},\dots ,w_{n})=0}$

ゼロ値の存在の主張には、より特殊な解釈があります。 またはなどの理論は、これらの命題が理論自身の矛盾の算術的主張と同等であることを証明します。 したがって、このような命題は、強力な古典的な集合論に対しても記述できます。 ${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {ZFC}}}$

首尾一貫した健全な算術理論では、そのような存在の主張は独立した-命題です。すると、 は、量指定子を通して否定を押すことで、独立したゴールドバッハ型の- または-命題であることがわかります。明示的に言うと、二重否定(または) も独立しています。また、いずれにせよ、任意の三重否定は、すでに直観的には単一の否定と同等です。 ${\displaystyle {\mathrm {I} _{f}}}$${\displaystyle \Sigma _{1}^{0}}$${\displaystyle {\mathrm {C} _{f}}:=\neg {\mathrm {I} _{f}}}$${\displaystyle \Pi _{1}^{0}}$${\displaystyle \neg \neg {\mathrm {I} _{f}}}$${\displaystyle \neg {\mathrm {C} _{f}}}$

以下は、このような独立したステートメントに含まれる意味を明らかにします。理論のすべての証明の列挙におけるインデックスが与えられている場合、それがどの命題の証明であるかを調べることができます。 は、この手順を正しく表すことができるという点で適切です。つまり、証明が不合理な命題 の 1 つであることを表す原始的な再帰述語が存在します。これは、多項式の戻り値がゼロであることに関する、上記のより明示的な算術述語に関連します。 が整合している場合、すべての個別のインデックス に対してが実際に証明されるとメタ論理的に推論できます。 ${\displaystyle {\mathsf {PA}}}$${\displaystyle \mathrm {F} (w):=\mathrm {Prf} (w,\ulcorner 0=1\urcorner )}$${\displaystyle 0=1}$${\displaystyle {\mathsf {PA}}}$${\displaystyle \neg \mathrm {F} ({\underline {\mathrm {w} }})}$${\displaystyle {\mathrm {w} }}$

事実上公理化された理論では、各証明を順に検証することができます。理論が実際に一貫している場合、不合理性の証明は存在しません。これは、前述の「不合理性の探索」が決して停止しないというステートメントに対応します。理論では、形式的には、前者は命題 によって表現され、算術的矛盾の主張を否定します。同等の命題 は、すべての証明が不合理性の証明ではないと述べることによって、探索が決して停止しないことを形式化します。そして確かに、証明可能性を正確に表すオメガ一貫性のある理論では、不合理性の探索が停止して終了するという証明はありません (明示的な矛盾は導出できません)。また、ゲーデルによって示されたように、不合理性の探索が決して停止しないという証明も存在しません (一貫性は導出できません)。言い換えると、不合理探索が決して停止しないという証明は存在しない (一貫性は導出不可能)。また、不合理探索が決して停止しないという証明も存在しない (一貫性は拒否不可能)。繰り返すと、これら 2 つの選言はどちらも-証明可能ではないが、その選言は自明に -証明可能である。確かに、が一貫している場合、 は に違反する。 ${\displaystyle \neg \exists w.\mathrm {F} (w)}$${\displaystyle \Pi _{1}^{0}}$${\displaystyle \forall w.\neg \mathrm {F} (w)}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathrm {DP} }}$

の証明の存在を表す -命題は、論理的に肯定的なステートメントです。それにもかかわらず、これは歴史的に と表記され、その否定はと表記される -命題です。建設的な文脈では、この否定記号の使用は誤解を招く命名法になる可能性があります。 ${\displaystyle \Sigma _{1}^{0}}$${\displaystyle 0=1}$${\displaystyle \neg {\mathrm {Con} }_{\mathsf {PA}}}$${\displaystyle \Pi _{1}^{0}}$${\displaystyle {\mathrm {Con} }_{\mathsf {PA}}}$

フリードマンは、もう一つの興味深い証明不可能な主張を確立しました。それは、一貫性があり適切な理論は、その算術的選言特性を決して証明しない、という主張です。

すでに極小論理は、すべての矛盾のない主張、特に とを論理的に証明しています。 であるため、定理は証明可能な二重否定の排中論理和 (または存在主張) として読むことができます。 しかし、論理和の性質を考慮すると、単純な排中論理和は-証明可能ではありません。 そのため、ド・モルガンの法則の 1 つは、一般に直観的に成立することもできません。 ${\displaystyle \neg ({\mathrm {I} _{f}}\land \neg {\mathrm {I} _{f}})}$${\displaystyle \neg ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})}$${\displaystyle ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})\leftrightarrow \neg ({\mathrm {I} _{f}}\lor \neg {\mathrm {I} _{f}})}$${\displaystyle \neg ({\mathrm {C} _{f}}\land \neg {\mathrm {C} _{f}})}$${\displaystyle {\mathrm {C} _{f}}\lor \neg {\mathrm {C} _{f}}}$${\displaystyle {\mathsf {HA}}}$

原理との内訳は説明済みです。 では、最小数原理は、帰納原理と同等の多くのステートメントの 1 つにすぎません。以下の証明は、 がを意味すること、したがってこの原理が においても一般に有効ではない理由を示しています。ただし、 で表されるすべての非自明な述語に対して二重否定最小数の存在を許すスキームは、一般に有効です。ゲーデルの証明に照らし合わせると、これら 3 つの原理の内訳は、ハイティング算術が構成的論理の証明可能性の解釈と一致するものとして理解できます。 ${\displaystyle {\mathrm {WPEM} }}$${\displaystyle {\mathrm {WLPO} }}$${\displaystyle {\mathsf {PA}}}$ ${\displaystyle {\mathrm {LNP} }}$${\displaystyle {\mathrm {LNP} }}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathsf {HA}}}$${\displaystyle \neg \neg {\mathrm {LNP} }}$

原始再帰述語に対するマルコフの原理は、厳密に強い は言うまでもなく、の含意スキーマとしても成立しません。対応する規則の形では、前述のようにそれらは許容されます。同様に、理論は、すべての否定命題に対する規則の下で閉じている、つまり の存在量指定子を取り出すことができるにもかかわらず、否定述語に対する前提の独立性の原理を証明しません。存在ステートメントが単なる選言に置き換えられたバージョンについても同じことが当てはまります。 ${\displaystyle {\mathrm {MP} _{\mathrm {PR} }}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$${\displaystyle {\mathrm {IP} }}$${\displaystyle \neg P\to \exists n.Q(n)}$

有効な含意は、選言三段論法を使用して、逆の形式でも成り立つことが証明できます。ただし、二重否定シフト、つまりすべての数に対する全称量化による「 」の可換性の図式は直観的に証明できません。これは、チャーチのテーゼのセクションで説明したように、一部の に対するの一貫性によって説明される興味深い分析です。 ${\displaystyle \neg \neg (\alpha \to \beta )\to (\alpha \to \neg \neg \beta )}$${\displaystyle {\mathrm {DNS} }}$${\displaystyle \neg \neg }$${\displaystyle \neg {\mathrm {Dec} _{M}}}$${\displaystyle M}$

自然数の順序関係を利用すると、強い帰納原理は次のように表される。

${\displaystyle \forall n.{\Big (}{\big (}\forall (k<n).\phi (k){\big )}\,\to \,\phi (n){\Big )}\,\to \,\forall m.\phi (m)}$

集合論でおなじみのクラス表記では、算術文は と表現されます。否定形の述語、つまり に対して、帰納法と同等の論理式は次のようになります 。${\displaystyle Q(n)}$${\displaystyle n\in B}$${\displaystyle B:=\{m\in {\mathbb {N} }\mid Q(m)\}}$${\displaystyle \phi (n):=\neg (n\in B)}$

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

洞察は、サブクラス の中で、最小のメンバーが存在しない (証明可能) という特性は、無人であること、つまり空のクラスであることと同等であるということです。 逆否定をとると、空でないサブクラスに対して、より小さいメンバーが存在しないようなメンバーが存在する可能性を一貫して排除できないことを表す定理が導かれます。 ${\displaystyle B\subseteq {\mathbb {N} }}$${\displaystyle n\in B}$${\displaystyle k\in B}$${\displaystyle n}$

${\displaystyle B\neq \{\}\,\to \,\neg \neg \exists (n\in B).\neg \exists (k\in B).k<n}$

ペアノ算術では、二重否定の除去が常に有効であり、これは一般的な定式化における最小数原理を証明します。古典的な解釈では、空でないことは、（証明可能に）何らかの最小の要素が存在することと同等です。

上記の形式の強い帰納スキーマを検証する二項関係「 」は常に非反射的でもある。または同等に ${\displaystyle <}$${\displaystyle \phi _{c}(n):=(n\neq c)}$

${\displaystyle Q_{c}(n):=(n=c)}$

ある固定された数 に対して、上記は のどの要素もを成立させない、つまり というステートメントに簡略化されます。(そして、この論理的演繹は、二項関係の他のどの特性も使用していません。) より一般的には、 が空でなく、関連する(古典的な)最小数原理を使用して否定形式のステートメント( など)を証明できる場合、これを完全に構成的な証明に拡張できます。これは、含意が常に形式的に強い と直観的に同等であるためです。 ${\displaystyle c}$${\displaystyle k}$${\displaystyle B=\{c\}}$${\displaystyle k<c}$${\displaystyle \neg (c<c)}$${\displaystyle B}$${\displaystyle \neg (c<c)}$${\displaystyle \alpha \to \neg \beta }$${\displaystyle (\neg \neg \alpha )\to \neg \beta }$

しかし、一般的には、構成的論理では、最小数原理の弱体化は解除できない。次の例がこれを示している。ある命題（例えば上記）に対して、述語を考える。 ${\displaystyle P}$${\displaystyle {\mathrm {C} _{f}}}$

${\displaystyle Q_{P}(n):=(n=0\land P)\lor (n=1)}$

これは自然数のサブクラスに対応します。このクラスの最小の要素は何かと問われるかもしれません。このクラスにあると証明された、または仮定された任意の数は、またはに等しいことが証明できます。つまり です。等式の決定可能性と選言三段論法を使用すると、同値 が証明されます。基礎となる命題が 独立している場合、述語は理論で決定不可能です。 であるため、命題は自明に真であり、したがってクラスには が存在します。特に、このクラスの最小数存在は拒否できません。 との連言が自明であると仮定すると、最小数の存在主張はの排中命題に変換されます。そのような数の値を知っていると、実際に が成り立つかどうかが決まります。したがって、 が独立している場合、 を伴う最小数原理インスタンスはとも独立です。 ${\displaystyle Q_{P}}$${\displaystyle b_{P}:=\{z\in \{0\}\mid P\}\cup \{1\}}$${\displaystyle 0}$${\displaystyle 1}$${\displaystyle b_{P}\subseteq \{0,1\}}$${\displaystyle P\leftrightarrow Q_{P}(0)}$${\displaystyle P}$${\displaystyle 1=1}$${\displaystyle Q_{P}(1)}$${\displaystyle 1\in b_{P}}$${\displaystyle Q_{P}(1)}$${\displaystyle Q_{P}}$${\displaystyle P}$${\displaystyle P}$${\displaystyle P}$${\displaystyle Q_{P}}$${\displaystyle {\mathsf {HA}}}$

集合論の表記法では、はと同等であり、したがって であり、その否定も と同等です。これは、とらえどころのない述語がとらえどころのない部分集合を定義できることを示しています。また、構成的集合論でも、自然数のクラス上の標準的な順序は決定可能ですが、自然数は整列していません。しかし、実現不可能な存在の主張を構成的に含まない強力な帰納原理も依然として利用可能です。 ${\displaystyle P}$${\displaystyle 0\in b_{P}}$${\displaystyle b_{P}=\{0,1\}}$${\displaystyle b_{P}=\{1\}}$

計算可能な文脈では、述語 に対して、古典的に自明な無限論理和 ${\displaystyle M}$

${\displaystyle \forall n.{\big (}M(n)\lor \neg M(n){\big )}}$、

は とも表記され、決定問題の決定可能性の検証として読み取ることができます。クラス表記ではは とも表記されます。 ${\displaystyle {\mathrm {Dec} }_{M}}$${\displaystyle M(n)}$${\displaystyle n\in M}$

${\displaystyle {\mathsf {HA}}}$は、 によって証明できない命題を証明しないので、特に、古典理論の定理を否定しません。しかし、公理が矛盾しないような述語も存在します。また、建設的に、そのような否定は、に対する排中律に対する特定の数値反例の存在と同等ではありません。実際、すでに極小論理によって、すべての命題に対して二重否定の排中律が証明されているため、 であり、任意の述語 に対して と同等です。 ${\displaystyle {\mathsf {PA}}}$${\displaystyle M}$${\displaystyle {\mathsf {HA}}+\neg {\mathrm {Dec} }_{M}}$${\displaystyle t}$${\displaystyle M(t)}$${\displaystyle \forall n.\neg \neg {\big (}Q(n)\lor \neg Q(n){\big )}}$${\displaystyle \neg \exists n.\neg {\big (}Q(n)\lor \neg Q(n){\big )}}$${\displaystyle Q}$

チャーチの規則は では許容される規則です。チャーチのテーゼ原理は では採用できますが、 ではそれを拒否します。これは、先ほど説明したような否定を意味します。 ${\displaystyle {\mathsf {HA}}}$ ${\displaystyle {\mathrm {CT} _{0}}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {PA}}}$

上の論理的意味で決定可能なすべての述語は、全計算可能関数によっても決定可能であるという形式の原理について考えます。これが排中律とどのように矛盾するかを確認するには、計算可能決定可能ではない述語を定義すればよいだけです。このために、クリーネの T 述語から定義された述語 について と書きます。全計算可能関数 のインデックスはを満たします。 は原始的な再帰的な方法で実現できますが、の述語、つまり、対角線上で停止する方法を説明する証拠を持つ部分計算可能関数インデックスのクラスは、計算可能列挙可能ですが、 は計算可能ではありません。を使用して定義された古典的な補語は、計算可能列挙さえできません。停止問題を参照してください。この決定不可能であることが証明された問題は、違反の例を提供します。任意のインデックス に対して、同等の形式は、対応する関数が ( で) 評価されるときに、評価履歴 ( ) の考えられるすべての記述が、手元の評価を記述するわけではないことを表します。具体的には、関数 に対してこれが決定可能ではないことは、 に相当するものの否定を確立します。 ${\displaystyle \Delta _{e}(w):=T_{1}(e,e,w)}$${\displaystyle e}$${\displaystyle \forall x.\exists w.T_{1}(e,x,w)}$${\displaystyle T_{1}}$${\displaystyle \exists w.\Delta _{e}(w)}$${\displaystyle e}$${\displaystyle H:=\{e\mid \exists w.\Delta _{e}(w)\}}$${\displaystyle M}$${\displaystyle \neg \exists w.\Delta _{e}(w)}$ ${\displaystyle e\in M}$${\displaystyle e}$${\displaystyle \forall w.\neg \Delta _{e}(w)}$${\displaystyle e}$${\displaystyle w}$${\displaystyle {\mathrm {WLPO} }}$

形式的なチャーチの原理は、当然のことながら、再帰学派と関連している。マルコフの原理は、その学派およびより広い意味での構成的数学によって一般的に採用されている。チャーチの原理が存在する場合、はその弱い形式 と同等である。後者は一般に単一の公理、すなわち任意の に対する二重否定消去法として表現できる。ヘイティング算術を と の両方と組み合わせると、決定可能な述語 の前提の独立性が証明される。しかし、これらは と一貫して一緒には機能しない。 はまた を否定する。LEJブラウワーの直観主義学派は、だけでなく も否定する一連の原理によってヘイティング算術を拡張する。 ${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$${\displaystyle {\mathrm {MP} _{\mathrm {PR} }}}$${\displaystyle \neg \neg \exists w.T_{1}(e,x,w)}$${\displaystyle {\mathrm {MP} _{\mathrm {Dec} }}}$${\displaystyle {\mathrm {ECT} _{0}}}$${\displaystyle {\mathrm {IP} }_{0}}$${\displaystyle {\mathrm {IP} }}$${\displaystyle {\mathrm {CT} _{0}}}$${\displaystyle {\mathrm {DNS} }}$${\displaystyle {\mathrm {PEM} }}$${\displaystyle {\mathrm {CT} _{0}}}$

理論に一貫性があれば、不合理性の証明は存在しない。クルト・ゲーデルは否定変換を導入し、ハイティング算術に一貫性があればペアノ算術も一貫性があることを証明した。つまり、彼は の一貫性の問題をの問題にまで縮小した。しかし、特定の理論が自身の一貫性を証明できないというゲーデルの不完全性定理は、ハイティング算術自体にも当てはまる。 ${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {HA}}}$

古典的な一階理論の標準モデルとその非標準モデルは、Heyting 算術のモデルでもあります。 ${\displaystyle {\mathsf {PA}}}$${\displaystyle {\mathsf {HA}}}$

完全なとその意図された意味論に対する構成的集合論モデルも存在します。比較的弱い集合論で十分です。それらは、における算術式の帰納法を証明するために、無限公理、述語分離の公理スキーム、および再帰的定義に対する有限領域上の関数空間の存在を採用します。具体的には、これらの理論は、完全な分離公理や集合帰納法(正則性公理 は言うまでもなく)、一般的な関数空間 (完全なべき集合 公理 は言うまでもありません)を必要としません。 ${\displaystyle {\mathsf {HA}}}$${\displaystyle \omega }$${\displaystyle {\mathrm {PEM} }}$

${\displaystyle {\mathsf {HA}}}$さらに、は、順序数のクラスが である弱い構成的集合論で双方向に解釈可能であるため、フォン・ノイマン自然数の集合は、理論では集合として存在しない。^{[3] [4]}メタ理論的には、その理論の定義域はその順序数のクラスと同じ大きさであり、本質的には、自然 と一対一であるすべての集合のクラスを通じて与えられる。公理として、これは と呼ばれ、他の公理は集合代数と順序に関連するものである。和集合と二項積集合は、述語的分離スキーマ、外延性、ペアリング、および集合帰納スキーマと密接に関連している。この理論は、強無限大がなく有限公理が追加された によって与えられた理論とすでに同一である。この集合論における の議論は、モデル理論の場合と同様である。そして逆の方向では、集合論的公理は原始再帰関係 に関して証明される。${\displaystyle \omega }$${\displaystyle {\mathrm {Fin} }}$${\displaystyle n\in \omega }$${\displaystyle V={\mathrm {Fin} }}$${\displaystyle {\mathsf {CZF}}}$${\displaystyle {\mathsf {HA}}}$

${\displaystyle x\in y\iff \exists (r<2^{x}).\exists (s<y).{\big (}2^{x}(2s+1)+r=y{\big )}}$

その小さな集合の宇宙は、相互のメンバーシップをエンコードする有限のバイナリ シーケンスの順序付けられたコレクションとして理解できます。たとえば、' 番目の集合には他の 1 つの集合が含まれ、' 番目の集合には他の 4 つの集合が含まれます。BIT述語を参照してください。 ${\displaystyle 100_{2}}$${\displaystyle 110101_{2}}$

メタ理論における何らかの数に対して、研究対象理論における数値は で表されます。 ${\displaystyle \mathrm {n} }$${\displaystyle {\underline {\mathrm {n} }}}$

直観主義的算術では、選言特性は典型的には有効です。そして、それが成り立つ算術の任意のce拡張は数値的存在特性も持つという定理があります。 ${\displaystyle {\mathrm {DP} }}$ ${\displaystyle {\mathrm {NEP} }}$

${\displaystyle {\mathsf {HA}}\vdash \exists n.\psi (n)\iff {\text{ exists }}{\mathrm {n} }{\text{ }}{\mathsf {HA}}\vdash \psi ({\underline {\mathrm {n} }})}$

したがって、これらの特性は、Heyting 算術ではメタ論理的等価です。存在と選言の特性は、実際には、存在の主張をハロップの公式によって相対化する場合でも、つまり、証明可能な に対しても依然として有効です。 ${\displaystyle \alpha }$${\displaystyle \alpha \to \exists n.\psi (n)}$

チャーチの弟子であるクリーネは、ヘイティング算術の重要な実現可能性モデルを導入しました。次に、彼の弟子であるネルス・デイビッド・ネルソンは、（ の拡張において） のすべての閉定理（つまり、すべての変数がバインドされている）が実現可能であることを証明しました。ヘイティング算術における推論は実現可能性を保存します。さらに、 の場合、で評価された関数が で終了するときはいつでもであるという意味でを実現する部分再帰関数が存在します。これは、関数引数 の有限個に拡張できます。-証明可能ではないが実現がある 古典的な定理もあります。${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {HA}}\vdash \forall n.\exists m.\varphi (n,m)}$${\displaystyle \varphi }$${\displaystyle {\mathrm {n} }}$${\displaystyle {\mathrm {m} }}$${\displaystyle {\mathsf {HA}}\vdash \varphi ({\underline {\mathrm {n} }},{\underline {\mathrm {m} }})}$${\displaystyle {\mathrm {n} }}$${\displaystyle {\mathsf {HA}}}$

実現可能性の型付きバージョンは、ゲオルク・クライゼルによって導入されました。これにより、彼は、古典的に有効なマルコフ原理が直観主義理論から独立していることを実証しました。

BHK 解釈およびDialectica 解釈も参照してください。

有効なトポスでは、 に制限された帰納法を持つ Heyting 算術の有限公理化可能なサブシステムはすでにカテゴリカルです。ここでのカテゴリ性はTennenbaum の定理を彷彿とさせます。モデルは を検証しますが は検証しないため、このコンテキストでは 完全性が失われます。${\displaystyle \Sigma _{1}}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {PA}}}$

推論規則に基づく論理形式化を反映した型理論的実現は、さまざまな言語で実装されています。

Heyting 算術は、原始再帰関数に追加された潜在的な関数記号を使用して説明されています。その理論は、Ackermann 関数の合計を証明します。

これ以外にも、公理と形式論の選択は、構成主義者の間でも常に議論の的となってきました。証明理論では、例えば数間の関数の型やそれらの間の関数など、の多くの型付き拡張が広範に研究されてきました。関数の適用を規定するさまざまな公理が考えられ、形式論は当然より複雑になります。関数のクラスが完全であることは、このようにして豊かにすることができます。有限型の理論は、関数の外延性と での選択公理をさらに組み合わせても、同じ算術式が正しいことを証明し、型理論的解釈を持ちます。しかし、その理論は、 に対するチャーチのテーゼと、 のすべての関数が連続するというテーゼを否定します。しかし、たとえば、さまざまな外延性規則、選択公理、マルコフの原理と独立性の原理、さらにはケーニッヒの補題を、すべて一緒に、ただしそれぞれ特定の強度またはレベルで採用すると、式のレベルで排中律を証明できない可能性のある、かなり「詰め込まれた」算術を定義することができます。初期には、内包的等価性とBrouwer選択シーケンスを持つ変種も研究されてきました。 ${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathsf {HA}}^{\omega }}$${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$${\displaystyle {\mathsf {HA}}}$${\displaystyle {\mathbb {N} }^{\mathbb {N} }}$${\displaystyle {\mathbb {N} }^{\mathbb {N} }\to {\mathbb {N} }}$${\displaystyle \Pi _{1}^{0}}$

構成的2階算術の逆数学研究も行われている。 ^[5]

この理論の正式な公理化は、 Heyting (1930)、Herbrand、Kleeneに遡ります。 ゲーデルは1933 年にこの理論に関する一貫性の結果を証明しました。 ${\displaystyle {\mathsf {PA}}}$

ヘイティング算術は、ブール代数の直観主義的類似物であるヘイティング代数と混同しないでください。

• BHKの解釈
• 建設的な分析
• 構成的集合論
• ハロップ式
• 実現可能性

• Ulrich Kohlenbach (2008)、「応用証明理論」、Springer。
• Anne S. Troelstra編 (1973)、『直観主義算術および解析のメタ数学的調査』、Springer、1973年。

• スタンフォード哲学百科事典：「直観主義数論」、ジョアン・モスコバキス著。
• ヴォルフガング・バール著『ヘイティング算術の断片』