第 4 章 $-translation に基づくクラス定義 25
4.4 論理式のクラスの構文論的な定義
定義 4.4 論理式のクラスQ, R, Iを以下のように同時帰納的に定義する. ここで, P は 原子論理式, Q, Q1, Q2はQに属する論理式, R, R1, R2はRに属する論理式, I, I1, I2は Iに属する論理式をそれぞれ表す.
· ⊥, P, Q1∧Q2, Q1∨Q2, ∀xQ, ∃xQ, I →Q∈ Q,
· ⊥, R1∧R2, ∀xR, I →R∈ R,
· ⊥, P, I1∧I2, I1 ∨I2, ∃xI, R →I ∈ I,
命題 4.2 論理式Aについて
· A∈ Q ならば IQCA→A$.
· A∈ R ならば IQC ¬$¬A→A$.
· A∈ I ならば IQC A$ → ¬$¬$A.
証明
論理式Aの複雑さに関する同時帰納法により証明する.
Basis:
· A≡ ⊥のときA$ ≡$.
⊥ ∈ Q, R, Iであるが
(1) ⊥
$ (⊥i)
(1)⊥ →$, (→I)
(2)¬$¬⊥
(1)⊥
(1)¬⊥ (→I)
$
(2)¬$¬⊥ →$, (→I)
(1)$
¬$¬$⊥ (→I)
(1)$→ ¬$¬$⊥ (→I)
はそれぞれIQCの証明図となる. したがって, IQC A → A$, IQC ¬$¬A → A$, IQCA$ → ¬$¬$A.
· A≡P (≡ ⊥)のときA$ ≡ ¬$¬$P. P ∈ Qであるが
(1)¬$P (2)P
$
(1)¬$¬$P (→I)
(2)P → ¬$¬$P (→I) はIQCの証明図となるため,IQC A→A$.
定義4.4よりP ∈ R. P ∈ Iであるが
(1)¬$¬$P
(1)¬$¬$P → ¬$¬$P (→I) はIQCの証明図となるため,IQC A$ → ¬$¬$A.
Induction steps:
· A≡B∧CのときA$ ≡B$∧C$.
A ∈ Qならば定義4.4よりB, C ∈ Qで, 帰納法の仮定からIQC B → B$, IQC C →C$. よって
(1)B∧C B
I.H...
..
B →B$ B$
(1)B ∧C C
I.H...
..
C →C$ C$ B$∧C$
(1)B∧C →B$∧C$ (→
I)
はIQCの証明図となるため,IQC A→A$.
A ∈ Rならば 定義4.4よりB, C ∈ Rで, 帰納法の仮定からIQC ¬$¬B → B$, IQC ¬$¬C →C$. よって
(5)¬$¬(B∧C)
(2)¬B
(1)B∧C
⊥ B
(1)¬(B ∧C) (→I)
$
(2)¬$¬B (→I)
I.H..
¬$¬B..→B$ B$
(5)¬$¬(B ∧C)
(4)¬C
(3)B∧C
⊥ C
(3)¬(B ∧C) (→I)
$
(4)¬$¬C (→I)
I.H..
¬$¬C..→C$ C$
B$∧C$
(5)¬$¬(B∧C)→ B$∧C$ (→I) はIQCの証明図となるため,IQC ¬$¬A→A$.
A ∈ I ならば 定義4.4よりB, C ∈ I で, 帰納法の仮定からIQC B$ → ¬$¬$B, IQCC$ → ¬$¬$C. よって
(4)B$∧C$ B$
I.H...
..
B$ → ¬$¬$B
¬$¬$B
(4)B$ ∧C$ C$
I.H...
..
C$ → ¬$¬$C
¬$¬$C
(3)¬$(B∧C)
(2)B (1)C B∧C
$
(1)¬$C (→I)
$
(2)¬$B (→I)
$
(3)¬$¬$(B ∧C) (→I)
(4)B$∧C$ → ¬$¬$(B∧C) (→
I)
はIQCの証明図となるため,IQC A$ → ¬$¬$A.
· A≡B →CのときA$ ≡B$ →C$.
A∈ Qならば 定義4.4よりB ∈ I, C ∈ Qで, 帰納法の仮定からIQC B$ → ¬$¬$B, IQCC →C$. よって
(3)B$
I.H...
..
B$ → ¬$¬$B
¬$¬$B
(2)¬$C$
(1)B (4)B →C
C
I.H...
..
C →C$ C$
$
(1)¬$B (→I)
$
(2)¬$¬$C$ (→I)
系4.1 ....
¬$¬$C$ →C$ C$
(3)B$ →C$ (→
I)
(4)(B →C)→(B$ →C$) (→I) はIQCの証明図となるため,IQC A→A$.
A∈ Rならば定義4.4よりB ∈ I, C ∈ Rで, 帰納法の仮定からIQC B$ → ¬$¬$B, IQC ¬$¬C →C$. よって
(4)B$
I.H...
..
B$ → ¬$¬$B
¬$¬$B
(5)¬$¬(B →C)
(3)¬C
(2)B (1)B →C
⊥ C
(1)¬(B →C) (→I)
$
(2)¬$B (→I)
$
(3)¬$¬C (→I)
I.H...
¬$¬C..→C$ C$
(4)B$ →C$ (→I)
(5)¬$¬(B →C)→(B$ →C$) (→I) はIQCの証明図となるため,IQC ¬$¬A→A$.
A ∈ Iならば定義4.4よりB ∈ R, C ∈ I で, 帰納法の仮定からIQC ¬$¬B → B$, IQCC$ → ¬$¬$C. よって
(4)¬$(B →C)
(2)¬B (1)B
⊥ C (⊥i)
(1)B →C (→I)
$
(2)¬$¬B (→I)
I.H...
¬$¬B..→B$
B$ (5)B$ →C$ C$
I.H...
..
C$ → ¬$¬$C
¬$¬$C
(4)¬$(B →C)
(3)C
B →C (→I)
$
(3)¬$C (→I)
$
(4)¬$¬$(B →C) (→I)
(5)(B$ →C$)→ ¬$¬$(B →C) (→I) はIQCの証明図となるため,IQC A$ → ¬$¬$A.
· A≡B∨CのときA$ ≡ ¬$¬$(B$∨C$).
A ∈ Qならば定義4.4よりB, C ∈ Qで, 帰納法の仮定からIQC B → B$, IQC C →C$. よって
(3)B∨C
(2)¬$(B$∨C$)
(1)B
I.H...
..
B →B$ B$ B$∨C$
$
(2)¬$(B$∨C$)
(1)C
I.H...
..
C →C$ C$ B$∨C$
$
(1)$ (∨E)
(2)¬$¬$(B$∨C$) (→
I)
(3)B∨C → ¬$¬$(B$∨C$) (→I) はIQCの証明図となるため,IQC A→Ag.
定義4.4よりA∈ R.
A ∈ I ならば定義4.4よりB, C ∈ I で, 帰納法の仮定からIQC B$ → ¬$¬$B, MQCC$ → ¬$¬$C. よって
(6)¬$¬$(B$∨C$)
(4)B$∨C$
(3)B$
I.H...
..
B$ → ¬$¬$B
¬$¬$B
(5)¬$(B∨C)
(1)B B∨C
$
(1)¬$B (→I)
$
(3)C$
I.H...
..
C$ → ¬$¬$C
¬$¬$C
(5)¬$(B∨C)
(2)C B∨C
$
(2)¬$C (→I)
$
(3)$ (∨E)
(4)¬$(B$∨C$) (→I)
$
(5)¬$¬$(B∨C) (→I)
(6)¬$¬$(B$∨C$)→ ¬$¬$(B∨C) (→I)
はIQCの証明図となるため,IQC A$ → ¬$¬$A.
· A≡ ∀xBのときA$ ≡ ∀xB$.
A∈ Qならば定義4.4よりB ∈ Qで, 帰納法の仮定からIQCB →B$. よって
(1)∀xB B
I.H...
..
B →B$ B$
∀xB$
(1)∀xB → ∀xB$ (→I) はIQCの証明図となるため,IQC A→A$.
A∈ Rならば定義4.4よりB ∈ Rで,帰納法の仮定からIQC ¬$¬B →B$. よって
(3)¬$¬∀xB
(2)¬B
(1)∀xB
⊥ B
(1)¬∀xB (→I)
$
(2)¬$¬B (→I)
I.H...
¬$¬B..→B$ B$
∀xB$
(3)¬$¬∀xB → ∀xB$ (→I) はIQCの証明図となるため,IQC ¬$¬A→A$.
定義4.4よりA∈ I.
· A≡ ∃xBのときA$ ≡ ¬$¬$∃xB$.
A∈ Qならば定義4.4よりB ∈ Qで, 帰納法の仮定からIQCB →B$. よって
∃xB
¬$∃xB$ B
I.H...
..
B →B$ B$
∃xB$
$
$
¬$¬$∃xB$
∃xB → ¬$¬$∃xB$ はIQCの証明図となるため,IQC A→A$.
定義4.4からA∈ R.
A∈ Iならば定義4.4よりB ∈ Iで, 帰納法の仮定からIQCB$ → ¬$¬$B. よって
(5)¬$¬$∃xB$
(3)∃xB$
(2)B$
I.H...
..
B$ → ¬$¬$B
¬$¬$B
(4)¬$∃xB
(1)B
∃xB
$
(1)¬$B (→I)
$
(2)$ (∃E)
(3)¬$∃xB$ (→
I)
$
(4)¬$¬$∃xB (→I)
(5)¬$¬$∃xB$ → ¬$¬$∃xB (→I) はIQCの証明図となるため,IQC A$ → ¬$¬$A.
2
定義 4.5 論理式の集合Γについて,
任意のB ∈ΓとF V(A)∩BV(Γ) = ∅をみたす任意の論理式A に対しΓi B$[$/A]
となるときΓは$に関して閉じているという.
定理 4.2 論理式のクラスKを
I, K1∧K2, ∀xK, Q→K ∈ K
と帰納的に定義する(ただし, QはQに属する論理式, IはIに属する論理式, K, K1, K2 はKに属する論理式をそれぞれ表す).
任意のA∈ Kと, $に関して閉じている論理式の集合Γについて Γc A ならば Γi A
すなわち, KについてCQC+ ΓはIQC+ Γの保守的拡大となる.
証明
Aの複雑さに関する帰納法により証明する. なお, 束縛変数の付け替えを行うことによ り, 一般性を失うことなくF V(A)∩BV(Γ∪ {A}) =∅ とすることができる.
Basis:
·A∈ Iの場合.
定理4.1よりΓc AならΓ$ m A$. すなわち, conclusion が A$, open assumption の集 合がΓ$の部分集合であるようなMQCの証明図Dが存在する.
また, A∈ IよりIQCA$ → ¬$¬$Aなので,つぎの証明図
D ≡ D A$
IQC..
..
A$ → ¬$¬$A
¬$¬$A はIQCの証明図となる.
F V(A)∩BV(Γ∪ {A}) =∅より, 証明図Dの中の$にAを代入することができ, その ような証明図をD[$/A]とするとつぎの証明図
D≡
D[$/A]
(A→A)→A
(1)A
(1)A→A (→I) A
は conclusion がA, open assumption の集合がΓ$[$/A]の部分集合であるようなIQCの 証明図である.
いまF V(A)∩BV(Γ∪ {A}) = ∅であり, Γは$に関して閉じているため任意のB ∈Γ に対してΓ i B$[$/A]となり, conclusion がB$[$/A], open assumption の集合がΓの部 分集合であるようなIQCの証明図が存在する.
Dのすべての open assumption をこれらの証明図で置き換えたものもまたIQCの証 明図となる. すなわち, Γi A.
Induction steps:
·A≡B∧Cの場合.
Γc B ∧Cより, conclusion がB∧C, open assumption の集合がΓの部分集合である ようなCQCの証明図Dが存在する.
Dに∧Eを適用すると conclusionがそれぞれB, CであるようなCQCの証明図が2つ 得られる. すなわち Γc BかつΓc C.
ここで, B, C ∈ Kなので帰納法の仮定からΓi BかつΓi Cであり, conclusion がそ れぞれB,CとなるようなIQCの証明図が存在する.
これらのIQCの証明図に∧Iを適用した証明図もまたIQCの証明図なのでΓi B∧C.
·A≡ ∀xBの場合.
Γc ∀xBより, conclusion が∀xB, open assumption の集合がΓの部分集合であるよう なCQCの証明図Dが存在する.
Dに∀Eを適用するとconclusionがB[x/y] (ただしy∈F V(Γ))であるようなCQCの 証明図が得られる. すなわち Γc B[x/y].
ここで, B ∈ Kなので帰納法の仮定からΓ i B[x/y]であり, conclusion がB[x/y]とな るようなIQCの証明図が存在する.
このIQCの証明図に∀Iを適用した証明図(y∈Γよりconclusionが∀x(B[x/y])[y/x]≡
∀xBとなるようなものを作ることができる) もまたIQCの証明図なのでΓi ∀xB.
·A≡B →Cの場合.
Γc B →Cより, conclusion がB →C, open assumption の集合がΓの部分集合であ るようなCQCの証明図Dが存在する.
Dに対して
B D
B →C C
のように→Eを適用すると conclusionがCで, open assumption の集合にBが追加され たCQCの証明図が得られる. すなわち Γ∪ {B} c C.
ここで,B ∈ QよりIQCB →B$なのでΓ∪ {B}は$に関して閉じており,F V(C)⊆ F V(A),BV(Γ∪{B})⊆BV(Γ∪{A})よりF V(C)∩BV(Γ∪{B}) = ∅となり,またC ∈ K なので帰納法の仮定からΓ∪ {B} iCであり, conclusion がCとなるようなIQCの証明 図が存在する.
このIQCの証明図に→Iを適用した証明図もまたIQCの証明図なのでΓi B →C.
2
注 なお, Qは$に関して閉じている論理式の集合の一例となっている.
注 クラスKとWiの関係について, 例えば
· (P →Q)→(¬Q→ ¬P) ∈ K,Wi,
· (¬P →Q)→(¬Q→ ¬¬P) ∈ Wiだが∈ K,
· P →P ∨Q ∈ Kだが∈ Wi
などの論理式があり, K ∩ Wi =∅, K ⊆ Wi, Wi ⊆ Kであることがわかる.