演繹定理2
さトぅー
「さっきの逆も言える。これは簡単」
■meta thm0.1
Tを公理の集合とする。
T |- (φ⇒ψ)
ならば
T∪{φ} |- ψ
proof
1 φ [ax]
2 (φ⇒ψ) [Tの定理]
3 ψ [→el 1,2]
■
さトぅー
「だからT∪{φ} |- ψ」
エーリル
「はやい」
さトぅー
「meta thm0.0とmeta thm0.1を合わせて、演繹 定理って呼ばれてる」
天々城
「これがないと証明が吐くほど長くなるんだよナあ……」
さトぅー
「演繹定理は推論規則に読み替えできる」
『Tとφからψが証明できた。
だから、φなしでTから(φ→ψ)を証明できる』
つまり、次の推論規則を追加していい」
■⇒in el
φ [ax]
---
：
：
---
ψ
---[⇒in el φ]
(φ⇒ψ)
天々城
「el φって書いてるけど、これ除去だっけ」
さトぅー
「"落ちる"、"解消"、"キャンセル"とかあんまり言い方統一されてないみたい。
"除去"なら消えてる感じがつかめてると思うし、それでいこうかなって思ったの」
天々城
「了解」
エーリル
「これは絶対できるってわかったからショートカットしてるのか」
さトぅー
「定理ってそういうことよ。
面倒だからもうしない。
例えば、こんなのとかね」
■thm0.1
{ψ} |- (φ⇒ψ)
proof
1 ψ [ax]
2 (ψ⇒(φ⇒ψ)) [Ax1]
3 (φ⇒ψ) [⇒el 1,2]
■
エーリル
「１個増えた」
さトぅー
「そんな感じ。これで推論規則を増やす」
■⇒in
ψ
--------
(φ⇒ψ) [⇒in]
エーリル
「んー、ショートカットの威力を見せてほしい」
■例2の証明
{} |- (φ→(ψ→φ))
proof
------------------
さトぅー
「まず次を証明する」
{φ} |- (ψ→φ)
------------------
1 φ [ax]
2 (ψ→φ) [⇒in 1]
------------------
さトぅー
「ここで⇒in elでφ [ax]を消す」
------------------
3 (φ⇒(ψ⇒φ)) [⇒in 2 el 1]
■
エーリル
「はやい」
さトぅー
「ただし、⇒in elを推論規則として追加するなら、証明の定義を変更しないといけなくなる」
エーリル
「え、なんで？」
さトぅー
「確かめてみる？」
■例3(間違った証明)
{} |- φ
proof
1 φ [ax]
2 (φ⇒φ) [⇒in 1 el 1]
3 φ [⇒el 1,2]
■
さトぅー
「φはなんでもいいわよね？」
エーリル
「どんな論理式も証明できてる……」
さトぅー
「これは証明にミスがあるからどんな論理式も証明できちゃったわけね。
公理に注意しながらミスを探してみよう」
■例3のなにがミスなのか
{} |- φ
proof
1 φ [ax]
-------------------
さトぅー
「ここでは{φ}が公理」
-------------------
2 (φ⇒φ) [⇒in 1 el 1]
-------------------
さトぅー
「演繹定理でφが除去されて{}が公理になる」
-------------------
3 φ [⇒el 1,2]
-------------------
さトぅー
「1行目の公理は{φ},2行目の公理は{}だから、そこから⇒elで導いたから3行目の公理は{φ}」
■
エーリル
「あ、除去した公理を使っちゃったのね」
さトぅー
「そういうこと。だから証明の定義を除去した公理があとの行に影響しないように変更する」
■公理の除去を含む証明の定義
φ_1,……,φ_Nは論理式の「有限」列で、
(1) Nが1のとき、φ_1が論理的公理または公理Tならφ_1は証明。
(2) Nがn+1のとき、φ_1,……,φ_nが証明で、φ_n+1が論理的公理または公理Tまたはφ_1,……,φ_nの中から"除去された公理からの結論ではない"いくつかを仮定とする推論規則の結論なら証明。
エーリル
「公理が変われば証明できる定理も変わる。
考えてみれば当たり前だった」
天々城
「さっきみたいなミスを減らしたいなら、公理を除去せずに証明終盤ギリギリまで粘って、最後の最後で公理を消していくようにすればいい」
さトぅー
「やっぱり演繹定理はほしいわよね」
天々城
「演繹定理がないと死ぬ」
