Up 2.3.2 “代入”の定式化  

　われわれは，“代入”を
《代入枠に対する一定の規則の適用》
というように，定式化する──この規則を“代入規則”と呼ぶ。“記号列の直接代入”は，これの特殊になる。いま

G＝(NＶ,TＶ,Ｐ,Ｓ)
G＝(NＶ,TＶ,Ｐ,Ｓ)
とする。

　“代入枠”は，NＶの部分で定義され NＶに値をもつ関数各々に対して考えられる──このように身分づけられた関数を，シェマ関数と呼ぶことにする。

　即ち，NＶの部分で定義され NＶに値をもつ関数σに対し，つぎの条件を満たす

{(ｘ1,ｘ1),････,(ｘn,ｘn)}⊂TＶ*×TＶ*
（ｘi は互いに異なる）　

は，σをシェマ関数とする代入枠であると言う：
    各 i＝1,････,n に対し，
    Ｘi∈NＶ,　Ｘi∈NＶ
    で，

    を満たすものが存在する。
　そして，“(シェマ関数σに関する)代入規則”とは，各代入枠 {(ｘ1,ｘ1),････,(ｘn,ｘn)} に対して代入の方法を一つ定める規則のことである。──それは，記号列：

φ＝Ｕ1η1Ｕ2η2････ＵpηpＵp+1
で，条件：
  1. ηj全体は，ｘi全体と一致する
  2. 各Ｕjの中にTＶ＼TＶの要素は現われない
を満たすものに対する代入規則であるが，ｘi に対するｘi の直接代入とは限らない。