ロッサーのトリック

数理論理学において、ロッサーのトリックは、検討中の理論がω-無矛盾であるという仮定に頼らずにゲーデルの不完全性定理の変形を証明する方法である（スモリンスキー 1977、p. 840; メンデルソン 1977、p. 160）。この方法は、1931年に発表されたゲーデルの不完全性定理の元の証明を改良したものとして、1936年に J.バークレー・ロッサーによって導入された 。

ゲーデルのオリジナルの証明では（非公式に）「この文は証明できない」という文が使われていますが、ロッサーのトリックでは「この文が証明可能であれば、その否定のより短い証明がある」という式が使われています。

ロッサーのトリックは、ゲーデルの不完全性定理の仮定から始まります。効果的で一貫性があり、十分な初等算術の断片を含む理論が選択されます。 ${\displaystyle T}$

ゲーデルの証明は、そのような理論に対して、 が式の自然数コード（ゲーデル数）であり、 がによってエンコードされた式の証明に対するゲーデル数であるという意図された意味を持つ式が存在することを示しています。 （この記事の残りの部分では、数と によってエンコードされた式を区別せず、式をエンコードする数はと表記します。）さらに、式はとして定義されます。これは、 から証明可能な式の集合を定義することを目的としています。 ${\displaystyle \operatorname {証明} _{T}(x,y)}$${\displaystyle y}$${\displaystyle x}$${\displaystyle T}$${\displaystyle y}$${\displaystyle y}$${\displaystyle y}$${\displaystyle \phi}$${\displaystyle \#\phi}$${\displaystyle \operatorname {Pvbl} _{T}(y)}$${\displaystyle \exists x\operatorname {証明} _{T}(x,y)}$${\displaystyle T}$

に関する仮定は、否定関数 を定義できることも示しています。この関数は、 が式のコードである場合、 は式 のコードであるという性質を持ちます。否定関数は、式のコードではない入力に対しては、どのような値でも取ることができます。 ${\displaystyle T}$${\displaystyle {\text{neg}}(y)}$${\displaystyle y}$${\displaystyle \phi}$${\displaystyle {\text{neg}}(y)}$${\displaystyle \neg \phi}$

理論のゲーデル文は、  ↔ を証明する式（ と表記されることもある）である。ゲーデルの証明は、が無矛盾である場合、ゲーデル文を証明できないことを示している。しかし、ゲーデル文の否定も証明できないことを示すためには、理論が単に無矛盾であるだけでなく、ω無矛盾であるというより強い仮定を加える必要がある。たとえば、 PA がペアノ公理である理論 は、 を証明している。ロッサー（1936）は、ゲーデルの証明のゲーデル文を置き換えるために使用できる別の自己参照文を構築し、ω 無矛盾性を仮定する必要をなくした。 ${\displaystyle T}$${\displaystyle \phi}$${\displaystyle G_{T}}$${\displaystyle T}$${\displaystyle \phi}$${\displaystyle \neg \operatorname {Pvbl} _{T}(\#\phi )}$${\displaystyle T}$${\displaystyle T={\text{PA}}+\neg {\text{G}}_{PA}}$${\displaystyle \neg G_{T}}$

固定された算術理論に対して、およびを関連する証明述語と否定関数とします。 ${\displaystyle T}$${\displaystyle \operatorname {証明} _{T}(x,y)}$${\displaystyle {\text{neg}}(x)}$

修正された証明述語は次のように定義されます。 ${\displaystyle \operatorname {証明} _{T}^{R}(x,y)}$

$${\displaystyle \operatorname {証明} _{T}^{R}(x,y)\equiv \operatorname {証明} _{T}(x,y)\land \lnot \exists z\leq x[\operatorname {証明} _{T}(z,\operatorname {neg} (y))],}$$

つまり

$${\displaystyle \lnot \operatorname {証明} _{T}^{R}(x,y)\equiv \operatorname {証明} _{T}(x,y)\to \exists z\leq x[\operatorname {証明} _{T}(z,\operatorname {neg} (y))].}$$

この修正された証明述語は、修正された証明可能性述語を定義するために使用されます。 ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$

$${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)\equiv \exists x\operatorname {証明} _{T}^{R}(x,y).}$$

非公式には、は何らかのコード化された証明によって証明可能な主張であり、 の否定を示すより小さいコード化された証明は存在しない。 が矛盾しないという仮定の下では、各式に対して が成り立つ場合のみ、かつ が成り立つ場合に限り、式は成り立つ。なぜなら、 の証明のコードが存在する場合、( の矛盾しない事実に従って) の証明のコードは存在しないからである。しかし、における証明可能性の観点からは、と は異なる特性を持つ。 ${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$${\displaystyle y}$${\displaystyle x}$${\displaystyle y}$${\displaystyle T}$${\displaystyle \phi}$${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$${\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}$${\displaystyle \phi}$${\displaystyle T}$${\displaystyle \neg \phi}$${\displaystyle \operatorname {Pvbl} _{T}(\#\phi )}$${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$${\displaystyle T}$

定義から直接得られる結果は、に十分な算術が含まれている場合、すべての式 に対して が成り立つことを証明できるということです。これは、そうでない場合、との両方を満たす との証明をそれぞれコード化する2 つの数 が存在するためです。(実際、 は、このような状況がどの 2 つの数にも当てはまらないことを証明し、一階述語論理を含めるだけで済みます) ${\displaystyle T}$${\displaystyle \phi}$${\displaystyle \operatorname {Pvbl} _{T}^{R}(\phi )}$${\displaystyle \neg \operatorname {Pvbl} _{T}^{R}({\text{neg}}(\phi ))}$${\displaystyle n,m}$${\displaystyle \phi}$${\displaystyle \neg \phi}$${\displaystyle n<m}$${\displaystyle m<n}$${\displaystyle T}$

対角補題を用いて、が を証明する式であるとします。この式は理論のRosser 文です。${\displaystyle \rho}$${\displaystyle T}$${\displaystyle \rho \iff \neg \operatorname {Pvbl} _{T}^{R}(\#\rho )}$${\displaystyle \rho}$${\displaystyle T}$

が、ロッサー文 を満たす、十分な量の算術を含む、有効で一貫した理論であるとします。このとき、次が成り立ちます (Mendelson 1977、p. 160)。 ${\displaystyle T}$${\displaystyle \rho}$

1. ${\displaystyle T}$証明しない${\displaystyle \rho}$
2. ${\displaystyle T}$証明しない${\displaystyle \neg \rho}$

これを証明するには、まず、式と数に対して、 が成り立つ場合、が証明されることを示します。これは、ゲーデルの第 1 不完全性定理の証明で行われたことと同様の方法で示されます。つまり、 は、2 つの具体的な自然数の間の関係である を証明します。次に、より小さい自然数すべてを1 つずつ調べ、各 に対して、再び、2 つの具体的な数の間の関係である を 証明します。${\displaystyle y}$${\displaystyle e}$${\displaystyle \operatorname {証明} _{T}^{R}(e,y)}$${\displaystyle T}$${\displaystyle \operatorname {証明} _{T}^{R}(e,y)}$${\displaystyle T}$${\displaystyle \operatorname {証明} _{T}(e,y)}$${\displaystyle z}$${\displaystyle e}$${\displaystyle z}$${\displaystyle T}$${\displaystyle \neg \operatorname {証明} _{T}(z,{\text{(neg}}(y))}$

十分な算術演算 (実際に必要なのは基本的な一階述語論理) が含まれているという仮定により、その場合でも が証明されることが保証されます。${\displaystyle T}$${\displaystyle T}$${\displaystyle \operatorname {Pvbl} _{T}^{R}(y)}$

さらに、が矛盾なく を証明する場合、におけるその証明の数コード化が存在し、におけるの否定の証明の数コード化は存在しません。したがって が成り立ち、 が証明されます。 ${\displaystyle T}$${\displaystyle \phi}$${\displaystyle e}$${\displaystyle T}$${\displaystyle \phi}$${\displaystyle T}$${\displaystyle \operatorname {証明} _{T}^{R}(e,y)}$${\displaystyle T}$${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\phi )}$

(1) の証明は、ゲーデルの第 1 不完全性定理の証明の証明と似ています。 が を証明すると仮定すると、前述の説明から、 が証明されます。したがって、 も証明されます。しかし、 が を証明すると仮定しましたが、が矛盾しない場合はこれは不可能です。 はを証明しないという結論に至らざるを得ません。 ${\displaystyle T}$${\displaystyle \rho}$${\displaystyle T}$${\displaystyle \operatorname {Pvbl} _{T}^{R}(\#\rho )}$${\displaystyle T}$${\displaystyle \neg \rho}$${\displaystyle T}$${\displaystyle \rho}$${\displaystyle T}$${\displaystyle T}$${\displaystyle \rho}$

(2) の証明でも、 の特別な形式が使われています。が を証明すると仮定すると、前述の説明から、 が を証明することがわかります。しかし、前のセクションで述べた Rosser の証明可能性述語の定義の直接的な帰結から、 が を証明することがわかります。したがって、も を証明することになります。しかし、 が を証明すると仮定しましたが、 が矛盾しない場合はこれは不可能です。 はを証明しないという結論に至らざるを得ません。 ${\displaystyle \operatorname {証明} _{T}^{R}}$${\displaystyle T}$${\displaystyle \neg \rho}$${\displaystyle T}$${\displaystyle \operatorname {Pvbl} _{T}^{R}({\text{neg}}\#(\rho ))}$${\displaystyle T}$${\displaystyle \neg \operatorname {Pvbl} _{T}^{R}(\#\rho )}$${\displaystyle T}$${\displaystyle \rho}$${\displaystyle T}$${\displaystyle \neg \rho}$${\displaystyle T}$${\displaystyle T}$${\displaystyle \neg \rho}$

• メンデルソン（1977）『数理論理学入門』
• スモリンスキー (1977)、「不完全性定理」、数学論理ハンドブック、ジョン・バーワイズ編、ノースホランド、1982年、ISBN  0-444-86388-5
• バークレー・ロッサー (1936年9 月) 。「ゲーデルとチャーチの定理の拡張」。Journal of Symbolic Logic。1 ( 3): 87–91。doi :10.2307/2269028。JSTOR 2269028。S2CID  36635388  。

• Avigad (2007)、「計算可能性と不完全性」、講義ノート。