数理論理学(鹿島亮)2

論理式の構成に使用できる記号

変数記号

a, b, c,…n, m, x, y, z,…

定数記号

zero,one,two, omega, unity, rt

関数記号

⊕, ⊙, ⊗,suc

命題記号

A, B, C,…

述語記号

=, ⧀, P, Q, R

論理記号

⊥, ¬, ∧, ∨, →, ∀, ∃

補助記号

括弧、カンマ

論理式の構成に使用できる記号は断らない限りここに列挙したものだけである

項の定義

変数記号は項である

定数記号は項である

t1,t2が項であるならば、

(t1⊕t2), (t1⊙t2), (t1⊗t2), suc(t1) は項である

こうしておけば、関数記号を増やしたときに項の定義を書き換えなくても済むけど

ちゃんと記載して定義したほうが色々便利なのかも？(帰納法とか)

一般の言語でやると難しいから初心者への配慮

具体的的な関数に対して定義しているだけ

上記に該当する記号列以外は項ではない

0suc()

こういうものは項ではないと言い切れる

論理式の定義

命題記号は論理式である

t1,t2が項ならば

(t1=t2), Q(t1), (t1⧀t2), P(t1), R(t1,t2)は論理式である

φとψが論理式でxが変数記号ならば

⊥, (¬φ), (φ∧ψ), (φ∨ψ), (φ→ψ), (∀xφ), (∃xφ)は論理式である

括弧は曖昧さがない範囲で省略しても良い

⊤って論理式があってもあんまり面白くないのかな

⊤普通に導入することがある

¬AをA→⊥の略記とするために、導入したくなるけど、⊤は導入するほどのモチベーションがない

((φ1∧φ2)∧φ3)∧… みたいなものは論理式と言えるのか

該当しない

有限回しか適用できない

((φ1∧φ2)∧φ3)∧…の1つ前の論理式が何？となる

(φ∧ψ)

あんまりメタ言語とかのことよく分かりませんが、メタ変数には任意の項や論理式を入れられると考えていいんでしたっけ？

図式schemeと言うこともある

原子論理式の定義

論理式の定義の上2つと、⊥

複合論理式の定義

原子論理式以外の論理式

新たな関数記号や述語記号を追加する場合は、関数や論理式の定義の文面に追加すれば良い

論理式の例

¬(A∧B)

一番外の括弧は省略されている

∀x∀y((x=y)→(suc(x)=suc(y)))

∃x∃y∃z((¬(x=y)∧¬(x=z))∧¬(y=z))

∃x∃y∃z(¬(x=y)∧¬(x=z)∧¬(y=z))

こんな感じで中の括弧を省略してもいい気がする

変数の指し得る対象が3個以上あるという意味

元が3つ以上

変数の指し得る有限個であるは書くことはできない

可算個の論理式では、変数の指し得る対象が無限個あることが言える

∃x∃y∃z∃z1(¬(x=y)∧¬(x=z)∧¬(y=z)∧¬(x=z1)∧¬(y=z1),¬(z=z1))

4つ異なっている

4C2の論理式の∧で結んだ論理式

nC2の論理式の∧で結んだ論理式でn個以上あると言う論理式が書ける

p82に証明がある

論理式ではない例

∃x(x)

論理式ではないことの証明

∃x(x)が論理式であると仮定する

論理式の定義より、∃x(x)が論理式ならばxは論理式である。

よって、xは論理式である

xは変数記号である

よって、xは論理式ではない

矛盾する。よって、∃x(x)が論理式でない

∀A(A→A)

Aは命題記号であるので束縛できない

論理式ではないことの証明

∀A(A→A)が論理式であると仮定する

論理式の定義より、∀A(A→A)が論理式ならばAは変数記号である。

よって、Aは変数記号である

Aは命題記号である

よって、Aは変数記号でない

矛盾する。よって、∀A(A→A)が論理式でない

任意の論理式や任意の項の表し方の約束

Γ, Δなどギリシャ大文字は論理式の集合

φ,ψ,ρなどギリシャ小文字は論理式

論理式中で量化子(∀や∃)によって指示されている記号の出現のこと

(…∀x(…x…)…)

(…∃x(…x…)…)

BVar(φ)

論理式φ中に束縛出現する変数記号全体の集合

束縛出現になっていない変数記号の出現のこと

FVar(φ)

論理式φ中に自由出現する変数記号全体の集合

項t中に出現する変数記号全体の集合

Var(t)

項tをsuc(n)とすると

Var(t) = {n}

FVar(φ) = ∅ のとき、φを閉論理式と呼ぶ

Var(t) = ∅ のとき、tを閉項と呼ぶ

例

φを∀a∀y( ∃x(z=x) ∧ (x⧀(y⊕x)) )とする

FVar(φ) = {z, x}

(x⧀(y⊕x))のxは束縛されていない

BVar(φ) = {a, y, x}

∃x(z=x)のxは束縛されている

xのように一つの論理式の中で、自由束縛の両方に出現する場合もある

aのように量化子の後ろにしか現れない場合も束縛出現と呼ぶ

φ中のxにtは代入不可能であるとは以下の2条件を満たす変数記号yが存在すること

条件

φは(…∀y(…x…)…)または(…∃y(…x…)…)という形をしている

xはφ中の自由出現

y ∈ Var(t)

φは論理式

xは変数記号

tは項

上記の2条件を満たす変数記号yが存在しないこと

x replaced by tと読んだりする

分かればなんて呼んでもいい

代入時に意図しない束縛条件が生まれないような状態のこと

例

∀a∀y( ∃x(z=x) ∧ (x⧀(y⊕x)) )

代入可能な例

xにzeroを代入する

代入可能かを調べる

Var(zero) = ∅

よってy ∈ Var(t)を満たす変数記号yは存在しない

xにzeroを代入可能

変数を含まないようなものはzero⊕zeroなど閉項であれば代入できる

∀a∀y( ∃x(z=x) ∧ (x⧀(y⊕x)) )[zero/x]

∀a∀y( ∃x(z=x) ∧ (zero⧀(y⊕zero)) )

自由出現しているxを全てzeroに置き換える

∃x(z=x)のxは自由出現していないので置き換えない

代入不可能な例

zにsuc(x)を代入する

代入可能かを調べる

Var(suc(x)) = {x}

∀a∀y( ∃x(z=x) ∧ (x⧀(y⊕x)) )は∃x(z=x)という形を持つ

よって代入不可能である

代入不可能であるが無理やり代入してみる

∀a∀y( ∃x(z=x) ∧ (x⧀(y⊕x)) )[suc(x)/z]

∀a∀y( ∃x(suc(x)=x) ∧ (suc(x)⧀(y⊕suc(x))) )

∃x(suc(x)=x)というsuc(x)が意図しない束縛をされてしまっている

自然演繹の推論規則

別の教科書で見かけたやつだけど、Cosenseで証明書く時に楽なので、これで証明書くかも

量化子の部分は授業でやってなくて授業メモなかったので適当に書いてます

導出図は時間とやる気があればdrawioで書きます

table:∧導入

前提番号 行番号 論理式 推論規則

1 1 A

2 2 B

1,2 3 A∧B 1,2.∧導入

table:∧除去

前提番号 行番号 論理式 推論規則

1 1 A∧B

1 2 A 1,∧除去

table:∧除去

前提番号 行番号 論理式 推論規則

1 1 A∧B

1 2 A 1,∧除去

table:∨導入

前提番号 行番号 論理式 推論規則

1 1 A

1 2 A∨B 1,∨導入

table:∨導入

前提番号 行番号 論理式 推論規則

1 1 B

1 2 A∨B 1,∨導入

table:∨除去

前提番号 行番号 論理式 推論規則

1 1 A∨B

2 2 A→C

3 3 B→C

1 4 C 1,2,3',∨除去

table:→導入

前提番号 行番号 論理式 推論規則

1 1 A

… … …

1,… 1' C

… 2 A→C 1-1',→導入

table:→除去

前提番号 行番号 論理式 推論規則

1 1 A→C

2 2 A

1,2 3 C 1,2,→除去

table:¬導入

前提番号 行番号 論理式 推論規則

1 1 A→⊥

1 2 ¬A 1,¬導入

table:¬除去

前提番号 行番号 論理式 推論規則

1 1 A

2 2 ¬A

1,2 3 ⊥ 1,2,¬除去

table:背理法 RAA

前提番号 行番号 論理式 推論規則

1 1 ¬A→⊥

1 2 A 1,背理法

table:爆発律

前提番号 行番号 論理式 推論規則

1 1 ⊥

1 2 A 爆発律

table:∀導入

前提番号 行番号 論理式 推論規則

1 2 ∀xA 1,∀導入

※

xは変数記号

yはA中の解消されていない仮定の中にも∀xAの中にも自由出現しない変数記号で、A中のxに代入可能なもの

変数条件とかって呼ばれますっけ？

table:∀除去

前提番号 行番号 論理式 推論規則

1 1 ∀xA

※

xは変数記号

tはA中のxに代入可能な項

table:∃導入

前提番号 行番号 論理式 推論規則

1 2 ∃xA 1,∃導入

※

xは変数記号

tはA中のxに代入可能な項

table:∃除去

前提番号 行番号 論理式 推論規則

1 1 ∃xA

1,2 3 C 1,2,∃除去

※

xは変数記号

yはA中のAy/x以外の解消されていない仮定の中にも、∃xAやCの中にも自由出現しない変数記号で、A中のxに代入可能なもの

これ間違っているので、GoodNoteで書き直して直したい

Cを導くための導出図𝜜上にyが出現してほしくないと書きたい

変数条件

table:等号公理

前提番号 行番号 論理式 推論規則

1 t=t 等号公理

※

tは項

table:等号規則

前提番号 行番号 論理式 推論規則

2 2 t=s

※

xは変数記号

t,s,はA中のxに代入可能な項

仮定の解消

→導入は仮定の解消をする

公理

公理は導出図の葉にあっても仮定とは見なされない

↓↓表を使って量化子を含む論理式の証明をやった経験がなくてわかりにくかったので、GoodNoteに導出図書きます

table:例9 ∀x(φ→ψ), ∃xφ ⊢ ∃xψ

前提番号 行番号 論理式 推論規則

1 1 ∀x(φ→ψ) 仮定

1,3 5 ∃xψ 4,∃導入

6 6 ∃xφ 仮定

1,6 7 ∃xψ 4,6,∃除去

※

ただしyは∀x(φ→ψ)中に出現しない変数記号とする

単に代入できるものを取ってきているだけ

そうしないと適用できない推論があるのかもしれない？ちゃんと理解できていない

∀x(x=y)

(y=y)

出現する自明な論理式が出てきてしまう

∀x((x=x)→(y=y))

((y=y)→(y=y))

自明な形になっちゃうので、出現していない変数記号を代入している

代入の分配

p33

例8

https://scrapbox.io/files/6769ab9eee50188fc23f9872.jpg

∀除去した時のyはyは(P(x)→Q(x))中のxに代入可能な項であるかを調べてみる

(P(x)→Q(x))中のxにyが代入可能であるとは、以下の2条件を満たす変数記号zが存在しないこと

条件

(P(x)→Q(x))は(…∀z(…x…)…)、(…∃z(…x…)…)という形をしている

ただし、xは(P(x)→Q(x))中の自由出現

z ∈ Var(y)

よってyは代入可能

∃導入した時のyはQ(x)中のxに代入可能な項であるかを調べてみる

Q(x)中のxにyが代入可能であるとは、以下の2条件を満たす変数記号zが存在しないこと

Q(x)は(…∀z(…x…)…)、(…∃z(…x…)…)という形をしている

ただし、xはQ(x)中の自由出現

z ∈ Var(y)

よってyは代入可能

∃除去した時の条件を満たしているかを調べて見る

条件

FVar(∀x(P(x)→Q(x)) = ∅であり、FVar(P(x)) = {x}であり、FVar(Q(x)) = {x}である

yはP(x)中のxに代入可能

Qのときと同じようにyは代入できる

よって∃除去可能

例9

例8のP(x)とQ(x)を一般の論理式にしたもの

https://scrapbox.io/files/67698eef001a9e1be0181168.jpg

なぜそういうyがとってこれるのか

使える変数記号の個数は無限個ある

∀x(φ→ψ)中に出現する変数の個数は有限個

∀x(φ→ψ)は有限の文字列なため

∀除去した時のyはyは(φ→ψ)中のxに代入可能な項であるかを調べてみる

(φ→ψ)中のxにyが代入可能であるとは、以下の2条件を満たす変数記号zが存在しないこと

条件

(φ→ψ)は(…∀z(…x…)…)、(…∃z(…x…)…)という形をしている

ただし、xは(φ→ψ)中の自由出現

この条件は満たしている可能性がある

z ∈ Var(y)

yは∀x(φ→ψ)に出現しない変数記号としているため

y ∉ BVar(∀x(φ→ψ)) かつ y ∉ FVar(∀x(φ→ψ))

Var(y) = {y}

よって条件1と合わせると(φ→ψ)は(…∀y(…x…)…)または(…∃y(…x…)…)という形をしている

つまりy ∈ BVar(φ→ψ)

y ∉ BVar(∀x(φ→ψ)) と y ∈ BVar(φ→ψ)が同時に成り立ってしまいこれは矛盾する

したがってこのようなzは存在しない

「yは∀x(φ→ψ)に出現しない変数記号」じゃなくて、「yは∀x(φ→ψ)に束縛変数として出現しない変数記号」

まで緩められそうだけどどうなんだろ？

なんか良くない気がする…

というか束縛変数を含んでいない項は一般に代入可能なのかな

自由変数の代入でも気をつける必要がある例

x=y

x = x

∀x(x = x)

∀x∀y(x=y)

∃導入した時のyはyはψ中のxに代入可能な項であるかを調べてみる

ψ中のxにyが代入可能であるとは、以下の2条件を満たす変数記号zが存在しないこと

ψは(…∀z(…x…)…)、(…∃z(…x…)…)という形をしている

ただし、xはψ中の自由出現

この条件は満たしている可能性がある

z ∈ Var(y)

yはψに出現しない変数記号としているため

y ∉ BVar(ψ) かつ y ∉ FVar(ψ)

Var(y) = {y}

よって条件1と合わせると(ψ)は(…∀y(…x…)…)または(…∃y(…x…)…)という形をしている

つまりy ∈ BVar(ψ)

y ∉ BVar(∀x(φ→ψ)) と y ∈ BVar(φ→ψ)が同時に成り立ってしまいこれは矛盾する

したがってこのようなzは存在しない

よってyは代入可能

やっぱり「yは∀x(φ→ψ)に出現しない変数記号」じゃなくて、「yは∀x(φ→ψ)に束縛変数として出現しない変数記号」

まで緩められそうだけどどうなんだろ？

∃除去で問題になるのでは？

∃除去した時の条件を満たしているかを調べて見る

条件

yはφ→ψに出現しない変数記号としているため

y ∉ BVar(φ→ψ) かつ y ∉ FVar(φ→ψ)

よって

y ∉ BVar(φ) かつ y ∉ FVar(φ)

y ∉ BVar(ψ) かつ y ∉ FVar(ψ)

y ∉ FVar(φ→ψ)であり、y ∉ FVar(φ)であり、y ∉ FVar(ψ)である

yは前の議論によりより、ψ中のxに代入可能

よって∃除去可能

ちゃんと必要十分になっている

例10

⊢∀x∀y((x=y)→(y=x))

a,b,x,yが異なる変数記号でないといけないのを確かめたい

∀除去の方で全部異なっていないと変数の条件が満たせないのかな

例11

φ⊢φ

自明な証明

例12

⊢t=t

等号公理の証明

⊢の使用方法

Γ⊢φ

「Γからφが導出できる」と読む

そのような導出図を「Γからφへの導出図」などと呼ぶ

φは論理式

Γは論理式の集合(有限でも無限でも)

定義

Γのある有限部分集合Γ'が存在して、「解消されていない仮定の集合がΓ'で、結論がφの導出図が存在すること」

解消できていない仮定が無限にある場合どんな問題があるのかな

導出図が存在して、解消できていない仮定が最低でも無限個ある時、導出図を木と見ると無限に道が存在してしまいそう

つまり、長い推論をしなくてはいけなそうな気がする

こういうのを扱いたくないのかな

導出図は有限個の長さである必要がある

推論規則も有限回しか適用できない

導出図の定義から解消されていない仮定の集合が有限集合である必要がある

Γがなぜ無限個で良いのか？

ZFCなどの数学には公理の数は無限個のものが結構ある

Γ = {γ1, γ2, … ,γn}のとき、集合を表す括弧を省略して以下のように書いても良い

γ1, γ2, … ,γn ⊢ φ

特にΓが空集合であるなら

⊢ φ

Γ⊬φ

定義

Γ⊢φでないこと

つまり解消されていない仮定がすべてΓの要素で結論がφであるような導出図が存在しないこと

Γ⊢φは「Γを公理とする数学理論において命題φが証明できる」を表していると考えて良い

演習問題

解かずに3章読み始めちゃったのでちゃんと解いていきたい

2.1

ア

P(zero) = ⊥ は論理式ではない

=は述語記号である

P(zero) = ⊥ が論理式であるためには、両側(P(zero)、⊥)がともに項でなくてはならない

P(zero)は論理式である

⊥は論理式である

よって、P(zero) = ⊥ は論理式ではない

イ

∀zero(suc(zero)=suc(zero)) は論理式ではない

zeroは定数記号である

∀で束縛できるのは変数記号のみである

が定数記号を束縛してしまっている

よって、∀zero(suc(zero)=suc(zero)) は論理式ではない

ウ

x = y = z は論理式ではない

論理式の括弧が省略されていると考える

(x = y) = z のとき

(x = y) は論理式である

zは項である

(x = y) = z が論理式であるためには、両側((x = y) 、z)がともに項でなくてはならない

よって、(x = y) = z は論理式ではない

同様にx = (y = z)の場合も論理式ではないといえる

p194解説の補足

x = y = z を(x = y)∧(y = z) の省略表現とするなら、x = y = z は論理式になる

エ

1 + 1 = 2 は論理式ではない

1, 2, +という記号は論理式の構成に使用できる記号ではない

よって、1 + 1 = 2 は論理式ではない

p194解説の補足

ただし、これらの記号を論理式の構成に使用できる記号に追加すれば、1 + 1 = 2 は論理式になる

オ

∀x⊥ は論理式である

再帰的に構成して確かめる

⊥は論理式である

xは変数記号である

よって∀x⊥は論理式である

2.2

ア

https://scrapbox.io/files/6779298fb3b0ad1d46569319.jpg

イ

https://scrapbox.io/files/677929a092615416ad9004e0.jpg

→導入するときには別に仮定として使っている論理式じゃなくてもいいんだよね

ウ

https://scrapbox.io/files/677929ad49718f8f1a405b56.jpg

論理式の順番はあんまり気にしなくてもよい

エ

https://scrapbox.io/files/677929ba33823e017ca6bf5a.jpg

2種類の∧除去がある

これ片方取り除いたらどうなるんだろ(大変そう)

自然演繹で背理法とか爆発律はよく取り除かれたりするイメージだけど他に何か取り除かれたりするのだろうか

オ

https://scrapbox.io/files/677929c40aa16240d27d707a.jpg

2種類の∨除去がある

カ

https://scrapbox.io/files/677929dfc1cc70f076e09112.jpg

キ

https://scrapbox.io/files/677929e95957d12a2ac79ece.jpg

これは最小論理でも証明可能

ク

https://scrapbox.io/files/677929fc5b8dff54e97092f8.jpg

これは二重否定導入と違って、背理法が必要

ケ

https://scrapbox.io/files/677a02e77211c39176e8a28b.jpg

量化子を別の変数に置き換えている

解答だと∀除去でP(y)としてる

個人の好み。読みやすいように

コ

https://scrapbox.io/files/67792a116e1817393701da1d.jpg

∀で括っている

逆は成り立たなそう

PかQが全ての要素で成り立ってる必要がある(左の方が強い)

P 1 0 1 0

Q 0 1 0 1

P∨Q 1 1 1 1

サ

https://scrapbox.io/files/67792a32658eb20a5ff6b2e7.jpg

これを逆にするとsucが単射であるという論理式になる(はず)

問題にないけど、2.2解いてた時のメモ

https://scrapbox.io/files/67792a365957d12a2ac7a01e.jpg

∃導入は同じ変数のうち好きなものだけ束縛できる

∀導入の変数の条件を一番右は満たしていない

∀y(a=y)の中に束縛する変数であるaが存在している

2.3

シ

https://scrapbox.io/files/677944a7c1cc70f076e13dfe.jpg

文字列とかを入れ替える時のものを思い出した

ス

https://scrapbox.io/files/677944ac58a6267fc1a3f312.jpg

思ったより難しかった…

((A→B)→A)を仮定してAを導きたい

¬Aと((A→B)→A)が矛盾すれば、¬Aは背理法使ってAにできる

¬Aも仮定して良い

そのために、A→Bを得たい

((A→B)→A)とA→BからAが得られるため

¬Aは仮定しても良い

¬A⊢A→Bを証明すれば良い

A,¬AからBを導けば良い

爆発律があればできる

セ

https://scrapbox.io/files/677944afae6f50ce5f47b2d1.jpg

これもまぁまぁ難しかった

Pa∨Aと∨除去を使って、∀xP(x)∨Aを導きたい気持ちがあるけど、うまくいかない

Paを仮定してもAは当然導けないし、∀xP(x)も変数条件を満たさないので導けない

∀xP(x)∨AにはAが含まれているから、A∨¬Aがあれば、Aを仮定したときは∀xP(x)∨Aが簡単に導ける

¬Aを仮定したときも驚くことに、∀xP(x)が導けるので∀xP(x)∨Aが導ける

A∨¬Aだし、真ん中にAを除去

https://scrapbox.io/files/677944b22b022761a8a976b6.jpg

https://scrapbox.io/files/677944b55b8dff54e9714698.jpg

2.4

https://scrapbox.io/files/677a1259d046eefd57c587cd.jpg

https://scrapbox.io/files/677949aba9a3c883c1209591.jpg

2.5

https://scrapbox.io/files/677a1282c1cc70f076e49c13.jpg

https://scrapbox.io/files/677949d4ecf9c4ecbc6a7b96.jpg

https://scrapbox.io/files/677949d8a6af7b2a7257afd2.jpg

2.6

https://scrapbox.io/files/677949f1b818aedea9b434f9.jpg

∀導入している部分が自然演繹の文法に反している

yは以下の条件を満たさなければならない

yはP(y)の中にも∀xP(x)の中にも自由出現しない変数記号で、P(x)中のxに代入可能なもの

yはP(y)に自由出現しているので、∀導入することはできないが、∀導入を適用してしまっている

対象領域が1個の時にも前件が真になる？ので、成り立ちそう

述語論理の対象領域って空ではないという条件があった気がする

2.7

∀t( Even(t)→Odd(suc(t)) )

tであまり使わない方がいいかも

量化する記号にtを使わない方がかもしれない。解答例だとnを使っている

間違っているわけではない

∀t( ∃x(t=two⊗x)→∃x(suc(t)=suc(two⊗x)) )

https://scrapbox.io/files/67794a20569cfe1d40886cac.jpg

∀m( ( ∃n( Even(n)∧(m=suc(n)) ) ) → Odd(m) )

https://scrapbox.io/files/67794a252a113fe94b94e1ae.jpg

正確にいうと不思議に思っているのは、異なる論理式をどうして、「偶数に1を足したら必ず奇数になる」という風に同じように読めてしまうのか

もっと言うと、論理式を「偶数に1を足したら必ず奇数になる」という風に読めることが不思議

論理式は真理値を持っているけど、「偶数に1を足したら必ず奇数になる」

2.8

ア

φ1,φ2,…,φn ⊢ ψ

解消されていない仮定の集合が{φ1,φ2,…,φn}のある有限部分集合であり、結論がψの導出図が存在する

イ

⊢ (φ1→(φ2→…→(φn→ψ)…))

解消されていない仮定の集合が空集合であり、結論が(φ1→(φ2→…→(φn→ψ)…))の導出図が存在する

括弧を省略するときに→を右結合がことが多い気がする

その理由はこれだったりするのかな

ア⇒イ

φ1,φ2,…,φn ⊢ ψが成り立っているとする

このときφn,ψに対して→導入をする

仮定φnが解消される

φ1,φ2,…,φn-1 ⊢(φn→ψ)が成り立つ

すなわち、解消されていない仮定の集合が{φ1,φ2,…,φn-1}のある有限部分集合となる

これをφn-1からφ1まで繰り返す

⊢ (φ1→(φ2→…→(φn→ψ)…)) が成り立つ

すなわち、解消されていない仮定の集合が{}のある有限部分集合つまり空集合となる

イ⇒ア

⊢ (φ1→(φ2→…→(φn→ψ)…))が成り立っているとする

φ1,φ2,…,φnを仮定する

φ1, (φ1→(φ2→…→(φn→ψ)…))に→除去をして、(φ2→…→(φn→ψ)…)を得る

φiと得られた論理式に→除去を繰り返す

ψを得る

解消されていない仮定の集合はφ1,φ2,…,φnである

(φ1→(φ2→…→(φn→ψ)…))は仮定なしで成り立っているとしているので、解消されていない仮定の集合に含まれない

よって、φ1,φ2,…,φn ⊢ ψが成り立つ

(教科書ではそう書いてないけど)ちゃんと証明するならnに関する数学的帰納法で証明していく

これで書いてみよ