Up 6.6 等号をもつ述語論理の構成一覧  

　ここで，等号をもつ述語論理

T＝( G, G, U, U)

の構成一覧を示しておく。

  1. 文生成システムG＝(NＶ,TＶ,Ｐ,Ｓ)：

    1. NＶ：
        SEN ： 文生成に関する
        TVR ： 変項生成に関する
        TRM ： 項生成に関する


    2. TＶ＝｛(，)，∧，¬，∨，→，，∀，∃，＝｝

    3. Ｐ：
        SEN → (SEN)∧(SEN)
        SEN → ¬(SEN)
        SEN → (SEN)∨(SEN)
        SEN → (SEN)→(SEN)
        SEN → (SEN)(SEN)
        SEN → (∀(TVR))(SEN)
        SEN → (∃(TVR))(SEN)
        SEN → (TRM)＝(TRM)
        TRM → TVR


  2. U＝(( G,σ, R), D)：

    1. G＝( NＶ, TＶ,Ｐ,SEN)：

      NＶ＝｛SEN，SVR，TVR，TRM，REL，FUN｝

      TＶ＝ TＶ∪｛sen，1，tvr，trm，[，]，↓，nf，＝｝
      Ｐ：
        SEN →(SEN)∧(SEN)
        SEN →¬(SEN)
        SEN → (SVR)

        SEN→(SEN)[(TVR)↓(TRM)]
        SEN→ nf[(TVR)]

        SEN → (TRM)＝(TRM)

        SVR → SVR1
        SVR → sen

        TRM→(TRM)[(TVR)↓(TRM)]
        TRM→ (TVR)
        TRM → TRM1
        TRM → trm

        TVR→ TVR1
        TVR→ tvr


    2. σ：
        SEN → SEN
        TRM → TRM


    3. R(“代入規則”)：

      1. 代入枠が
        SENｓ， TVRｘ， TRMｔ，
        SENｓ， TVRｘ， TRMｔ

        に対する
        {(ｓ,ｓ),(ｘ,ｘ),(ｔ,ｔ),････}

        であるとき，(ｓ[ｘ↓ｔ]) には，ｓの中の自由なｘにｔを直接代入することでｓから得られる記号列（式）を，直接代入する。

      2. 代入枠が
        TRMｓ， TVRｘ， TRMｔ，
        TRMｓ， TVRｘ， TRMｔ

        に対する
        {(ｓ,ｓ),(ｘ,ｘ),(ｔ,ｔ),････}

        であるとき，(ｓ[ｘ↓ｔ]) には，ｓの中のｘにｔを直接代入することでｓから得られる記号列（項）を，直接代入する。

      3. 代入枠が
        TVRｘ， TVRｘ，
        SENnf[ｘ]， SENｓ

        に対する
        {(ｘ,ｘ)，(nf[ｘ],ｓ),････}

        であるとき，(nf[ｘ]) には，
          (i) ｓがｘを自由変項として含まないときは，ｓ自身；
          (ii)ｓがｘを自由変項として含むときは，(∀ｘ)ｓ

        を直接代入する。

      4. 代入枠が
        TVRｘ， TVRｘ

        に対する
        {(ｘ,ｘ),････}

        であるとき，右に↓のないｘには，ｘを直接代入する。

      5. 代入枠が
        TRMｔ， TRMｔ

        に対する
        {(ｔ,ｔ),････}

        であるとき，左に↓のないｔには，ｔを直接代入する。


    4. D(“換言規則”)：
      文変形補助記号は無し。
      文変形規則は，

        (C1) ¬(¬(sen)) ﾌ sen
        (C2) sen∧sen1 → sen1∧sen
        (C3) ¬((¬sen)∧(¬sen1)) ﾌ sen∨sen1
        あるいは，同じこととして，
        sen∧sen1 ﾌ ¬((¬sen)∨(¬sen1))
        (C4) ¬(sen∧(¬sen1)) ﾌ sen⊃sen1
        あるいは，同じこととして，
        sen∧sen1 ﾌ ¬(sen⊃¬sen1)
        (¬sen)∨sen1 ﾌ sen⊃sen1
        sen∨sen1 ﾌ ¬sen⊃sen1
        (C5) (sen⊃sen1)∧(sen1⊃sen)
        ﾌ sensen1
        (C6)¬((∀tvr)(¬sen)) ﾌ (∃tvr)sen
        ¬((∃tvr)(¬sen)) ﾌ (∀tvr)sen
        (E1) (trm＝trm1) → (trm1＝trm)


  3. U＝(( G,σ, R), D)：

    1. G：
      G# の終端記号に
      txt
      を追加し，プロダクションに
      TXT → TXT1
      TXT → txt
      を追加。

    2. D：
      テクスト変形補助記号は無し。
      テクスト変形規則は，文変形規則から導かれるテクスト変形規則の他に，

        (MP) “sen と sen⊃sen1 から sen1 が導かれる"
        (S1)　ε → sen ⊃ (sen1⊃sen)
        (S2)　ε → (sen⊃(sen1⊃sen11)) ⊃ ((sen⊃sen1)⊃(sen⊃sen11))
        (S3)　ε → (¬sen1⊃¬sen)⊃ (sen⊃sen1)
        (Q0) ε → sen⊃sen[tvr↓trm]
        (Q1) ε → (∀(tvr))(sen) ⊃ (sen)[(tvr)↓(trm)]
        ε → sen[tvr↓trm]⊃(∃tvr)sen
        (Q2) ε → (∀(tvr))((nf[tvr])⊃(sen)) ⊃ ((nf[tvr])⊃(∀(tvr))(sen))
        ε → nf[tvr]∧(∃tvr)sen ⊃ (∃tvr)(nf[tvr]∧sen)
        (Q3) ε → nf[tvr]⊃(∀tvr)nf[tvr]
        ε → (∃tvr)nf[tvr] ⊃ nf[tvr]
        (Q4) ε → (sen⊃sen1) ⊃((∀tvr)sen⊃(∀tvr)sen1)
        ε → (sen⊃sen1) ⊃((∃tvr)sen)⊃(∃tvr)sen1))
        (E2) ε → trm＝trm
        (E3) “trm＝trm1 と trm1＝trm2 から trm＝trm2 が導かれる”