Fandom

巨大数研究 Wiki

コメント0

完全性定理とコンパクト性定理

Wikipedia にでも書かれてある部分は Wikipedia にまかせます。|- は \longrightarrow で代用します。

具体的には言語、抽象的には論理の性質です。

概要

妥当 valid :前提条件から推論規則に則って結論が得られている。入力から構文規則に則った計算で出力が得られている。

健全 sound :妥当な推論がその意味世界に沿う解釈で証明となっている。妥当な出力の入力と構文規則が要求を満たしている。

完全 complete :その意味世界のトートロジーが証明できる。その理論で真となる式を計算で証明できる。

英語は形容詞

例えば・・・

ウィキアは前提=入力に則って妥当な推論=予めプログラミングされた計算(構文規則による変換)を行い検索結果を出力する。プログラムに誤りがあれば健全ではなく、入力された内容にふさわしくないページを出力することもある。完全であれば、すべてのふさわしいページを出力することができる。


すべての動物は飛ぶ、豚は動物である。よって豚は飛ぶ

これは妥当ではあるが、常識的に考えて健全ではない。

数学的に議論可能な対象そのものは記述可能であり、すべての数学的な論理式、およびその数学的な証明は記述することができる。記述可能とは有限の文字で表すことができることを意味する。記述不可能な論理式や証明の存在を数学的に証明することは可能である(表現する言語の抽象の度合いが問題でなく、まったく数学的に扱うことができない場合でもそうなのかは・・・今後の宿題。構成主義に反する?)。ある人が記述された文章を見て、それを論理式とみることができるのか、証明とみることができるのかは第一に形式言語の妥当性、つぎに解釈の健全性の問題となる。

証明には統語論上の形式的な証明と意味論上の理論的な証明がある。理論と論理はそれぞれ異なる概念を意味することに注意。

直観的に表現すると、論理は普遍的な推論方法、理論はそれぞれの分野に特有の常識。論理には普遍性が要求され、歴史的にも、とくに20世紀にはいって、命題論理くらいしかなかった状態から述語論理の開発などの抽象化が進み、さらに論理主義、形式主義、直観主義などさまざまな考え方の立場の違いが明確になっていった。理論は、古くから行われていた数学と専ら同じほうを向いており、虚数の存在を認めることが論理的な抽象化への一歩だとすれば、そこからガロア理論や群論、体論などへの発展が理論的な具体化となる。

証明とは一般的に、前提から目的とする命題を導き出すことを意味する。これを形式的に具体化すると、ある言語で記述される前提を構文規則にのっとって変換し、最終的に目的とする命題がその言語で出力されることになる――実際には記述できない場合も考えられる。

その前提だけからは証明できないとき、特定のモデルを選んで(しぼりこんで)証明することになる。(命題論理の公理より任意の矛盾した前提からは任意の命題が証明可能となる。また第一不完全性定理により、自然数論を含む十分強い無矛盾な前提は、その言語で表現可能な証明も反証もできない命題をもつ)。特定のモデルを選ぶということは、形式的な言語やモデルを充足するということであり、これは前提により強いモデルの前提を追加して強化すると捉えることもできる。論理的な推論規則、つまり言語の構文規則 syntax だけで証明可能であれば恒真命題 tautology であり、反証可能であれば恒偽命題であり、矛盾が導かれれば真でも偽でもモデルは存在しない。

完全性について書かれたテキストはよく見かけるけど健全性についてはなかなか見かけない気がする。完全性と違って直接言葉が使われる機会が少ないだけかもしれない。健全性を問わなければ、そして形式的、より穿った言い方をして、実在的存在を介してのみ公平な議論が成立するのであれば、数学的に完全に共有されるべきいかなる理論も、無矛盾だと主張したところでそれはある表現上だけの話であり、表現に制限を設けなければいくらでも矛盾の例をあげることができる。健全性を確かめるためには論理的帰結を知らなければならないが、それは厳密には主観的な事実でしかなく、健全性は絶対的な意味をもちえない? 完全なもろもろの共有が幻想というのは外界問題と絡めて大昔から分かりきった真理ではある。あるいは自分が「論理的帰結」の意味を捉え違えているだけかもしれない。

「前提」という言葉で統一したが、分野や文脈によっては体系、理論、環境などの言葉が使われることもある。

統語論的な証明

書かれた文章を機械的に処理して与えられる証明。推論ともいう。

言語と論理式

言語 

定数記号、関数記号、述語記号に分けることができる。

変数記号

定数記号やべつの変数を代入することができる。自由変数、束縛変数、媒介変数、など

論理記号

対象の意味に関係なく、形式的に普遍的なつながりをあらわす。

論理的な公理

ZFCなど理論的な公理とは違い形式的で、認識可能な意味が要求されない――(古典的な)数学で議論できなくともよい。

1 命題論理の公理

トートロジーの命題変数にそれぞれの論理式を代入して得られる。自由変数は全称量化する。(メモ ここではそれぞれの命題変数に真偽の真理値をどのように割り当てても真となる命題のことをトートロジーと呼んでいるが、矛盾した論理式を代入した場合を公理とはべつに考えることについては、議論と止揚の余地がありそう)

2 論理記号の公理

この記事では量化記号に関することだけ。この類でほかの公理が必要とされることがあるのかは知らない。

3 等号に関する公理


推論規則

命題論理と述語論理それぞれに推論規則があるが、ひとつづつ採用する。

命題論理から

モーダスポネンス Modus Ponens
\frac {\longrightarrow \phi,\longrightarrow \phi \to \psi}{\psi}(MP)

述語論理から

普遍汎化 Universal Generalization 一般化 Generalization GEN とも
\frac {\longrightarrow \phi}{\forall x \phi (x)}(GEN)
補足
自然な解釈では、恒に成り立つならすべてにおいて成り立つ、という意味。

意味論的な証明

形式的な構成を問わず、一般的な事実(とされているもの)から結論を導く。

モデル

3箱に2個づつみかんが入っています、みかんは全部で2*3=6(個)あります――と言ったときの箱とみかんにあたるもの。構造ということもある。同じ意味を有っていても異なる形をとることもある。領域 {Ω,Ω*2,Ω*3,...} で 1+1=2 の意味するものが Ω+Ω=Ω*2 となったり。

L=\{ c_i \}_{i<\alpha } \cup \{ F_i \} _{i<\beta } \cup \{ P_i  \} _{i<\gamma }

M=\{ |M|, \{ c_i^M \}_{i<\alpha },\{ F_i^{M_{m_i}}\} _{i<\beta },\{ P_i^{M_{n_i}} \} _{i<\gamma }\}

|M| は領域、c^M は定数記号、F_i^{M_{m_i}} はアリティ m_i の関数、P_i^{n_i} はアリティ n_i の述語記号。言語 L によって定義されるので L 構造と呼ぶ。

M(\lnot \phi ,t) \iff \lnot M(\phi ,t)

M(\phi \land \theta ,t) \iff M(\phi,t) \land M(\theta ,t)

M(\phi \lor \theta ,t) \iff M(\phi ,t) \lor M(\theta ,t)

M(\phi \to \theta ,t) \iff M(\phi ,t) \to M(\theta ,t)

一階論理の場合

\forall t M(\phi ,t) \iff \forall t(\phi ^M (t(x_1),t(x_2),...,t(x_n))

\exist t M(\phi ,t) \iff \exist t(\phi ^M (t(x_1),t(x_2),...,t(x_n))

二階論理では一階論理の述語や関数の割り当てまで考えなければなりません。

論理的帰結

\Gamma \models \phi は、Γ ならば当然 φ って感じ

様相的 modal な記述

Γ のすべての要素が真であるとき、φ が真であることは「必然 neccesarry」である。

あるいは、

Γ のすべての要素が真であるとき、φ が偽であることは「不可能 impossible」である。

様相論理学やら可能世界論やら

形式的な記述

\forall t [M(\Gamma ,t) \to M(\phi ,t)]

完全性定理

P \longrightarrow Q \iff P \models Q

右向きが健全性、左向きが完全性

準備

演繹定理

\Gamma \cup \{ \phi \} \longrightarrow \theta \iff \Gamma \longrightarrow \phi \to \theta

その他もろもろ

c が閉論理式の集合 Γ にあらわれないとき、

\Gamma \longrightarrow \phi (c) \iff \Gamma \longrightarrow \phi (x)

新しい定数記号を当てはめるには例化や代入規則しかないということ。この記事ではどれも採用してないが、公理で補完できているので一般性に欠くことはない。

命題論理の完全性

Γ から φ が証明されるならば、φ が恒真となるモデルは Γ を充足する――中には直観や自然言語に反するモデルもあるだろうが、とりあえず形式主義的には条件を満たせばよい。どのよううなモデルでも論理の公理と推論規則は(直観的に)適用される。よってΓのいかなる証明もそれぞれのΓを真とするモデルにおいて健全となる。

上の例に倣えば、すべての動物が飛ぶとかいうのは、一般的な解釈においては真ではないが、これらを(形式的に)真とするモデル、世界論でいうところの意味世界では豚が飛ぶことの証明も健全となる。妥当であれば証明となっているかが問題であって、一般論に沿うかどうか自体は問題ではない。

モダスポーネンスは恒真式から恒真式を推論する、より正確には前提をすべて真とする任意の設定から同じ設定で真となる論理式を導き出すため、命題論理は健全である。

トートロジーにそれぞれの言語の定数記号を代入したものは公理となる。Γ→φ は、条件より恒真である。よって演繹定理より、

\longrightarrow \Gamma \to \phi \Rightarrow \Gamma \longrightarrow \phi

一階述語論理の完全性

MP も GEN も恒真式から恒真式を導くため健全である。

完全でなければ証明できない恒真式 \phi が存在し \lnot \phi を加えた論証体系は無矛盾でもモデルをもたない。また、完全でない体系をいかに拡大しても完全にはならない。よって、任意の拡大の極大がモデルを持てばその論証体系はモデルを持つ。

無矛盾な閉論理式の集合 \Gamma を矛盾しないようにどこまでも拡大し極大 \Gamma ^* を得る。\Gamma に出てこない定数記号 c_0,c_1,c_2,... を言語 L に追加し L^* を得る。\Gamma^*L^* で構成される。

健全性より証明されれば恒真であり、反証されれば恒偽である。

言語 L^* の任意の論理式 \phi について \phi \in \Gamma^* あるいは \lnot \phi \in \Gamma^* が成り立つため、\Gamma^* は任意の(有限の長さの)論理式を証明もしくは反証可能であり、無矛盾であるためモデルを持ち完全である。

\Gamma^* のモデル M^* の、言語を L に制限した部分 M は、\Gamma のモデルとなっている。

完全性定理が成り立たない例

一階述語論理と同じ言語を使うが、量化子の使用に制限のある RCA_0 のモデルでは、すべての2変数アッカーマンの全域性が恒に成り立つが、証明することはできない。

コンパクト性定理

Γ は充足的である ⇔ Γ の各有限部分集合 Γ_0 は充足的である

コンパクト性定理が成り立たないとき、任意の有限部分集合に充足する設定があっても、それらは必ず充足できない Γ の論理式を、それぞれ無数にもつ。

コンパクト性定理が成り立つとき、Γ の各有限部分がモデルをもてば Γ 自身もモデルをもつ。たとえば、ラヨ関数が対角化する一階の集合論(一階の有限の集合論を極大化したもの)は、フォン・ノイマン宇宙をドメインとするモデルをもつ。

命題論理のコンパクト性

証明

⇒ は明らかなので、<= を示す。

一階述語論理のコンパクト性

WKL_0 のコンパクト性

RCA_0 にコンパクト性を追加すると WKL_0 になる。RCA_0 上ではそれぞれの x につき φ(x) を証明できても ∀xφ(x) を証明できないことがある。先ほどのすべての2変数アッカーマンの全域性とか。

応用

ラヨ命名する論理式 φ(x) は、一階述語論理の完全性より、x がある構成可能な集合であるときだけ成り立つことを一階述語論理で証明できる。

リンク

命題論理

広告ブロッカーが検出されました。


広告収入で運営されている無料サイトWikiaでは、このたび広告ブロッカーをご利用の方向けの変更が加わりました。

広告ブロッカーが改変されている場合、Wikiaにアクセスしていただくことができなくなっています。カスタム広告ブロッカーを解除してご利用ください。

Fandomでも見てみる

おまかせWikia