現代数学の系譜11 ガロア理論を読む25 [無断転載禁止]©2ch.net

[過去ﾛｸﾞ] 現代数学の系譜11 ガロア理論を読む25 [無断転載禁止]©2ch.net (716ﾚｽ)
上下前次1-新
通常表示 512ﾊﾞｲﾄ分割ﾚｽ栞
抽出解除ﾚｽ栞

このｽﾚｯﾄﾞは過去ﾛｸﾞ倉庫に格納されています｡
次ｽﾚ検索歴削→次ｽﾚ栞削→次ｽﾚ過去ﾛｸﾞﾒﾆｭｰ

272: 現代数学の系譜11 ガロア理論を読む [sage] 2016/11/12(土) 08:06:34.09 ID:CRbt3jrT

>>268 補足
定理とその帰結
ゲーデルの完全性定理は、一階述語計算の演繹系が、全ての論理的に妥当な論理式の証明に追加の推論規則を必要としないという意味で「完全」であるとしている。完全性の逆は健全性であり、演繹系において論理的に妥当な論理式のみが証明可能だということを意味する。
これらから、論理式が論理的に妥当であることと、それが形式的演繹の帰結であることは同値である。

ゲーデルの完全性定理をより一般化した版もある。すなわち、任意の一階の理論 T とその理論での言語における任意の命題 S について、T における S の形式的演繹が存在することと、S が T のあらゆるモデルで成り立つことは同値である。
この一般化された定理は暗黙のうちに使われており、例えば、命題を群論の公理系で証明可能であることを示すとき、任意の群についてその命題が成り立つことを示すことで証明とする。

異なるモデルでも真となることを扱う数理論理学の一分野をモデル理論と呼ぶ。証明論という一分野では形式体系の証明そのものの構造を研究する。完全性定理は意味論と統語論の間を繋ぐことでこれら2つの分野の基本的な繋がりを確立している。
しかし、完全性定理はこれら2つの概念の差異をなくすものではない。実際、もう1つの成果であるゲーデルの不完全性定理によれば、数学における形式的証明で達成できることには本質的な限界がある。不完全性定理でいう「完全」は別の意味で使われている。
完全性定理は一階の理論の論理的帰結である論理式を扱い、不完全性定理は特定の理論の論理的帰結にはならない論理式を構築する。

完全性定理の重要な帰結の1つとして、一階の理論での論理的帰結の集合が帰納的可算集合であるという事実がある。論理的帰結の定義は特定の言語でのあらゆる構造上で全称化するもので、論理式が論理的に妥当かどうかをアルゴリズム的に検証する直接の手段とはならない。
さらに言えば、ゲーデルの不完全性定理の帰結により、論理的に妥当な論理式の集合は決定可能ではない。しかし完全性定理は、実効的な理論の帰結の集合が枚挙可能であることを示している。
そのアルゴリズムは、まずその理論から全ての形式的演繹を枚挙する方法を構成し、それを使って帰結の枚挙を生み出すことになる。
形式的演繹の有限かつ統語的性質により、それらを枚挙することが可能になっている。

http://rio2016.5ch.net/test/read.cgi/math/1477804000/272

273: 現代数学の系譜11 ガロア理論を読む [sage] 2016/11/12(土) 08:16:01.37 ID:CRbt3jrT

>>272
英語版 （日本語版だけではよくわからん）
https://en.wikipedia.org/wiki/G%C3%B6del%27s_completeness_theorem
(抜粋)
As a theorem of arithmetic

The Model Existence Theorem and its proof can be formalized in the framework of Peano arithmetic.
Precisely, we can systematically define a model of any consistent effective first-order theory T in Peano arithmetic by interpreting each symbol of T by an arithmetical formula whose free variables are the arguments of the symbol. However, the definition expressed by this formula is not recursive.

Consequences

An important consequence of the completeness theorem is that it is possible to recursively enumerate the semantic consequences of any effective first-order theory, by enumerating all the possible formal deductions from the axioms of the theory, and use this to produce an enumeration of their conclusions.

This comes in contrast with the direct meaning of the notion of semantic consequence, that quantifies over all structures in a particular language, which is clearly not a recursive definition.

Also, it makes the concept of "provability," and thus of "theorem," a clear concept that only depends on the chosen system of axioms of the theory, and not on the choice of a proof system.

つづく

http://rio2016.5ch.net/test/read.cgi/math/1477804000/273

上下前次1-新書関写板覧索設栞歴

ｽﾚ情報赤ﾚｽ抽出画像ﾚｽ抽出歴の未読ｽﾚ AAｻﾑﾈｲﾙ

ぬこの手ぬこTOP 2.076s*