数理論理学 第2回

数理論理学 第10回
茨城大学工学部情報工学科
佐々木 稔
前回までのあらすじ
 述語論理
 関数
 定義域
 量記号
 配布資料は以下のURLからダウンロードできます
http://sas.cis.ibaraki.ac.jp/sasaki/Logic/
今週のお題
 述語論理の解釈
 述語論理式の形成規則
 述語論理式の解釈
 述語論理の恒真式
述語論理式の形成規則
項
 固体定数、固体変数
 t1, t2, ・・・, tn が項ならば、
n 引数の関数 f(t1, t2, ・・・, tn) も項
 基礎項
 項のなかで固体変数を含まないもの
 Alice, 父親(Bob) など
述語論理式の形成規則
 述語論理式の形成規則
 t1, t2, ・・・, tn が項ならば、基本論理式で
ある n 項述語 P(t1, t2, ・・・, tn) は論理式
 P, Q が論理式ならば、
 ~P, P⇒Q も論理式
 P∨Q、 P∧Q、 P⇔Q も論理式
 P が論理式、x が固体変数ならば、
 ∀xP、∃xP も論理式
形成規則を用いた例
 P(a)∧Q(a, b) は論理式かどうか
1. a, bは項であるから、P(a), Q(a, b) は論理式
2. P(a), Q(a, b) は論理式であるから、
P(a)∧Q(a, b) は論理式
 従って、P(a)∧Q(a, b) は論理式
閉論理式
 束縛変数と自由変数
 束縛変数: 量記号を伴った変数
 自由変数: 量記号を伴わない変数
 閉論理式
 自由変数を含まない論理式
 閉論理式でない論理式
 どんな固体定数を割り当ててもよい
 一般に論理式の真偽を決められない
閉論理式の真偽値
 固体変数、関数値の定義域を D
 真偽値の決め方
1. 各変数に定義域 D の要素を割り当て、
関数があればその値を求める
2. 基本論理式である述語の真偽値を決める
3. 真偽値の組合せから論理演算を行う
4. ∀x では、すべての x で∀xP が真であれば真、
∃x では、ある x で∃xP が真であれば真
述語論理式の解釈
 論理式 A の真偽は固体の取り方で異なる






定義域の取り方
固体定数
固体変数
関数記号
定義域と述語記号の対応関係
述語への真偽の割り当て
 論理式 A の解釈は多数存在する
述語論理式の解釈例
 論理式 ∀x(P(x)∨Q(f(x), a))
 解釈例
 D = {スペード、ハート、ダイヤ、クラブ}
 a = クラブ
 f: f(スペード)=ハート、 f(ハート)=スペード、
f(ダイヤ)=クラブ、 f(クラブ)=ハート
 P(x) : 「x は赤いマークである」
 Q(x, y) : 「x は y より順位が高い」
述語論理式の解釈例
 Q(x, y) : 「x は y より順位が高い」
 (x, y) ∈ {(スペード、ハート)、
(スペード、ダイヤ)、
(スペード、クラブ)、
(ハート、ダイヤ)、
(ハート、クラブ)、
(ダイヤ、クラブ)}
のとき、Q(x, y) は真
述語論理式の解釈例
 x = スペード
 P(スペード)∨Q(f(スペード), クラブ)
= P(スペード)∨Q(ハート, クラブ) = F∨T = T
 x = ハート
 P(ハート)∨Q(f(ハート), クラブ)
= P(ハート)∨Q(スペード, クラブ) = T∨T = T
 x = ダイヤ
 P(ダイヤ)∨Q(f(ダイヤ), クラブ)
= P(ダイヤ)∨Q(クラブ, クラブ) = T∨F = T
述語論理式の解釈例
 x = クラブ
 P(クラブ)∨Q(f(クラブ), クラブ)
= P(クラブ)∨Q(ダイヤ, クラブ) = F∨T = T
 したがって、
 ∀x(P(x)∨Q(f(x), a)) = T となる
論理式の解釈
 論理式 A がある解釈 I に対して真
 A は充足可能
 I は A のモデル
 論理式 A があらゆる解釈に対して常に真
 A は恒真(妥当)
 論理式 A を真とする解釈が存在しない
 A は充足不能(恒偽)
述語論理式の論理的帰結
 いくつかの論理式 A1, A2, ・・・, An
 すべての Ai が真となるあらゆる解釈で A が真
 トートロジーである命題論理の論理的帰結と同じ
述語論理の恒真式
 恒真式




あらゆる定義域について真
固体変数のあらゆる割り当てについて真
関数記号へのあらゆる関数について真
述語記号へのあらゆる述語について真
 命題論理式の命題変数
 述語論理式を代入しても恒真な述語論理式
恒真式の例
 P⇒(Q⇒P)
 P : ∀x∃y(A(x)⇒B(x, y))
 Q : ∀xC(x)
 P, Q を代入すると
 ∀x∃y(A(x)⇒B(x, y))
⇒ (∀xC(x) ⇒ ∀x∃y(A(x)⇒B(x, y)))
 上の述語論理式は恒真
 ∀x(P(x)⇒P(x)) も恒真式
述語論理式の恒真性
 恒真であれば、証明可能
 導出原理(この講義で説明予定)
 一般的な論理式
 恒真かどうかを判定する方法は存在しない
 高階述語の場合は、恒真でも証明できない
 ゲーデルの完全性定理
 公理から導かれる定理式は恒真式である
 逆(恒真式ならば定理式である)も成り立つ