Up 6.3.6 推論システム  

　U＝( S, D) は，つぎのようになる。
  1. Sは， S#＝( G#,σ#, R＃) の G#を， G#と命題論理の G#の合併に改めたもの。
  2. Dは，命題論理の Dに，文変形規則から導かれるテクスト変形規則と，

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

    を追加したもの(註)。


（註） (Q1),(Q2) は，所謂“限量子公理(quantifier axiom)"。(Q0),(Q3),(Q4) は，“一般化規則”を排除したために必要となった。