Up 6.3.5 文変形システム  

　Gの上の文変形システム U＝( S, D) は，以下のようになる：

  1. Gのシェマシステム S＝( G,σ, R) では，

    1. G＝( NＶ, TＶ, Ｐ, SEN) は，
      1. NＶは，命題論理のNＶに
          TVR ：変項シェマ記号の生成に関する
          TRM ：項シェマ記号の生成に関する
        を追加したもの。
      2. TＶは，命題論理のTＶに
          tvr ： 原初変項シェマ記号
          trm ： 原初項シェマ記号
          [，]： 括弧
          ↓ ： 代入記号
          nf
        を追加したもの。
      3. Ｐは，命題論理のＰに，
        式，項の生成(註1)
          SEN→(SEN)[(TVR)↓(TRM)]
          SEN→ nf[(TVR)]
          TRM→(TRM)[(TVR)↓(TRM)]
        変項シェマ記号の生成(註2)
          TRM→ (TVR)
          TVR→ TVR1
          TVR→ tvr
        項シェマ記号の生成(註3)
          TRM → TRM1
          TRM → trm
        を追加したもの。


    2. シェマ関数σは，命題論理のσに
        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)。
      4. 代入枠が TVRｘ， TVRｘに対する
          {(ｘ,ｘ),････}
        であるとき，右に↓のないｘには，ｘを直接代入する。
      5. 代入枠が TRMｔ， TRMｔに対する
          {(ｔ,ｔ),････}
        であるとき，左に↓のないｔには，ｔを直接代入する。


  2. Dは，命題論理のDに同じ。



（註１） これの意味は，次節で明らかになる。

（註２） したがって，
(tvr),(tvr1),(tvr11),････
が，変項シェマ記号の全て。

（註３） したがって，
trm,trm1,trm11,････
が，項シェマ記号の全て。

（註４）‘nf'は,“not free”の‘n',‘f'をとったもの。代入枠 {(ｘ,ｘ)，(nf[ｘ],ｓ),････} の下で nf[ｘ] に代入されるのは，文ｓに対して《ｓが変項ｘを自由変項として含むときは，これを (∀ｘ) で束縛する》という処置を施して得られる文である。この文においてｘは自由変項でない。