プレスバーガー算術

プレスバーガー算術()とは加法を含む自然数に関する一階述語論理体系である。モイジェシュ・プレスバーガーにより1929年に導入された。プレスバーガー算術のシグネチャには加法と等号のみが含まれ乗法は省かれる。公理には数学的帰納法の公理図式を含む。

プレスバーガー算術は加法と乗法両方含むペアノ算術より弱い体系である。ペアノ算術とは異なりプレスバーガー算術は決定可能である。これはプレスバーガー算術の言語で書かれた任意の閉論理式がプレスバーガー算術の公理で証明可能かどうかを判定するアルゴリズムが存在することを意味する。この決定問題の計算複雑性は漸近的に二重指数関数であることがで示されている。

概説プレスバーガー算術の言語は0と1、加法と解釈される二項関数+からなる。公理は以下の論理式を全称閉包したものである。 ¬(0 = x + 1) x + 1 = y + 1 → x = y x + 0 = x x + (y + 1) = (x + y) + 1 P(x)をプレスバーガー算術の言語による自由変数xを含む一階述語論理式とする。このとき次の論理式は公理である。 (P(0) ∧ ∀x(P(x) → P(x + 1))) → ∀y P(y).

(5) は数学的帰納法の公理図式であり、無限個の公理を表している。 (5) は有限の公理で置き換えることができないためプレスバーガー算術は有限公理化不可能である。

プレスバーガー算術は因数分解に関する規則や素数のような概念を形式化できない。一般的に乗法に関する自然数の概念は不完全性と決定不可能性につながることからプレスバーガー算術では定義することはできない。しかし、個々の論理式としては形式化可能である。例えば次は証明可能である。"任意のxに対して、あるyが存在し : (y + y = x) ∨ (y + y + 1 = x)" これは、すべての自然数は偶数もしくは奇数のどちらかであることを意味する。

性質

モイジェシュ・プレスバーガーはプレスバーガー算術に関して以下を証明した。無矛盾: 任意の文とその否定が共に演繹可能であることはない。完全: 任意の文が演繹可能であるか、もしくはその否定が演繹可能である。決定可能: 任意に与えられた文が定理であるか定理ではないかを判定するアルゴリズムが存在する。

応用

プレスバーガー算術

Źródło i licencja