Which Hypothese can be found with Inverse

情報科学基礎論
演習と応用
山本章博
京都大学情報学研究科
http://www.i.kyoto-u.ac.jp/~akihiro
恒真式と定理式
形式的証明(1)
AB=AC
BAC = CAB
AB=AC  AC=AB
AC=AB
AB=AC
BAC = CAB AC=AB  AB=AC
(BAC = CAB AC=AB  AB=AC) DBAC  DCAB
DBAC  DCAB  ABC= ACB DBAC  DCAB
ABC = ACB
形式的証明(2)
p
p
r
q
p
r 
q 
(
s
r

q
p

q

p
t
s
)
s
t
形式的証明(3)



証明は命題中に用いられている論理結合子
 (ならば)
(かつ)
の用法に従って構成されている．
用法と構成の関係は，命題が何を表している
かには依存しない．
表記法
j
q
d
jq
jq
d
d
推論規則(1)

推論規則：命題から命題を導くための規則


命題中の論理結合子の用法で定まる
命題 j と j z から z を導く
“jと j z が成り立つので, zも成り立つ”
j
jz
z
推論規則(2)
j
z
jz
j
jz
z
jz
[j ]
…
z
j  z
jz
j
jz
z
[j ][z ]
…
…
jzqq
q
j
z
jz
推論規則(3)
[j ]
…
^
j
[j ][z ]
…
…
zj
jz
j
j
z
jz
^
z
^
j
j j
j
j
jz
推論規則(4)
j[a]
"xj [x]
a は変数で，j [a]の上
にある仮定に自由に出
現してはならない
j[t]
$ xj [x]
t は項
"xj[x]
j [t]
t は項
$ xj [x]
[j [a]]
...
q
q
a は変数で，q の上にある
仮定とqに自由に出現して
はならない
公理

公理：証明なしで正しさを認める命題
証明の始点


証明：命題から命題を次々と導く連鎖Þ始点が必要
公理の設定が考察対象領域を決めてしまう．
例前出の証明で用いる公理
 等号の対称性: AB=AC  AC=AB
 角の対称性: BAC=CAB
 合同: AB=EF AC=EG BAC=FEG  DABC=DEFG
 合同な三角形の角が等しい:
DBAC  DCAB  ABC= ACB
数学的定理と定理式


数学的定理: 個別の前提(公理)を用いて，証明
可能な命題の集合
G|- j
数学的理論:前提(公理)となる命題の集合から
証明可能な命題の集合
定理式: 個別の前提(公理)を用いなくても証明
可能な命題
|- j
推論規則のみに依存
定理式の例(1)
|- (( p) ( q))  (q  p)
[( p) ( q)]
q
[ p]
[q]
^
p
q p
(( p) ( q))  (q  p)
定理式の例(2)
|- (( p) ( q))  (p  q)
[( p) ( q)]
p
[p]
[p  q]
^
[( p) ( q )]
q
[q]
^
^
 (p  q)
(( p) ( q))  (p  q)
否定, 論理和, 論理積の性質
交換律
結合律
分配律
冪等律
零元
単位元
補元
x+ y = y + x
xy = y x
(x + y) + z = x + (y + z)
(x y)z = x (y z)
(x + y) z = x z + y z
x y + z = (x + z)(y + z)
x+x=x
xx=x
x+ 0 = x
x・0 = 0
x ・1 = x
x +1=1
x+x=1
xx=0
1 = 0,
0=1
二重否定
x=x
ド・モルガン律 x + y = x y, x y = x + y
2項(2引数)論理演算
2項（2引数）論理演算は24種類
x y f1
f16
0 0 0 0 0 0 0 0 0 0 1 1 1 1 1 1 1 1
0 1 0 0 0 0 1 1 1 1 0 0 0 0 1 1 1 1
1 0 0 0 1 1 0 0 1 1 0 0 1 1 0 0 1 1
1 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1
論理積 x y
論理和 x + y
同値 x  y
含意 x  y
代表的な論理演算
論理積
論理和
x
y
xy
0
0
0
x y x+y
0 0
0
0
1
1
1
0
1
0
0
1
0 1
1 0
1 1
1
1
1
否定
x
y
0
1
1
0
恒真式



恒真式: 命題変数へどのような真偽値の代入を
行っても1となる論理式
|=j
論理演算の定義によって決まる
論理演算に関する“公式”に対して



変数 x, y, z,…を命題変数p, q, r,…に置換える
演算記号 +, ・,
を , , に置換える
等号 = を  に置換える
を施して得られる論理式は恒真式
恒真式の例(1)
|=(( p)  ( q))  (q  p)
x
0
0
1
1
y
0
1
0
1
x
1
1
0
0
y xy yx
1
1
1
0
0
0
1
1
1
0
1
1
(x  y) (y  x)
1
1
1
1
恒真式の例(2)
|=(( p) ( q))  (p  q)
x
0
0
1
1
y
0
1
0
1
x
1
1
0
0
y
1
0
1
0
x y
1
0
0
0
x+y x+y
0
1
1
0
1
0
1
0
( x y ) (x+y)
1
1
1
1
健全性と完全性


健全性:|- j ならば |=j
完全性:|=j ならば |- j
命題の構造と証明(1)
AB=AC
BAC = CAB
AB=AC  AC=AB
AC=AB
AB=AC
BAC = CAB AC=AB  AB=AC
(BAC = CAB AC=AB  AB=AC) DBAC  DCAB
DBAC  DCAB  ABC= ACB DBAC  DCAB
ABC = ACB
命題の構造と証明(2)
B=C
BC=CB
BC=CB
B=C  C=B
C=B
B=C
 C=B  B=C
BC=CB  C=B  B=C
DBAC = DCAB 
AB=AC
 DBAC = DCAB
DBAC = DCAB
AB=AC
述語論理の論理式と意味(1)


論理式は，命題を記号化したもの
述語論理では，命題中の主述を表現
論理式中で用いられる記号が何を表現してい
るかは，表現する人が決める
 命題の正しさは，
命題中の個々の記号が何を表しているのか
接続詞の使い方
一般性の表現
で決まる．

量化子のない論理式の解釈

解釈 I ： Herbrand base Bから{0, 1}への関数



基礎原子論理式に真偽値を“代入”する
{0, 1}n 内の1点
解釈 I のもとでの論理式の解釈
1. 命題定数の解釈値
I (□) = 0, I (■) = 1
2. 論理演算子
I (j  z ) = I (j) ・ I (z )
I (j  z ) = I (j) + I (z )
I (j  z ) = I (j)  I (z )
I ( j ) = I (j)
述語論理の論理式の解釈（１）
基礎原子論式の解釈 I
D : 考察対象全体からなる集合(領域)
IC : 対象(定数)記号をD中の対象に写す写像
IF : 関数記号をDnからDへの関数へ写す写像
IP : 述語記号をDnから{0,1}への関数へ写す写像
例 geq (s(s(0)), s(0))
 D : 自然数の集合N
 IC (0) :自然数の 0
 IF (s) :次の自然数
 IP (geq) : 自然数の順序関係 

述語論理の論理式の解釈（２）



命題定数，論理演算子の解釈は量化子の
ない場合と論理と同じ
I("x (j [x])) ：
x にD中の任意の対象 c を“代入” したときに，
常にI(j [c]) = 1であれば I("x (j [x])) =1
そうでなければ I("x (j[x])) = 0
I($x (j [x])) ：
D中の対象 c で， x に c を“代入” したときに，
I(j [c]) = 1なるものがあれば I($x (j [x])) =1
そうでなければ I($x (j [x])) = 0
述語論理の論理式の解釈（3）
例 "x "y geq(s(x), y)
 自然数 4, 2をx, y に代入して I (geq(5, 2))=1
 自然数 2, 4をx, y に代入して I (geq(3, 4))=0
I ("x "y geq(s(x), y))=0
述語論理の論理式の解釈（4）
記号の解釈は一般にいくつでも種類与えられる
例 "x geq(s(x), x)
 解釈１ D : 自然数の集合N
IC (0) :自然数の 0
IF (s) : 次の自然数
IP (geq) : 自然数の順序関係 
解釈１’ IP (geq) : =
 解釈２
D : 平面 p
IC (0) :原点
IF (s) : 原点と対称点
IP (geq) : 一直線上にある

例(1)
("x geq(x,0))("y"z(geq(y,z) geq(s(y),s(z)))
 ("w geq(s(w)), s(0)))
例(2)
|- ( r(a)  r(e(e(a,a), a)) )
$x  r(x)  r(e(x, a))
Cf.
|- ( r(a)  r( s( s(a))) )$x r(x)  r(s(x))

Download Report