テキスト48ページ「(12)存在の除去」について

[kagamiwari]

テキスト48ページの「述語論理の公理系の導出規則」の項の下から2行目にある

これは、(10)と構造的には同じです

という記述に関して，著者の方が書面の編集段階での間違いとおっしゃっているので，紹介します．

https://twitter.com/7shi/status/613149892513402880

初めまして。「理論から学ぶデータベース実践入門」の読書会を開催しています。早速ですが、P.48で⓬について「❿と構造的には同じ」とあり、見比べても分かりませんでした。前件肯定式に似ているとは思ったのですが、こちらは関係ないでしょうか。

https://twitter.com/nippondanji/status/613516117143719937

こんにちは。すみません、これは書面が間違っています。原稿を見ましたが、原稿では8（p.40にあります）となっています。編集の途中で間違った模様です。

導出規則 (8) と導出規則 (12) とがどのように構造的に同じなのか考えてみました．
それぞれの導出規則をテキストから引用します．

(8) ∨の除去 ... P∨Q、P⊃R、Q⊃R から R を導出して良い

(12) 存在の除去 ... ( ∃xP(x) ∧ (P(c)⊃Q) ) ⊃ Q

ここで、c という記号は任意の値を表しています。

P(x) が真になる x の集合を
S[P] = { a[1], a[2], a[3], ..., a[n] }
と仮定すると，
(12) における ∃xP(x) は，
P(a[1]) ∨ P(a[2]) ∨ P(a[3]) ∨ ... ∨ P(a[n])
という選言の命題と等しくなります．
一方 (12) における (P(c)⊃Q) は，
( P(a[1]) ⊃ Q ) ∧ ( P(a[2]) ⊃ Q ) ∧ ( P(a[3]) ⊃ Q ) ∧ ... ∧ ( P(a[n]) ⊃ Q )
という連言の命題と等しくなります．
ここで，n=2とおくと，
( P(a[1]) ∨ P(a[2]) ) ∧ ( P(a[1]) ⊃ Q ) ∧ ( P(a[2]) ⊃ Q ) ⊃ Q
となります．
この命題のP(a[1]) を (8) の P，P(a[2]) を (8) の Q，Q を (8) の R と置き換えれば，
( (P∨Q) ∧ (P⊃R) ∧ (Q⊃R) ) ⊃ R
となります．
つまり，(12) における x が2個だけ存在すると，(8) の形になるということが確認できました．