FANDOM


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

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

概要

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

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

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

英語は形容詞

例えば・・・

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


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

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

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

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

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

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

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

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

統語論的な証明

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

言語と論理式

言語 

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

変数記号

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

論理記号

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

論理的な公理

a=a のように、無条件で明らかに成り立てばよい。

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

その他もろもろ

リンク

命題論理

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


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

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