Up 6.3.7 簡約記号∃ の導入  

　簡約記号∃ を，つぎの手続きで導入する：

  1. GとU＝(S,D) を，以下のように変更する：
    1. TＶに記号∃ を追加する。
    2. Ｐにつぎの規則を追加する：

        SEN　→　(∃TVR)(SEN)

    3. 上の変更に， S＝( G,σ, R) の変更を対応させる。
    4. Dにつぎの規則を追加する：

        (C6) ¬((∀tvr)(¬sen)) ﾌ (∃tvr)sen

      あるいは同じこととして，
        　　 ¬((∃tvr)(¬sen)) ﾌ (∀tvr)sen

  2. (1)の変更に， U＝( S, D) の変更を対応させる。

    　記号∀に関するテクスト変形規則 (Q1),(Q2) は，記号∃に対してはつぎのようになる(註)：

      (Q1) ε → sen[tvr↓trm]⊃(∃tvr)sen
      (Q2) ε → nf[tvr]∧(∃tvr)sen ⊃(∃tvr)(nf[tvr]∧sen)
      (Q3) ε → (∃tvr)nf[tvr] ⊃ nf[tvr]
      (Q4) ε → (sen⊃sen1) ⊃((∃tvr)sen)⊃(∃tvr)sen1))


（註） (Q1),(Q2),(Q3),(Q4) の → の右辺を，以下のように順次変形する：
(Q1)：
(∀tvr)sen ⊃ sen[tvr↓trm]
¬(sen[tvr↓trm]) ⊃ ¬((∀tvr)sen)
(¬sen)[tvr↓trm]) ⊃ ¬((∀tvr)(¬¬sen))
sen[tvr↓trm]) ⊃ ¬((∀tvr)(¬sen))
sen[tvr↓trm]) ⊃ (∃tvr)sen

(Q2)：
(∀tvr)(nf[tvr]⊃sen) ⊃ (nf[tvr]⊃(∀tvr)sen)
¬(nf[tvr]⊃(∀tvr)sen) ⊃ ¬((∀tvr)(nf[tvr]⊃sen)
nf[tvr]∧(((∀tvr)sen) ⊃ ¬((∀tvr)(¬¬(nf[tvr]⊃sen))
nf[tvr]∧¬((∀tvr)(¬¬sen)) ⊃ ¬((∀tvr)(¬(nf[tvr]∧¬sen)))
nf[tvr]∧¬((∀tvr)(¬sen)) ⊃ ¬((∀tvr)(¬(nf[tvr]∧sen)))
nf[tvr]∧(∃tvr)sen ⊃ (∃tvr)(nf[tvr]∧sen)

(Q3)：
nf[tvr]⊃(∀tvr)nf[tvr]
¬(∀tvr)nf[tvr]⊃¬nf[tvr]
(∃tvr)¬nf[tvr]⊃¬nf[tvr]
(∃tvr)nf[tvr]⊃nf[tvr]

(Q4)：
(sen⊃sen1)⊃((∀tvr)sen⊃(∀tvr)sen1)
(¬sen1⊃¬sen) ⊃(¬(∀tvr)sen1⊃¬(∀tvr)sen)
(¬sen1⊃¬sen) ⊃((∃tvr)¬sen1⊃(∃tvr)¬sen)
(sen⊃sen1) ⊃((∃tvr)sen⊃(∃tvr)sen1)