2014年度情報論理学第 9回講義

2014 年度情報論理学第 9 回講義
2014 年 6 月 24 日 (火)
青戸等人 (東北大学電気通信研究所)
目次
- 変数の自由出現と束縛出現
- 代入と代入の記法
- 述語論理式に対する代入
量化子とそのスコープ
定義 1. ∀ x や ∃ x を量化子という．述語論理式に ∀ xA や
∃ xA の形が含まれるとき， A の部分を量化子 ∀ x や ∃ x のス
コープとよぶ．
例．述語論理式 ∀x (∀y P(x, y) ∧ Q(x)) を考える．この述語論
理式には， ∀x と ∀y の 2 つの量化子が出現する． ∀x のスコー
プは， ∀y P(x, y) ∧ Q(x)． ∀y のスコープは， P(x, y)．
例．述語論理式 ∀x (∀x P(x) ∧ ∀x Q(x) ∧ R(x)) を考える．こ
の述語論理式には，量化子 ∀x が 3 箇所に出現する．そのス
コープは左から順に， ∀x P(x) ∧ ∀x Q(x) ∧ R(x)， P(x)， Q(x)．
1
変数の束縛出現と自由出現
定義 2. 変数 x の原子論理式における出現が量化子 ∀ x や
∃ x のスコープに入っていないとき，その出現を自由出現と
よび，量化子 ∀ x や ∃ x のスコープに入っているとき，その
出現を束縛出現とよぶ．
例．述語論理式 ∀x P(x, y) において，変数 x の出現は束縛出
現，変数 y の出現は自由出現．
例．述語論理式 ∀x (∀y P(x, y) ∧ Q(x, y)) を考える． P(x, y) に
現われる変数 x, y の出現は束縛出現． Q(x, y) に現われる変数
x, y の出現については，変数 x の方は束縛出現だが，変数 y
の方は自由出現．
2
述語論理式に含まれる自由変数の集合
自由出現をもつ変数を自由変数とよぶ．
定義 3. A を述語論理式とするとき， A に含まれる自由変
数集合 FV(A) を以下のように定義する． FV(A) =
S

V(ti)
(A = P (t1, . . . , tn) のとき )

1≤i≤n



V(s) ∪ V(t)
(A = s ≈ t のとき )



∅
(A ∈ {⊥, ⊤} のとき )

FV(B)
(A = ¬B のとき )




FV(B) ∪ FV(C) (A = B ◦ C, ◦ ∈ {∧, ∨, →} のとき )


 FV(B) \ {x}
(A = QxB, Q ∈ {∀, ∃} のとき )
V(t) は項 t に含まれる変数集合を表わすことに注意．
3
例．述語論理式 A = ∀y (x ≈ y ∧ P(y, z)) を考える．このと
き， FV(A) = {x, z}．つまり，自由変数は x と z．
例．述語論理式 A = ∀y (x ≈ y) ∧ P(x, y) を考える．このと
き， FV(A) = {x, y}． (左側の y は束縛出現だが，右側の y
は自由出現であることに注意． )
演習 4. 以下を求めよ．
(1) FV(f(x) ≈ g(x, y))
(2) FV(∀x ∀y P(f(x), g(y, z)))
(3) FV(∀y (x + y ≤ 10) ∧ ∀x P(x, y))
4
(解答)
(1) FV(f(x) ≈ g(x, y)) = V(f(x)) ∪ V(g(x, y))
= V(x) ∪ (V(x) ∪ V(y)) = {x, y}
(2) FV(∀x ∀y P(f(x), g(y, z)))
= FV(∀y P(f(x), g(y, z))) \ {x}
= (FV(P(f(x), g(y, z))) \ {y}) \ {x}
= ({x, y, z} \ {y}) \ {x} = {z}
(3) FV(∀y (x + y ≤ 10) ∧ ∀x P(x, y))
= FV(∀y (x + y ≤ 10)) ∪ FV(∀x P(x, y))
= (FV(x + y ≤ 10) \ {y}) ∪ (FV(P(x, y)) \ {x})
= ((V(x + y) ∪ V(10)) \ {y}) ∪ ((V(x) ∪ V(y)) \ {x})
= (((V(x) ∪ V(y)) ∪ ∅) \ {y}) ∪ ({x, y} \ {x})
= ({x, y} \ {y}) ∪ ({x, y} \ {x}) = {x} ∪ {y} = {x, y}
5
述語論理式の解釈と自由変数
自由変数に関連して，述語論理式の解釈は以下のような
性質をもつ．証明は付録に示す．
補題 5. M を L-構造， v, v ′ を M 上の付値とする．
(1) 任意の変数 x ∈ V(t) について v(x) = v ′(x) が成立す
るとき， [[t]]v = [[t]]v′ ．
(2) 任意の自由変数 x ∈ FV(A) について v(x) = v ′(x) が
成立するとき， [[A]]v = [[A]]v′ ．
つまり，異なる付値であっても，自由に出現する変数に
ついての値が等しければ，述語論理式の解釈は等しくなる．
6
束縛の導入・消去
自由変数集合を利用した次の同値式が成立する．
束縛の導入・消去 (x ∈
/ FV(C) とする )
∀x C ∼
∃x C ∼
= C，
=C
例． ∀y P(x) ∼
= P(x)
∀y ∀x P(x) ∼
= ∀x P(x)
∃y (∀x P(x) ∧ ∀y Q(y)) ∼
= ∀x P(x) ∧ ∀y Q(y)
7
(証明)
∀x C ∼
/ FV(C) とする )
= C (x ∈
C をシグニチャ L 上の述語論理式とし， x ∈
/ FV(C) とする．
このとき，任意の L-構造 M と， L-構造 M への任意の付値
v について， [[∀x C]]v = [[C]]v となることを示せばよい．
条件 x ∈
/ FV(C) から，補題 5(2) より， [[C]]v[a/x] = [[C]]v が
成立することに注意すると，
[[∀x C]]v = T ⇔ 任意の a ∈ |M| について，[[C]]v[a/x] = T
⇔ 任意の a ∈ |M| について，[[C]]v = T
⇔ [[C]]v = T
よって， [[∀x C]]v = [[C]]v ．
∃x C ∼
= C ．省略．
8
変数の束縛
定義 6. 変数 x の A における自由出現は， ∀ x A や ∃ x A に
おいて，量化子 ∀ x や ∃ x によって束縛されるという．
“束縛されている ” という関係 (束縛関係) を矢印で表わして
みる．
例．
∀y (∀x Q(x, y) ∧ Q(x, y))
変数 x のどんな束縛出現も，ある量化子 ∀ x や ∃ x のス
コープにあるが，その出現をスコープにもつ量化子の中で
1 番内側の ∀ x A や ∃ x A を考えると， A で変数 x は自由に出
現しているはず．従って，どんな束縛出現も，ある量化子に
より束縛されている．
9
例．
∀x (∀x P(x) → ∃x R(x) → Q(x))
先頭の ∀x により束縛されているのは， ∀x P(x) → ∃x R(x) →
Q(x) で自由な出現のみ．つまり， Q(x) の x のみ．
逆に，出現する変数の方から見ると， 1 番近い量化子に
束縛される．
演習 7. 次の述語論理式における束縛関係を図示せよ．
∀y (∀x (x + y ≥ 0) → ∀x (|x + y| ≈ x + y))
10
(解答)
∀y (∀x (x + y ≥ 0) → ∀x (|x + y| ≈ x + y))
11
束縛変数の名前替え
自由変数でない変数を束縛変数とよぶことがある．しか
し，変数の束縛出現では，どこに束縛されているかが重要
で，その変数が何かということは重要でない．従って，量
化子 Q x とそれにより束縛されている変数出現を一斉に他
の変数に置きかえても論理的には同値である．この変数置
き換え操作を束縛変数の名前替えとよぶ．
以下の述語論理式は全て論理的に同値であり，相互に変
換してもよい．
∀y (∀x (x + y ≥ 0) → ∀x (|x + y| ≈ x + y))
∀z (∀x (x + z ≥ 0) → ∀x (|x + z| ≈ x + z))
∀z (∀y (y + z ≥ 0) → ∀x (|x + z| ≈ x + z))
∀z (∀y (y + z ≥ 0) → ∀y (|y + z| ≈ y + z))
12
∀y (∀x (x + y ≥ 0) → ∀x (|x + y| ≈ x + y))
∀z (∀x (x + z ≥ 0) → ∀x (|x + z| ≈ x + z))
∀z (∀y (y + z ≥ 0) → ∀x (|x + z| ≈ x + z))
∀z (∀y (y + z ≥ 0) → ∀y (|y + z| ≈ y + z))
13
束縛変数の名前替えの正しさ
補題 8. 項 t における変数 x の出現すべてを変数 y ∈
/ V(t)
に置き替えて得られる項を t′ とおき，述語論理式 A におけ
る変数 x の自由出現すべてを変数 y ∈
/ FV(A) に置き替えて
得られる述語論理式を A′ とおく．また， M を L-構造， v を
M 上の付値とする．
(1) 任意の a ∈ |M| について， [[t]]v[a/x] = [[t′]]v[a/y]．
(2) 任意の a ∈ |M| について， [[A]]v[a/x] = [[A′]]v[a/y]．
(3) [[∀x A]]v = [[∀y A′]]v ， [[∃x A]]v = [[∃y A′]]v ．
この補題から，以下が導かれる．
定理 9. A を述語論理式， A′ を A から束縛変数の名前替え
で得られる述語論理式とする．このとき， A ∼
= A′ ．
14
目次
- 変数の自由出現と束縛出現
- 代入と代入の記法
- 述語論理式に対する代入
14
代入
定義 10. 変数集合 V から項集合 T(F, V ) への関数を代入と
よぶ．
代入の例 1．
+(xi−1, xi+1)
−(xi)
(i が奇数のとき )
(それ以外のとき )


 −(0)
σ(xi) =
−(+(0, x0))

 xi
(i = 0 のとき )
(i = 1 のとき )
(それ以外のとき )
σ(xi) =
代入の例 2．
15
代入の準同型拡張
定義 11. σ を代入とする． σ を項 t に適用した結果 σ(t) を
次のように定義する．
σ(t)
t ∈ V のとき
σ(t) =
f (σ(t1), . . . , σ(tn)) t = f (t1, . . . , tn) のとき
2 番目の場合分けは f が定数の場合も含むことに注意．
演習 12.
σ(xi) =
+(xi−1, xi+1)
xi
(i が奇数のとき )
(それ以外のとき )
とするとき， σ(+(−(x3), −(0))) を計算せよ．
16
σ(xi) =
+(xi−1, xi+1)
xi
(i が奇数のとき )
(それ以外のとき )
のとき，
σ(+(−(x3), −(0))) =
=
=
=
=
+(σ(−(x3)), σ(−(0)))
+(−(σ(x3)), σ(−(0)))
+(−(σ(x3)), −(σ(0)))
+(−(+(x2, x4)), −(σ(0)))
+(−(+(x2, x4)), −(0))
σ は，項の変数の部分だけを σ で変更し，残りはそのままに
するような関数になっている．
17
代入の記法
代入が有限個の変数しか変更しないとき，つまり，


t1
(i = k1 のとき )




(i = k2 のとき )
 t2
σ(xi) =
..
.............



tm
(i = km のとき )


 x
(それ以外のとき )
i
(ただし， ti =
6 xki (1 ≤ i ≤ m)) と書けるとき，この代入 σ
を
[xk1 := t1, xk2 := t2, . . . , xkm := tm]
と書く．
18
演習 13. σ = [x1 := +(x1, x2), x2 := −(x1)] とする．この
とき，以下を求めよ．
(1) σ(−(−(0)))
(2) σ(+(x1, x1))
(3) σ(+(x2, x3))
19
(1)
σ(−(−(0))) = −(σ(−(0)))
= −(−(σ(0)))
= −(−(0))
σ(0) = 0 となることに注意．
(2)
σ(+(x1, x1)) = +(σ(x1), σ(x1 ))
= +(+(x1, x2), +(x1, x2))
x1 が 2 箇所あっても定義通りに計算すればよい．
σ(+(x2, x3)) = +(σ(x2), σ(x3 ))
= +(−(x1), x3)
x3:= は代入 [. . .] の中に現わないので， σ(x3) = x3 となるこ
とに注意
(3)
20
代入の制限
定義 14. σ を代入， x を変数とするとき， σ|x を以下により
与えられる代入と定義する：
x
(x = y のとき )
σ|x(y) =
σ(y)
(x 6= y のとき )
つまり， σ|x は， x 以外について， σ と同じように代入する．
例． σ = [x := a, y := b, z := c] とする．このとき，
σ|x(f(x, y, z)) = f(x, b, c)
σ|y(f(x, y, z)) = f(a, y, c)
σ|z(f(x, y, z)) = f(a, b, z)
21
目次
- 変数の自由出現と束縛出現
- 代入と代入の記法
- 述語論理式に対する代入
21
述語論理式に対する代入のアイデア
代入を述語論理式に適用する．述語論理式に対する代入
の適用は，変数の自由な出現だけを項に置きかえる．
例． σ = [x := s(y)] とする．このとき，
σ(x < 0 ∧ ∀x (x ∈ u)) = s(y) < 0 ∧ ∀x (x ∈ u)
このように，束縛出現は代入により置き代わらない．
しかし，このアイデアだけでは問題があり，もうひと工夫
する (次ページ )．
22
素朴な代入の問題点
代入される項に，量化子のスコープにある変数が存在す
ると，束縛関係を破壊してしまう．
例 (誤り )． σ = [x := y + 1] とする．このとき，
σ(∀y (y ∈ u → x < y)) = ∀y (y ∈ u → y + 1 < y)
としてしまうと， ∀y に対する束縛関係が変わってしまう！
∀y (y ∈ u → x < y)
∀y (y ∈ u → y + 1 < y)
そこで，束縛関係を保存して代入を行うために次に説明
する便宜法を用いる．
23
束縛変数の名前替えの便宜法
約束 15. [束縛変数の名前替えの便宜法] 述語論理式の代
入においては，代入する項にある自由変数と代入される項
にある束縛変数が代入によって重なる場合は，代入の前に
束縛変数の名前替えを行って重なりをなくした後，代入を
行う．
正しい代入
σ = [x := y + 1] とする．
σ(∀y (y ∈ u → x < y)) = σ(∀z (z ∈ u → x < z))
= ∀z (z ∈ u → y + 1 < z)
この約束に従えば，束縛関係は代入によって変わらない．
24
述語論理式に対する代入
束縛変数の名前替えの便宜法のもとで，代入の定義を行
う．
定義 16. 述語論理式 A へ代入 σ を行って得られる述語論理
式 σ(A) を次のように定義する． σ(A) =


P (σ(t1), . . . , σ(tn))




(σ(s) ≈ σ(t))



A
(¬σ(B))





(σ(B) ◦ σ(C))


 (Qxσ| (B))
x
(A = P (t1, . . . , tn) のとき )
(A = (s ≈ t) のとき )
(A ∈ {⊥, ⊤} のとき )
(A = ¬B のとき )
(A = (B ◦ C), ◦ ∈ {∧, ∨, →} のとき )
(A = (QxB), Q ∈ {∀, ∃} のとき )
25
代入の制限 |x を用いることにより，変数の束縛出現は代
入によって置き換わらないことに注意．
例． σ = [x := s(y)] とする．
=
=
=
=
=
=
σ(∀y (x ≈ y × x) ∧ ∀x (x ≈ y + 0))
σ(∀y (x ≈ y × x))∧σ(∀x (x ≈ y + 0))
σ(∀w (x ≈ w × x))∧σ(∀x (x ≈ y + 0)) (束縛変数の名前替え )
∀w (σ|w(x ≈ w × x))∧σ(∀x (x ≈ y + 0))
∀w (s(y) ≈ w × s(y))∧σ(∀x (x ≈ y + 0))
∀w (s(y) ≈ w × s(y))∧∀x (σ|x(x ≈ y + 0))
∀w (s(y) ≈ w × s(y))∧∀x (x ≈ y + 0)
定義 16 自体には記述されていないが，束縛変数の名前替
えを用いることに注意．
26
演習 17. 以下で与えられる σ に対して σ(∀z(x×z ≈ y×z))
を計算せよ．
(1) σ = [x := 0]， (2) σ = [u := 0]，
(3) σ = [z := 0]， (4) σ = [x := z].
27
解．
(1)
(2)
(3)
(4)
∀z (0 × z ≈ y × z)
∀z (x × z ≈ y × z)
∀z (x × z ≈ y × z)
∀w (z × w ≈ y × w)
(4) は，「束縛変数の名前替えの便宜法」により，代入を
行う前に，束縛変数の名前替えを行う必要がある．名前替
えに用いる変数は， z, y 以外なら， w でなくてもよい．
28
述語論理式の解釈と代入
代入に関連して，述語論理式の解釈は以下のような性質
をもつ．証明は付録に示す．
補題 18. s をシグニチャ L 上の項， x を変数， v を L-構造 M
への付値とする．
(1) 任意の項 t について， [[[x := s]t]]v = [[t]]v[[[s]]v /x]．
(2) 任意の述語論理式 A について， [[[x := s]A]]v = [[A]]v[[[s]]v /x]．
29
代入と全称/存在
代入を用いた次の恒真式が成立する．
代入と全称/存在
∀x A → [x := t](A)，
[x := t](A) → ∃x A
(証明)
∀x A → [x := t](A)
A をシグニチャ L 上の述語論理式とする． M を任意の L-構
造， v を L-構造 M への任意の付値とし， [[∀x A]]v = T と仮
定する．
解釈の定義から，任意の a ∈ |M| について， [[A]]v[a/x] = T．
従って， [[t]]v ∈ |M| であるから， [[A]]v[[[t]]v /x] = T．
30
ここで，補題 18(2) より， [[[x := t]A]]v = [[A]]v[[[t]]v /x] である
から， [[[x := t]A]]v = T．
[x := t](A) → ∃x A
A をシグニチャ L 上の述語論理式する． M を任意の L-構造，
v を L-構造 M への任意の付値とし， [[[x := t]A]]v = T と仮
定する．
補題 18(2) より， [[[x := t]A]]v = [[A]]v[[[t]]v /x] であるから，
[[A]]v[[[t]]v /x] = T．よって， [[t]]v ∈ |M| であるから，ある
a ∈ |M| が存在して [[A]]v[a/x] = T．
従って， [[∃A]]v = T．
31
∀x A → [x := t](A) の逆向きの含意，つまり， [x :=
t](A) → ∀x A は一般には成立しない．
演習 19. シグニチャを h{a0}, {P1}i とするとき， P(a) →
∀x P(x) の反例を与えよ．
同様に， [x := t](A) → ∃x A の逆向きの含意，つまり，
∃x A → [x := t](A) は一般には成立しない．
演習 20. シグニチャを h{a0}, {P1}i とするとき， ∃ xP(x) →
P(a) の反例を与えよ．
32
全称一般化
∀x A → [x := t](A) の特殊形である ∀x A → A も，一般
には成立しない．しかし，次の命題は成立する．
定理 21. 任意の述語論理式 A と任意の変数 x について， A
が恒真であれば， ∀x A も恒真．
(証明) A を恒真な述語論理式とする．すると，定義より，
任意の L-構造 M， L-構造 M への任意の付値 v について，
[[A]]v = T．従って，特に，任意の a ∈ |M| について，
[[A]]v[a/x] = T．よって，定義から， [[∀x A]]v = T．よって，
任意の L-構造 M について， [[∀x A]]M = T となる．ゆえに，
∀x A は恒真．
33
まとめ
• 変数の自由出現と束縛出現
自由変数集合
束縛関係と束縛変数の名前替え
• 述語論理式における代入
代入は自由変数のみを置き換える
束縛変数の名前替えの便宜法
連絡： 7 月 15,22 日は休講，期末試験は 7 月 29 日の予定です．
34
(補題 5 の証明) (1) t に関する帰納法で，任意の x ∈ V(t) に
ついて v(x) = v ′(x) ならば， [[t]]v = [[t]]v′ となることを示す．
t = x ∈ V の場合．
このとき， V(t) = {x} であるから，仮定より， [[t]]v = v(x) =
v ′(x) = [[t]]v′ ．
t = f (t1, . . . , tn) の場合．
Sn
このとき，定義から V(t) = i=1 V(ti)．
よって， 1 ≤ i ≤ n とするとき， V(ti) ⊆ V(t)．従って，仮定
より，任意の x ∈ V(ti) について v(x) = v ′(x)．よって，帰
納法の仮定から， [[ti]]v = [[ti]]v′ が成立する．
以上より，
[[f (t1, . . . , tn)]]v = f M([[t1]]v , . . . , [[tn]]v )
= f M([[t1]]v′ , . . . , [[tn]]v′ )
= [[f (t1, . . . , tn)]]v′
35
(2) 述語論理式 A に関する帰納法で，任意の x ∈ FV(A) に
ついて v(x) = v ′(x) ならば [[A]]v = [[A]]v′ となることを示す．
A = P (t1, . . . , tn) の場合．
Sn
このとき，定義から FV(A) = i=1 V(ti)．
よって，仮定より，任意の x ∈ V(ti) について， v(x) = v ′(x)．
従って， (1) から， [[ti]]v = [[ti]]v′ ．
よって，
[[P (t1, . . . , tn)]]v = T
⇔ h[[t1]]v , . . . , [[tn]]v i ∈ P M
⇔ h[[t1]]v′ , . . . , [[tn]]v′ i ∈ P M
⇔ [[P (t1, . . . , tn)]]v′ = T
よって，解釈の取り得る値は T, F であるから，
[[P (t1, . . . , tn)]]v = [[P (t1, . . . , tn)]]v′ ．
A = s ≈ t の場合．省略
36
A ∈ {⊥, ⊤}， A = ¬B の場合．省略
A = B ∧ C の場合．
このとき，定義から， FV(A) = FV(B) ∪ FV(C)．
よって，仮定より，任意の x ∈ FV(B) について v(x) = v ′(x)，
また，任意の x ∈ FV(C) について v(x) = v ′(x)．
よって，帰納法の仮定より， [[B]]v = [[B]]v′ かつ [[C]]v] =
[[C]]v ．
よって，
[[B ∧ C]]v = T ⇔ [[B]]v = T かつ [[C]]v = T
⇔ [[B]]v′ = T かつ [[C]]v′ = T
⇔ [[B ∧ C]]v′ = T
よって，解釈の取り得る値は T, F であるから，
[[B ∧ C]]v = [[B ∧ C]]v′ ．
37
A = B ∨ C ， A = B → C の場合. 省略．
A = ∀y B の場合．
このとき，定義から FV(A) = FV(B) \ {y}．
よって，仮定より，任意の x ∈ FV(B) と任意の a ∈ |M| に
ついて， v[a/y] = v ′[a/y] が成立する．よって，帰納法の仮
定より， [[B]]v[a/y] = [[B]]v′[a/y]．従って，
[[∀y B]]v = T
⇔ 任意の a ∈ |M| について，[[B]]v[a/y] = T
⇔ 任意の a ∈ |M| について，[[B]]v′[a/y] = T
⇔ [[∀y B]]v′ = T
よって，解釈の取り得る値は T, F であるから， [[∀x B]]v =
[[∀x B]]v′ ．
A = ∃y B の場合．省略．
38
(補題 8 の証明) (1) t に関する帰納法で， [[t]]v[a/x] = [[t′]]v[a/y]
となることを示す．
t が変数の場合．
t = x の場合は， [[t]]v[a/x] = a = [[t′]]v[a/y] より明らか． t = y
の場合は， y ∈ V(y) となるから仮定に矛盾． t = z ∈
/ {x, y}
の場合は， [[t]]v[a/x] = v(z) = [[t′]]v[a/y] より明らか．
t = f (t1, . . . , tn) の場合．
このとき，項 ti における変数 x の出現すべてを変数 y に置き
替えて得られる項を t′i とすると， t = f (t′1, . . . , t′n) とおけ，
帰納法の仮定より [[ti]]v[a/x] = [[t′i]]v[a/y] が成立する．よって，
[[f (t1, . . . , tn)]]v[a/x] = f M([[t1]]v[a/x] , . . . , [[tn]]v[a/x] )
= f M([[t′1]]v[a/y], . . . , [[t′n]]v[a/y])
= [[f (t′1, . . . , t′n)]]v[a/y]
39
(2) 述語論理式 A に関する帰納法で，任意の付値 v につい
て， [[A]]v[a/x] = [[A′]]v[a/y] となることを示す．
A = P (t1, . . . , tn) の場合．
このとき，項 ti における変数 x の出現すべてを変数 y に置き
替えて得られる項を t′i とすると， A′ = P (t′1, . . . , t′n) とおけ，
(1) から， [[ti]]v[a/x] = [[t′i]]v[a/y]．
よって，
[[P (t1, . . . , tn)]]v[a/x] = T
⇔ h[[t1]]v[a/x] , . . . , [[tn]]v[a/x] i ∈ P M
⇔ h[[t′1]]v[a/y], . . . , [[t′n]]v[a/y]i ∈ P M
⇔ [[P (t′1, . . . , t′n)]]v[a/y] = T
よって，解釈の取り得る値は T, F であるから，
[[P (t1, . . . , tn)]]v = [[P (t1, . . . , tn)]]v′ ．
A = s ≈ t の場合．省略
40
A ∈ {⊥, ⊤}， A = ¬B の場合．省略
A = B ∧ C の場合．
このとき， B および C における変数 x の自由出現すべて
を変数 y に置き替えて得られる項をそれぞれ B ′, C ′ とする
と， A′ = B ′ ∧ C ′ とおける．よって，帰納法の仮定より，
[[B]]v[a/x] = [[B ′]]v[a/y] かつ [[C]]v[a/x] = [[C ′]]v[a/y] ．
よって，
[[B ∧ C]]v[a/x] = T ⇔ [[B]]v[a/x] = T かつ [[C]]v[a/x] = T
⇔ [[B ′]]v[a/y] = T かつ [[C ′]]v[a/y] = T
⇔ [[B ′ ∧ C ′]]v[a/y] = T
よって，解釈の取り得る値は T, F であるから，
[[B ∧ C]]v[a/x] = [[B ′ ∧ C ′]]v[a/y]．
A = B ∨ C ， A = B → C の場合. 省略．
41
A = ∀z B の場合．
x = z のときは， A′ = A となり自明． y = z のと
きは， y ∈ FV(A) に矛盾． z ∈
/ {x, y} のとき．このと
き， B における変数 x の自由出現すべてを変数 y に置き替
えて得られる項をそれぞれ B ′ とすると， A′ = ∀z B ′ とお
ける．よって，帰納法の仮定より，任意の b ∈ |M| につ
いて， [[B]]v[b/z][a/x] = [[B ′]]v[b/z][a/y] が成立する．従って，
[[B]]v[a/x][b/z] = [[B ′]]v[a/y][b/z] が成立．以上より，
[[∀z B]]v[a/x] = T
⇔ 任意の b ∈ |M| について，[[B]]v[a/x][b/z] = T
⇔ 任意の b ∈ |M| について，[[B ′]]v[a/y][b/z] = T
⇔ [[∀z B ′]]v[a/y] = T
よって， [[∀x B]]v = [[∀x B]]v′ ．
A = ∃y B の場合．省略．
42
(3) (2) より，任意の a
[[A′]]v[a/y]．よって，
∈
|M| について [[A]]v[a/x]
=
[[∀x A]]v = T
⇔ 任意の a ∈ |M| について，[[A]]v[a/x] = T
⇔ 任意の b ∈ |M| について，[[A′]]v[a/y] = T
⇔ [[∀y A′]]v = T
[[∃x A]]v = T
⇔ ある a ∈ |M| が存在して，[[A]]v[a/x] = T
⇔ ある a ∈ |M| が存在して，[[A′]]v[a/y] = T
⇔ [[∃y A′]]v = T
よって， [[∀x A]]v = [[∀y A′]]v および [[∃x A]]v = [[∃y A′]]v が成
立する．
43
(定理 9 の証明) A′ を A から束縛変数の名前替えで得られる
述語論理式とすると， A′ は， A から補題 8 の操作を何回か繰
り返して得られる．よって，補題 8(3) と ∼
= の合同関係性か
ら， A ∼
= A′ ．
44
(補題 18 の証明) (1) t に関する帰納法で， [[[x := s]t]]v =
[[t]]v[[[s]]v /x] を示す．
t が変数の場合．
t = x の場合．
[[[x := s]x]]v = [[s]]v = v(x) = [[x]]v[[[s]]v /x] より成立．
t = y 6= x の場合．
[[[x := s]y]]v = [[y]]v = v(y) = [[y]]v[[[s]]v /x] より成立．
t = f (t1, . . . , tn) の場合．
このとき，帰納法の仮定より，任意の 1 ≤ i ≤ n について，
[[[x := s]ti]]v = [[ti]]v[[[s]]v /x] が成立する．
従って，
45
[[[x := s](f (t1, . . . , tn))]]v
= [[f ([x := s](t1), . . . , [x := s](tn)]]v
= f M([[[x := s](t1)]]v , . . . , [[[x := s](tn)]]v )
= f M([[t1]]v[[[s]]v /x], . . . , [[tn]]v[[[s]]v /x])
= [[f (t1, . . . , tn)]]v[[[s]]v /x]
(2) 述語論理式 A に関する帰納法で， [[[x := s]A]]v =
[[A]]v[[[s]]v /x] となることを示す．
A = P (t1, . . . , tn) の場合．
(1) より， [[[x := s]ti]]v = [[ti]]v[[[s]]v /x]．
よって，
[[[x := s]A]]v = T
⇔ [[[x := s]P (t1, . . . , tn)]]v = T
⇔ [[P ([x := s]t1, . . . , [x := s]tn)]]v = T
46
⇔ h[[[x := s]t1]]v , . . . , [[[x := s]tn]]v i ∈ P M
⇔ h[[t1]]v[[[s]]v /x], . . . , [[tn]]v[[[s]]v /x]i ∈ P M
⇔ [[P (t1, . . . , tn)]]v[[[s]]v /x] = T
よって，解釈のとる値は T, F であるから，
[[[x := s]ti]]v = [[ti]]v[[[s]]v /x]．
A = s ≈ t の場合．省略
A ∈ {⊥, ⊤} の場合．省略
A = ¬B の場合．
帰納法の仮定より， [[[x := s]B]]v = [[B]]v[[[s]]v /x]．
よって，
[[[x := s]¬B]]v = T ⇔ [[[x := s]B]]v = F
⇔ [[B]]v[[[s]]v /x] = F ⇔ [[¬B]]v[[[s]]v /x] = T.
よって，解釈のとる値は T, F であるから，
[[[x := s]A]]v = [[A]]v[[[s]]v /x]．
47
A = B ∧ C ， A = B ∨ C ， A = B ∧ C の場合．省略．
A = ∀y B の場合．
x = y の場合．
このとき，解釈の定義から， [[[x := s](∀x B)]]v = [[∀x B]]v ．
ここで， x ∈
/ FV(∀x B) であることから，
補題 5(2) より， [[∀x B]]v = [[∀x B]]v[[[s]]v /x]．
よって， [[[x := s]∀x B]]v = [[∀x B]]v[[[s]]v /x]．
x 6= y の場合．
このとき， [[[x := s]∀y B]]v = [[∀y [x := s]B]]v ．
よって，
[[[x := s]∀y B]]v = T
⇔ [[∀y [x := s]B]]v = T
⇔ 任意の a ∈ |M| について， [[[x := s]B]]v[a/y] = T
ここで， b = [[s]]v[a/y] とおくと，
48
帰納法の仮定より， [[[x := s]B]]v[a/y] = [[B]]v[a/y][b/x] ．
また， x 6= y より， [[B]]v[a/y][b/x] = [[B]]v[b/x][a/y] ．
一方，束縛変数の名前替えの便宜法より， y ∈
/ V(s)．
よって，補題 5(2) より， b = [[s]]v[a/y] = [[s]]v ．
以上より，
任意の a ∈ |M| について， [[[x := s]B]]v[a/y] = T
⇔ 任意の a ∈ |M| について， [[B]]v[a/y][b/x] = T
⇔ 任意の a ∈ |M| について， [[B]]v[b/x][a/y] = T
⇔ 任意の a ∈ |M| について， [[B]]v[[[s]]v /x][a/y] = T
⇔ [[∀y B]]v[[[s]]v /x] = T
よって，解釈のとる値は T, F であることから，
[[[x := s]∀y B]]v = [[∀y B]]v[[[s]]v /x]．
A = ∃y B の場合．省略．
49

Download Report