Loading article…
数理論理学において、ヘイティング算術これは直観主義の哲学に従った算術の公理化である。[ 1 ] これは最初にそれを提唱したアーレント・ヘイティングにちなんで名付けられた。
ハイティング算術は、ペアノ算術の一次理論と全く同じように特徴づけることができる。ただし、直観主義述語論理を使用している点を除く。推論のために。特に、これは二重否定除去原理と排中律の原理を意味します。保持しない。厳密には成り立たないということは、排中文がすべての命題に対して自動的に証明できるわけではないことを意味する。実際、そのような命題の多くは依然として証明可能である。そして、そのような論理和の否定は矛盾している。より厳密に強いすべてという意味で定理もまた定理。
ハイティング算術はペアノ算術の公理から成り、そのモデルは自然数の集合である。署名にはゼロが含まれています「そして後継者」そして、これらの理論は加算と乗算を特徴づけています。これは論理に影響を与えます。それはメタ定理である定義できるそして、はすべての命題についての否定形式はしたがって、それは自明の命題である。
用語については、のために一定期間平等反射律と命題により真であると同等次のようなことが示されるかもしれない。次のように定義できます。. この形式的な選言の排除は、量化子のない原始的な再帰的算術では不可能であった。この理論は、任意の原始再帰関数の関数記号で拡張することができ、また、この理論の断片でもある。全関数については多くの場合、次のような形式の述語が考えられます。。
直観主義理論では爆発が有効なので、ある定理定義により理論が矛盾している場合に限り、証明可能である。実際、ハイティング算術では、二重否定は明示的に述語の場合、次の形式の定理それは矛盾していると述べています。一部については検証可能建設的に言えば、これはそのような存在の主張よりも弱い。メタ理論的な議論の大部分は、古典的に証明可能な存在主張に関するものとなるだろう。
二重否定伴うという形式の定理また、常に（肯定的な）主張を決定的に拒否する新たな手段を提供する。。
の含意を思い出してください。は古典的に反転することができ、それに伴い、ここでの区別は、数値的な反例の存在と、すべての数値に対して妥当性を仮定した場合の不合理な結論との違いである。二重否定を挿入すると-定理を-定理。より正確には、で証明可能な任意の式に対して古典的に同等なゲーデル・ゲンツェンの否定変換は既に証明可能であり、ある定式化では、翻訳手順には書き換えが含まれる。にこの結果は、すべてのペアノ算術定理には、構成的証明とそれに続く古典的論理的書き換えからなる証明が存在することを意味する。大まかに言えば、最終段階は二重否定除去の適用に相当する。
特に、決定不能な原子命題が存在しない場合、任意の命題に対して存在量化や選言を一切含まないと、。
最小限の論理により、否定式に対する二重否定の除去が証明される。より一般的には、ヘイティング算術は、任意のハロップ公式に対してこの古典的な等価性を証明する。
そして結果も良好です。算術階層の最下層におけるマルコフの規則は、許容可能な推論規則です。つまり、と無料、
量化子なし述語について話す代わりに、これを原始再帰述語またはクリーネのT述語と同等に定式化することができる。、それぞれ。そして関連するルールも許容される、その扱いやすさの側面例えば構文条件に基づくものではなく、左辺も要求する。
命題をその構文形式に基づいて分類する際には、古典的に有効な等価性のみに基づいて、誤って低い複雑性を割り当てないように注意すべきである。
直観主義論理に関する他の理論と同様に、さまざまな事例でこの構成的算術では証明できます。選言導入により、命題がまたは証明されれば、も証明されています。例えば、そして公理から、述語に対する排中律の帰納の前提を検証することができる。すると、ゼロに等しいかどうかは決定可能であると言う。実際、平等を証明するすべての数に対して決定可能である、すなわちさらに、等号はヘイティング算術における唯一の述語記号であるため、任意の量化子を含まない式に対して、次のことが成り立つ。、 どこは自由変数であり、理論は規則の下で閉じている。
最小限の論理を超える理論はすべての命題について。したがって、理論が矛盾していなければ、排中律の否定を証明することは決してない。
実際には、次のような保守的な構成フレームワークではどのような種類のステートメントがアルゴリズム的に決定可能であるかが理解されると、排中論理和の証明不可能性の結果は、アルゴリズム的決定不可能性を表す。。
単純な記述の場合、この理論は、古典的に妥当な二項対立を検証するだけでなく、フリードマン訳は、の-定理はすべて次のように証明されます: いずれの場合も数量詞なし、
この結果は、もちろん明示的な全称閉包を用いて表現することもできる。大まかに言えば、古典的に証明可能な計算可能な関係についての単純な記述は、すでに構成的に証明可能です。停止問題では、量化子のない命題だけでなく、-命題は重要な役割を果たし、後述するように、これらは古典的に独立している場合もある。同様に、すでに一意な存在無限領域において、すなわちは、形式的には特に単純ではない。
それでは保守的これはロビンソン算術の状況とは対照的である。これは帰納法を欠いている点で弱い理論である。まず、古典的なすべてを証明する-定理ですが、いくつかの単純な--定理はすでにそれとは独立している。帰納法はフリードマンの結果において重要な役割を果たしていることがわかる。なぜなら、より実用的な理論は、順序に関する公理と、任意に決定可能な等価性により、直観主義的な主張よりも多くの主張がある。
ここでの議論は決して網羅的なものではありません。古典的な定理が構成的理論によって既に導かれる場合、様々な結果が存在します。また、メタ論理的な結果を得るためにどのような論理が用いられたかも重要となる場合があることにも注意が必要です。例えば、実現可能性に関する多くの結果は、実際に構成的メタ論理によって得られました。しかし、具体的な文脈が示されていない場合は、述べられた結果は古典的なものとみなす必要があります。
独立性の結果は、理論において、その命題もその否定も証明できない命題に関するものです。古典理論が無矛盾である場合（つまり、証明しない場合））そして構成的な対応物は、その古典的な定理の1つを証明しない。そうすればは後者とは独立している。いくつかの独立した命題が与えられれば、特に構成的な枠組みにおいては、それらからさらに多くの命題を定義することは容易である。
ハイティング算術は選言の性質を持つ: すべての命題についてそして[ 2 ]
実際、これと数値的な一般化は、構成的2階算術や一般的な集合論などでも示されています。そしてこれは、非公式な構成理論の概念に対する一般的な要望である。命題がが独立である場合、古典的に自明なは別の独立した命題であり、逆もまた然りです。証明できないインスタンスが少なくとも 1 つある場合、スキーマは有効ではありません。失敗するかもしれない。排中命題を公理的に採用し、どちらの選言子も検証しない場合、。
さらに言うと、もし古典的に独立している場合でも、否定も同様ですは独立している—これは、と同等そして、建設的に、弱い排除中間層成り立たない、つまり、すべての命題に当てはまるという主張は妥当ではありません。は論理和の証明不可能性は、-または、 原始的な再帰関数の場合。
ゲーデルの不完全性定理の知識は、どのような種類の命題が証明可能だが、証明可能。
ヒルベルトの第10問題の解決により、いくつかの具体的な多項式が得られた。そして対応する多項式方程式があり、後者が解を持つという主張はアルゴリズム的に決定不能である。この命題は次のように表現できる。
そのようなゼロ値の存在主張には、より特別な解釈があります。例えば、またはこれらの命題が、理論自身の矛盾を算術的に表現した主張と等価であることを証明します。したがって、このような命題は、強力な古典的集合論についても記述することができます。
一貫性のある健全な算術理論では、そのような存在の主張は独立系―命題。それから量化子を通して否定を押し込むことで、独立したゴールドバッハ型であることがわかります。-命題。明確に言うと、二重否定（または）もまた独立している。そして、いずれにせよ、三重否定は直観的に単一の否定と等価である。
以下に、そのような独立した記述に含まれる意味を明らかにする。ある理論のすべての証明を列挙したリストにおいて、あるインデックスが与えられた場合、それがどの命題の証明であるかを調べることができる。この手順を正しく表現できるという意味で十分である。原始的な再帰述語が存在する。証明が不条理な命題の一つであることを表現するこれは、多項式の戻り値がゼロであるという、上記のより明示的な算術的述語に関連しています。メタ論理的に考えると、一貫しているならば、それは確かに証明する各個別インデックスについて。
効果的に公理化された理論では、各証明を順次検証することができる。理論が本当に無矛盾であれば、矛盾の証明は存在せず、これは前述の「矛盾探索」が決して停止しないという主張に対応する。理論において形式的に言えば、前者は次の命題で表現される。算術的矛盾の主張を否定する。同等の-命題すべての証明が不条理の証明ではないと述べることで、探索が決して停止しないことを形式化します。そして実際、証明可能性を正確に表すオメガ無矛盾理論では、不条理探索が停止して終わるという証明はなく（明示的な矛盾は導出できない）、また、ゲーデルが示したように、不条理探索が決して停止しないという証明もありません（無矛盾は導出できない）。言い換えると、不条理探索が決して停止しないという証明はなく（無矛盾は導出できない）、また、不条理探索が決して停止しないという証明もありません（無矛盾は拒否できない）。繰り返しますが、これら2つの選言のどちらも証明可能だが、それらの論理和は自明である証明可能。実際、もし一貫性がある場合、違反する。
の-証明の存在を表す命題論理的には肯定的な記述である。しかしながら、歴史的には、その否定は-命題は、建設的な文脈では、この否定記号の使用は誤解を招く用語となる可能性がある。
フリードマンは、もう一つ興味深い証明不可能な命題を確立した。それは、一貫性があり適切な理論は、その算術的選言性質を決して証明しない、というものである。
すでに最小限の論理はすべての非矛盾主張を論理的に証明しており、特にそしてまた定理これは、証明可能な二重否定排中項（または存在主張）として解釈できる。しかし、この選言の性質を考慮すると、単純な排中項はできない証明可能。したがって、ド・モルガンの法則の1つは、直観的に一般には成り立たない。
原則の内訳そして説明しました。最小数の原理これは帰納法の原理と同等の多くの命題のうちの1つにすぎません。以下の証明は、暗示するしたがって、この原則が一般的に有効でない理由しかし、すべての非自明な述語に対して二重否定最小数の存在を付与するスキーマは、は一般的に妥当である。ゲーデルの証明に照らして、これら３つの原理の破綻は、ハイティング算術が構成的論理の証明可能性の解釈と整合しているものとして理解できる。
原始再帰述語に対するマルコフの原理含意スキーマとして既に成立していない厳密に言えばより強い前述のとおり、対応する規則の形式では許容されるが、同様に、理論は前提原理の独立性を証明するものではない。否定述語の場合、すべての否定命題の規則の下で閉じられているが、つまり存在量化子を抜き出すことができる。存在命題を単なる選言に置き換えたバージョンについても同様である。
妥当な含意選言三段論法を用いれば、その逆の形でも成り立つことが証明できる。しかし、二重否定の転換は直観主義的に証明できない、つまり「「すべての数に対する普遍量化を伴う。これは、一貫性によって説明される興味深い内訳である。一部の人にとってチャーチの論文に関するセクションで述べたとおりです。
自然数の順序関係を利用すると、強い帰納法の原理は次のようになる。
集合論でおなじみのクラス表記では、算術式はは次のように表現されます。どこ任意の否定形の述語、すなわち帰納法の論理的等価物は
洞察は、サブクラス間で最小メンバーが存在しないことが証明できる性質は、空クラスであること、すなわち、メンバーが存在しない状態と同等である。対偶を取ると、任意の空でない部分クラスに対して、メンバーが存在することを一貫して排除することはできないという定理が得られる。メンバーが存在しないより小さい:
ペアノ算術では、二重否定の消去が常に有効であるため、これは最小数原理の一般的な定式化を証明する。古典的な解釈では、空でないことは、（証明可能な形で）何らかの最小要素が存在することと同値である。
二項関係「上記の形式で強い帰納スキーマを検証することは、常に非反射的でもある。または同等に
ある固定数に対して上記は、どのメンバーもの検証するつまり（そしてこの論理的推論では、二項関係の他の性質は一切使用されていません。）より一般的に言えば、は空集合ではなく、関連する（古典的な）最小数原理を使用して、否定形式の何らかの命題（例えば、) ならば、これを完全に構成的な証明に拡張することができる。これは含意が常に直観的に形式的に強いものと同等である。
しかし一般的に、構成的論理においては、最小数原理の弱化は解消されない。次の例がこれを示している。ある命題について（言う上記のように）述語を考慮する
これサブクラスに対応します自然数のクラスに属すると証明または仮定された任意の数は、またはつまり。 として提案またはこれは自明に真であり、したがってクラスは存在する。さらに、等価性の決定可能性と選言三段論法を用いることで、等価性が証明される。言い換えれば、クラスのメンバーは、. 基礎となる命題がが独立であれば、その述語も理論上は決定不能である。
クラスの中で最も小さいメンバーは何かと問うことができるそうかもしれない。そこに人が住んでいるので、このクラスの最小数の存在は否定できない。実際、結合が与えられた場合、は自明であり、最小数の存在の主張はそれ自体は除外中間文に翻訳されますこのような数値の値を知ることで、成り立つ。したがって、独立最小数原理のインスタンスまた、。
集合論の記法では、また、、一方その否定は以下と同等である。これは、捉えどころのない述語が捉えどころのない部分集合を定義できることを示している。同様に、構成的集合論においても、自然数のクラス上の標準順序は決定可能であるが、自然数は整列順序ではない。しかし、構成的に実現不可能な存在主張を含意しない強力な帰納原理も依然として利用可能である。
計算可能なコンテキストでは、述語に対して古典的には自明な無限選言
また、次のように書かれているは、決定問題の決定可能性の検証として解釈できます。クラス表記では、また、次のように書かれています。。
証明できない命題は証明しないしたがって、特に、古典理論の定理を否定するものではありません。しかし、述語も存在します。公理が一貫性がある。繰り返しになるが、このような否定は、特定の数値反例の存在と等価ではない。除外された中間実際、最小論理はすでにすべての命題に対して二重否定排中律を証明しており、したがってこれは、任意の述語に対して。
教会の規則は、チャーチのテーゼの原則採用される可能性がある、 その間それを拒否する：それは、先ほど述べたような否定を意味する。
上記の論理的意味で決定可能な述語はすべて、全計算可能関数によっても決定可能であるという形式の原理を考えてみましょう。これが排中律とどのように矛盾するかを見るには、計算可能決定不可能な述語を定義するだけで十分です。そのために、次のように記述します。KleeneのT述語から定義された述語の場合。インデックス計算可能な関数の総数を満たす。 その間原始的な再帰的な方法で実現できる述語でつまりクラス対角線上で停止する様子を記述する証拠を伴う部分計算可能関数インデックスは、計算可能列挙可能だが計算可能ではない。古典的な補集合定義済み計算可能列挙すらできない（停止問題を参照）。これは証明済みの決定不能問題である。違反例を示します。任意のインデックスについて同等の形式対応する関数が評価されるとき ()、評価履歴の考えられるすべての記述 () は、目の前の評価を記述していません。具体的には、関数に対してこれが決定不可能であることは、次のことの否定を確立します。。
形式的な教会の原則は、当然ながら再帰的学派と結びついている。マルコフの原理チャーチの原理は、その学派と、より広くは構成的数学によって一般的に採用されている。より弱い形式と同等後者は一般に単一の公理、すなわち任意の に対する二重否定除去として表現できる。ヘイティング算術と両方+決定可能な述語の前提の独立性を証明する、しかし、それらは一貫して一緒にはならない。。 また否定するLEJ Brouwerの直観主義学派は、Heytingの算術を、両方の原則を否定する一連の原理によって拡張している。同様に。
ある数に対してメタ理論では、研究対象理論における数字は次のように表される。。
直観主義算術では、選言の性質これは一般的に妥当である。そして、この定理が成り立つ算術の任意の拡張は、数値存在性も持つことが定理である。:
したがって、これらの性質はヘイティング算術においてメタ論理的に等価である。存在と選言の性質は、存在の主張をハロップの公式によって相対化しても実際には依然として成り立つ。つまり、証明可能な。
チャーチの弟子であるクリーネは、ヘイティング算術の重要な実現可能性モデルを導入した。一方、彼の弟子であるネルス・デイヴィッド・ネルソンは、（拡張として）) 全ての閉じた定理（つまり、すべての変数が束縛されている）が実現可能です。ハイティング算術における推論は実現可能性を保持します。さらに、すると、部分的な再帰関数が実現されます関数が評価されるたびにで終了する、 それからこれは任意の有限個の関数引数に拡張できます。また、古典的な定理の中には、証明可能だが、認識は必要だ。
実現可能性の型付きバージョンはゲオルク・クライゼルによって導入された。彼はそれを用いて、直観主義理論において古典的に妥当なマルコフの原理が独立していることを示した。
BHK解釈およびDialectica解釈も参照のこと。
有効トポスでは、帰納法が制限されたハイティング算術の有限公理化可能なサブシステムはすでにこれはカテゴリカルです。ここでのカテゴリカル性は、テネンバウムの定理を彷彿とさせます。このモデルは、しかしそうではないしたがって、この文脈においては完全性は成り立たない。
理論が無矛盾であれば、証明は不条理の証明にはならない。クルト・ゲーデルは否定変換を導入し、ハイティング算術が無矛盾であればペアノ算術も無矛盾であることを証明した。つまり、彼は無矛盾性の課題をのしかし、ゲーデルの不完全性定理、つまり特定の理論が自身の無矛盾性を証明できないという定理は、ハイティング算術自体にも当てはまる。
または、数値存在特性を持つその一貫した拡張自動的に-健全。[ 3 ]（逆に、この性質は健全性を要求する。したがって、たとえば、理論でさえ実際には、すでにそのペンダントは不健全であり、したがって）
古典的一次理論の標準モデルまた、その非標準モデルは、ヘイティング算術のモデルでもある。。
完全な構成的集合論モデルも存在するそしてその意図された意味論。比較的弱い集合論で十分である。それらは無限公理、述語分離の公理図式を採用して、算術式の帰納を証明する。また、再帰的定義のための有限領域上の関数空間の存在も必要となる。具体的には、これらの理論は、分離公理や集合帰納法の完全な公理（ましてや正則性の公理）も、一般的な関数空間（ましてや冪集合の完全な公理）も含まれていない。
さらに、弱い構成的集合論では順序数のクラスはそのため、フォン・ノイマン自然数の集合は、この理論において集合として存在しない。[ 4 ] [ 5 ]メタ理論的には、この理論の領域は、その順序数のクラスと同じ大きさであり、本質的にクラスを通して与えられる。自然なものと全単射なすべての集合のうち公理として、これはそして他の公理は集合代数と順序に関連するもので、和集合と二項交差（述語的分離スキーマ、外延性、ペアリング、集合帰納スキーマと密接に関連している）である。この理論は、すでに以下の理論と同一である。強い無限性はなく、有限性の公理が追加されている。この集合論はモデル理論と同様である。そして反対に、集合論の公理は原始再帰関係に関して証明される。
その小さな集合の世界は、それらの相互メンバーシップを符号化する有限バイナリシーケンスの順序付きコレクションとして理解できます。たとえば、'番目のセットには、もう1つのセットと'th セットには他の 4 つのセットが含まれています。BIT述語を参照してください。
推論規則に基づく論理形式化を反映した型理論的な実現が、さまざまな言語で実装されている。
ハイティング算術について、原始再帰関数に潜在的な関数記号を追加して議論した。この理論はアッカーマン関数の総和を証明する。
さらに、公理と形式主義の選択は、構成主義者の間でも常に議論の的となってきた。証明論では、例えば数間の関数型やそれらの間の関数型などについて、広く研究されてきた。形式は当然より複雑になり、関数の適用を規定するさまざまな公理が可能になる。全関数のクラスはこのようにして豊かにすることができる。有限型を用いた理論さらに関数拡張性と選択公理を組み合わせるとそれでも同じ算術式を証明するそして、型理論的な解釈がある。しかし、その理論は、チャーチのテーゼを否定する。また、すべての機能において連続的になるだろう。しかし、例えば、異なる外延性規則、選択公理、マルコフ原理と独立性原理、さらにはケーニッヒの補題を、それぞれ特定の強度またはレベルで全てまとめて採用すると、排中律を証明できないかもしれないかなり「詰め込まれた」算術を定義することができる。-式。初期の段階では、内包的等価性やブロウワーの選択シーケンスを持つ変種も研究された。
構成的2階算術の逆算術研究が行われた。 [ 6 ]
この理論の形式的な公理化は、 Heyting (1930)、Herbrand、Kleeneに遡る。Gödel は、以下の無矛盾性結果を証明した。1933年に。
ハイティング算術は、ブール代数の直観主義的類似物であるハイティング代数と混同してはならない。
