1 歴史
ペアノ算術（Peano arithmetic, PA）は、自然数の性質を公理として定式化する試みの到達点の一つとして位置づけられる。19世紀末から20世紀初頭にかけて、数学を論理的な根拠の上に組み立て直そうとする基礎論の運動が進み、数の扱いを厳密な形式体系へ落とし込むことが重要課題となった。そうした潮流の中で、後者（successor）操作や零元、帰納原理といった要素を最小限の公理で束ね、加法・乗法をそこから構成する枠組みが形成された。
1.1 数学基礎論における位置づけ
ペアノ算術は、数学基礎論において「自然数論の標準的な形式化」の代表例とみなされる。なぜなら、対象は比較的素朴である一方、形式体系としては十分に強く、演算や証明の操作を内部で扱えるためである。特に、形式的に書き下された証明がどの程度まで自然数の性質を捕捉できるか、また自己言及的な構造がどのように現れるかを検討する土台として、論理学の中核的な議論に結びつく。
1.2 ペアノの公理化の成立
ペアノは自然数の性質を公理で記述する方針を体系化し、後者関数と零元を核に据えた。ここで重要なのは、自然数の数体系を「既存の算術に依存して」構築するのではなく、後者と帰納の原理に基づいて段階的に規則を与える点である。これにより、加法や乗法のような演算は、後から定義されてもなお体系全体の一貫性が保たれるよう設計される。
1.3 形式化の発展
その後、論理学の形式体系が洗練されるにつれ、ペアノのアイデアは精密な論理記号を用いる形へと再構成されていった。とりわけ、形式言語・推論規則・公理体系という枠組みが確立されると、ペアノ算術は単なる公理列ではなく、モデルや証明可能性といった概念と結びついた対象として研究されるようになった。結果として、モデル理論や証明論の成果がこの体系に直接適用される道が開けた。
2 公理体系
ペアノ算術は、自然数を表す定数記号・関数記号・関係記号を備えた一階述語論理に基づく体系として与えられる。典型的には、零元を表す定数、後者を表す単項関数、等号、および加法・乗法を表す関数記号（あるいはそれらを定義により導入する）が用いられる。
2.1 零元と後者関数
零元は自然数の基底点を示し、後者関数は各自然数に次の自然数を対応させる操作として導入される。公理化の核には、「後者が自然数を生成する」という直観があり、帰納法によって後者の反復が自然数列の全体を覆うことが保証される。これにより、数の直列性が形式的に扱えるようになる。
2.2 等号に関する公理
等号は、代入により意味が変わらないことを反映するため、同一性に関する通常の公理群で規定される。具体的には、反射的な性質、対称性、推移性が体系に組み込まれ、さらに基本的な一致の概念に従って、関数や関係の引数の置換が妥当になるように扱われる。これにより、形式証明の段階で等式の変形が安全に行える。
2.3 帰納法の公理
帰納法はペアノ算術を特徴づける中心的要素である。任意の性質について、その性質が零元に当てはまり、かつ後者に継承されるなら、すべての自然数に対して成り立つ、という形式化が与えられる。
2.3.1 帰納法の役割
帰納原理が担うのは、有限段数の検討にとどまらず、無限に見える全自然数への拡張を可能にする点である。後者操作から数列が生成される以上、性質の伝播を論理的に一括して保証する仕組みが必要になる。帰納法はそのための橋渡しとして働き、体系の強度の源泉でもある。
2.3.2 スキーマとしての表現
一階述語言語では、帰納法を「特定の性質に対して」与えると汎用性が失われる。そのため、帰納法は述語（性質）を変数として含む形で無数の公理を生成するスキーマとして表現される。具体的には、自由変数を持つ任意の述語に対して同型の枠組みが適用され、これにより体系は帰納の汎用性を保持したまま形式的な公理集合として成立する。
2.4 加法と乗法の定義
加法と乗法は、後者関数と帰納法から再帰的に定義されるのが典型的である。定義を与えることで演算記号が体系の中で意味を持ち、以後の議論では定義から導かれる性質が形式的に利用される。
2.4.1 再帰的定義
加法は、右引数に関する後者の反復を通じて構成されるのが一般的である。同様に乗法も、乗算を加法の反復として見る再帰構造を利用して定義できる。これにより、演算は単なる外部の直観ではなく、後者と帰納の規則だけで確定する。
2.4.2 基本性質の導出
再帰的定義と帰納法を併用すれば、基本的な性質、例えば零元との整合性や、後者に関する遷移則といった恒等式が体系内で証明される。さらに、計算規則の組合せによって、加法・乗法の形式的な振る舞いが安定に確保される。こうしてペアノ算術は「演算を持つ形式体系」へと具体化される。
3 数理論理学上の性質
ペアノ算術は、論理学的性質を解析する格好の対象となっている。ここでは無矛盾性、完全性・不完全性、決定不能性、さらにモデルの多様性という観点から整理する。
3.1 無矛盾性
無矛盾性とは、体系が矛盾した命題とその否定を同時に証明できないことを指す。ペアノ算術は非常に自然な形式化であるため、実際には矛盾を含まないと考えられているが、「体系自身がその無矛盾性を証明できるか」は別問題となる。通常、強度の面から、体系の内部で完全な自己保証を与えることは制限されると理解される。
3.2 完全性と不完全性
完全性は、ある形式体系について、任意の文が証明可能または反証可能のどちらかに振り分けられるという性質を意味する。ゲーデルの枠組みによって、ペアノ算術は少なくとも一定の意味で不完全であることが示される。
3.2.1 ゲーデルの不完全性定理との関係
ゲーデルの不完全性定理は、十分に強い整合的（無矛盾的と見なされる）形式体系が、自身の無矛盾性のような内在的性質を含めて完全になり得ないことを述べる。ペアノ算術はその条件を満たす代表例であり、その結果、体系の言語において真であるが証明できない文が存在することが導かれる。この現象は単に技術的な巧妙さにとどまらず、形式化の限界を示す指標として扱われる。
3.2.2 証明可能性の限界
証明可能性の限界とは、体系がどれほど精密に公理を与えても、自然数に関するすべての真理を網羅できないという状況を指す。具体的には、特定の算術文について、体系内で証明も反証もできない立場が生じうる。これにより、形式体系の到達点と、それを超える追加原理の必要性が浮かび上がる。
3.3 決定不能性
決定不能性は、ある問題について機械的な手続きが「いつでも」正しい答えを出せないことを意味する。ペアノ算術では、成り立つ算術文の集合が計算可能な仕方で一様に決定されるわけではないことが示され、したがって一般的な意味での可否判定は不可能となる。これは、体系の表現力が高いことの帰結として現れる。
3.4 可算モデルと非標準モデル
モデル理論の観点では、ペアノ算術の公理を満たす「解釈の仕方」を考えることができる。その際、自然数として解釈される対象が実際の自然数と一致するとは限らない。特に、無限の対象を持つモデルが存在し、その中には通常の自然数とは一致しないものも現れる。
3.4.1 非標準自然数の存在
非標準モデルでは、後者の反復構造が通常の自然数と同型にはならない形で成り立つ。結果として、通常の自然数に対応しない元が「自然数のように」振る舞う。帰納法の公理が与える制約は強いが、それでもモデルの外部視点では、帰納法が適用されない形の非標準要素を潜在的に許す場合がある。
3.4.2 モデルの構造的特徴
非標準モデルは、加法や乗法の解釈、後者操作の閉包性、そして量化の振る舞いによって特徴づけられる。特に、同じ公理集合でも、どの文が真として評価されるかがモデルごとに変化しうるため、体系の表現力が「モデル差」を生むことになる。この差異は、標準モデルが持つ性質を論理的にどこまで固定できるかという観点で分析される。
4 応用と関連分野
ペアノ算術は単独で完結する理論ではなく、証明論・計算理論・数学基礎論といった周辺領域へ橋を提供する。以下では、それぞれの分野での利用のされ方を整理する。
4.1 証明論
証明論では、証明や反証を形式的対象として扱い、体系の強度や構造を調べる。ペアノ算術は、計算可能な推論の枠において算術的文がどの程度まで導出できるかを評価するための基本的舞台になる。
4.1.1 形式証明の記述
形式証明とは、記号列の規則に従って推論が積み上げられる過程を、メタレベルではなく体系の側で記述できる形にすることを指す。ペアノ算術は、証明の符号化を通じて「証明そのもの」を算術的に語るための言語と推論基盤を提供し得る。これにより、証明論的分析が算術文の枠組みに接続される。
4.1.2 帰納的証明技法
帰納に基づく証明技法は、ペアノ算術の構造と整合的である。たとえば、ある性質が数の段階に応じて成り立つことを示し、後者継承により全体へ広げる手順が体系内部で自然に実装される。証明の設計が再帰や帰納の枠組みによって行われるため、推論の体系性が保たれる。
4.2 計算理論
計算理論との関係は、ペアノ算術が「計算を表す」言語として働く点にある。計算可能関数やアルゴリズムの記述を算術文の形に翻訳できるため、計算可能性と論理的性質の接点が生まれる。
4.2.1 再帰関数との関係
再帰関数は、基本的な演算と合成、再帰を用いて計算可能な関数を特徴づける枠組みである。ペアノ算術では、再帰的構成で得られる関数の挙動を定義し、性質を証明することが可能になる。そのため、再帰関数の性質が論理文として扱われ、体系の強さを測る指標になり得る。
4.2.2 アルゴリズムの形式化
アルゴリズムの形式化とは、計算手順を論理的に記述し、計算の成否や出力の存在を文として表すことを指す。ペアノ算術は、そのための符号化の土台を与え、計算過程に関する一般的主張を一階述語論理の中で表現できる。この連結によって、決定不能性や計算量に関する論点が論理側へと移植される。
4.3 数学基礎論
数学基礎論では、ペアノ算術がどこまで自然数論を固められるか、また他の強度を持つ体系との関係が問題になる。
4.3.1 より強い体系との比較
より強い体系は、追加の公理やより強い帰納原理を導入することで、ペアノ算術では証明できない文まで到達しうる。比較の観点では、どの種類の命題クラスが追加されるのか、無矛盾性の扱いがどのように変わるのかが重要となる。ペアノ算術は、その比較の基準点として機能し、強度のグラデーションを測る基盤になる。
4.3.2 公理の拡張と制限
公理の拡張とは、例えば帰納原理の範囲を広げる、あるいは新しい関数や関係記号を導入して表現力を増すなどの操作である。一方、制限は帰納法の範囲や利用可能な量化の形を狭めることで、体系を弱める方向を指す。拡張と制限のいずれも、証明可能性・モデル理論的性質・計算的特徴の変化として現れ、ペアノ算術を軸にした体系研究を体系化する。