ロビンソン算術

数学において、ロビンソン算術は、 1950年にラファエル・M・ロビンソンによって初めて提唱された一階ペアノ算術(PA)の有限公理化された部分である。 [ 1 ]通常、 Qと表記される。

Qは数学的帰納法公理スキームを持たないPAである。QはPAよりも弱いが、同じ言語を持ち、どちらの理論も不完全である。QはPAの有限公理化された断片であり、再帰的に不完全かつ本質的に決定不可能であるため、重要かつ興味深い。

公理

Qの背景論理は、中置「=」で表される恒等式 を持つ一階述語論理である。自然数と呼ばれる個体は、ゼロと呼ばれる特別な元0を含むNと呼ばれる集合の元である。Nに対しては3つの演算が存在する。

Qに関する以下の公理は、 Burgess (2005 , p. 42)の Q1–Q7 である(一階算術の公理も参照)。存在量指定子によって束縛されない変数は、暗黙の全称量指定子によって束縛される。

  1. Sx0
    • 0はどの数字の後続数字でもありません。
  2. ( Sx = Sy ) → x = y
    • xの後続集合がyの後続集合と同一である場合、xyは同一である。(1)と(2)は、N0を境界とする無限集合)とSNを定義とする単射関数)に関する、非自明性に必要な事実の最小値を与える。 (2)の逆は、恒等関数の性質から導かれる。
  3. y = 0 ∨ ∃ x ( Sx = y )
  4. x + 0 = x
  5. x + Sy = S ( x + y )
  6. x · 0 = 0
  7. x·Sy = ( x·y ) + x

異形公理化

Robinson (1950)の公理は、 Mendelson (2015 、pp. 202–203)の(1)~(13)である。Robinsonの13個の公理のうち最初の6個は、本稿とは異なり、背景論理に恒等性が含まれない場合にのみ必要となる。

N上の通常の厳密な全順序である「より小さい」(「<」で示される)は、x < y ↔ ∃ z ( Sz + x = y )という規則によって加算によって定義できます。同様に、「<」を原始的なものとしてこの規則を8番目の公理として追加することで、 Qの定義的保存的拡張が得られます。このシステムは、Boolos、Burgess、Jeffrey (2002 、Sec 16.4)で「ロビンソン算術R 」と呼ばれています。

Qの別の拡張(ここでは仮にQ+と呼ぶ)は、「<」を原始的なものとして、(最後の定義公理の代わりに)次の3つの公理をQの公理(1)~(7)に追加することで得られる。

  • ¬( x < 0 )
  • x < Sy ↔ ( x < yx = y )
  • x < yx = yy < x

Q+ は依然としてQの保守的な拡張であり、これはQ+で証明可能な任意の式で記号 "<" を含まないものはQで既に証明可能であるという意味です。(上記の 3 つの公理のうち最初の 2 つだけをQに追加すると、 Burgess (2005、p. 56) がQ*と呼ぶものと同等のQの保守的な拡張が得られます。Burgess (2005 、p. 230、fn. 24 も参照)。ただし、上記の 3 つの公理の 2 番目は、公理x < y ↔ ∃ z ( Sz + x = y )だけを追加して得られるQの「純粋な定義拡張」からは演繹できないことに注意してください。)

Qの公理 (1)–(7) のうち、公理 (3) には内部存在量指定子が必要である。Shoenfield (1967 、p. 22) は、 Qの公理 (3) を使わずに、上記 3 つの公理に < を基本公理として加えることで、(暗黙の)外部全称量指定子のみを持つ公理化を与えている。つまり、Shoenfield の体系はQ+から公理 (3) を引いたものであり、 Q+よりも厳密に弱い。なぜなら、公理 (3) は他の公理から独立しているからである(例えば、Sv がv + 1と解釈される場合、より小さい順序数は (3) を除くすべての公理のモデルとなる)。Shoenfield の体系はBoolos、Burgess、Jeffrey (2002 、Sec 16.2)にも登場し、そこでは「最小算術」( Qとも表記)と呼ばれている。 「<」の代わりに「≤」を使用する、密接に関連した公理化は、Machover(1996、pp. 256-257)に記載されています。 ωω{\displaystyle \omega ^{\omega }}

メタ数学

Qのメタ数学については、Boolos , Burgess & Jeffrey (2002 , chpt. 16)、Tarski, Mostowski & Robinson (1953)Smullyan (1991)Mendelson (2015 , pp. 202–203)、Burgess (2005 , §§1.5a, 2.2) を参照のこと。Qの意図する解釈は自然数とその通常の算術であり、加算乗算は通常の意味を持ち、恒等式は等式Sx = x + 1、0自然数である。

Qの公理をすべて満たすモデル(構造)は、公理(3)を除いて、標準自然数N、+、·、S、0)と同型の一意のサブモデル(「標準部分」)を持ちます。(公理(3)は必ずしも満たされる必要はありません。例えば、非負整数係数を持つ 多項式は、(3)を除くすべての公理を満たすモデルを形成します。)

Q はペアノ算術と同様に、あらゆる無限基数に対する非標準モデルを持つ。しかし、ペアノ算術とは異なり、テネンバウムの定理はQには適用されず、計算可能な非標準モデルを持つ。例えば、正の先頭係数を持つ整数係数多項式と零多項式を通常の算術で組み合わせたQの計算可能モデルが存在する。

Qの注目すべき特徴は、帰納法の公理体系が存在しないことである。そのため、 Qでは自然数に関する事実のあらゆる具体的な事例を証明できることが多いが、それに関連する一般定理は証明できない。例えば、5 + 7 = 7 + 5 はQで証明できるが、一般命題x + y = y + xは証明できない。同様に、一般命題Sxxは証明できない。[ 2 ]標準的な事実の多くを満たさないQのモデルは、自然数の標準モデルに2 つの異なる新しい要素abを追加し、すべてのxについてSa = aSb = bx + a = b 、 x + b = aと定義することで得られます。また、nが標準の自然数である場合は、すべての x についてa + n = aおよびb + n = b 、すべてのxについてx · 0 = 0 、n0 以外の標準自然数である場合はa · n = bおよびb · n = a 、 x = aを除くすべてのxについてx · a = ax = b を除くすべてのxについてx · b = ba · a = b、およびb · b = aと定義します。[ 3 ]

Q は、外延性空集合の存在、および随伴公理からなるツェルメロの公理的集合論の断片で解釈可能である。この理論は、 Tarski, Mostowski & Robinson (1953 , p. 34)では S'、Burgess (2005 , pp. 90–91, 223)では ST である。詳細は 一般集合論を参照のこと。

Qは有限に公理化された一階理論であるが、これはペアノ​​算術(PA) よりもかなり弱く、その公理には存在量化子が1 つしか含まれない。しかし、PA と同様に、ゲーデルの不完全性定理の意味で不完全かつ不完全であり、本質的に決定不能である。Robinson (1950)は、すべての計算可能関数が PA で表現可能であることを証明するためにどの PA 公理が必要であるかに注目して、上記のQ公理 (1) - (7)を導出した[ 4 ][ 5 ]この証明が PA 公理帰納法のスキームを使用する唯一の目的は、上記の公理 (3) であるステートメントを証明することであり、したがって、すべての計算可能関数はQで表現可能である。[ 6 ] [ 7 ] [ 8 ]ゲーデルの第二不完全性定理の結論はQにも当てはまる。Qの一貫した再帰的に公理化された拡張はたとえゲーデル数の証明を定義可能なカットに制限したとしても、それ自身の一貫性を証明することはできない。[ 9 ] [ 10 ] [ 11 ]

第一不完全性定理は、必要な符号化構成(ゲーデル数を含む)を実行するのに十分な算術を定義する公理系にのみ適用される。Q の公理は、この目的に十分強力であることを保証するように特別に選択された。したがって、第一不完全性定理の通常の証明を用いて、Q が不完全かつ決定不能であることを示すことができる。これは、PA の不完全性と決定不能性が、PA とQを区別する唯一の側面、すなわち帰納法公理スキームのせいではないことを示している。

ゲーデルの定理は、上記の7つの公理のいずれか1つでも欠けると成立しなくなります。Qのこれらの断片は決定不可能なままですが、本質的に決定不可能ではなくなりました。つまり、それらは矛盾なく決定可能な拡大と、興味深くないモデル(つまり、標準的な自然数の端拡大ではないモデル)を持ちます。

参照

参考文献

  1. ^ロビンソン 1950 .
  2. ^バージェス 2005、56ページ。
  3. ^ Boolos、Burgess、Jeffrey 2002、第16.4節。
  4. ^メンデルソン 2015、p. 188、命題3.24。
  5. ^関数がで表現可能であるとは、すべてのf{\displaystyle f}PA{\displaystyle \operatorname {PA} }ϕ{\displaystyle \phi }×1×y{\displaystyle x_{1},\cdots,x_{k},y}
    f×yPAϕ×y{\displaystyle f({\vec {x}})=y\Longleftrightarrow \operatorname {PA} \vdash \phi ({\vec {x}},y),}
    f×yPA¬ϕ×y{\displaystyle f({\vec {x}})\neq y\Longleftrightarrow \operatorname {PA} \vdash \lnot \phi ({\vec {x}},y)。}
  6. ^オディフレディ 1989 .
  7. ^メンデルソン 2015、p. 203、命題3.33。
  8. ^ラウテンバーグ 2010、246ページ。
  9. ^ベズボルア&シェパードソン 1976 .
  10. ^パドラック 1985 .
  11. ^ハジェク & プドラーク 1993、p. 387.

参考文献