●補題10.57について
――もともと私たちが持っている代入記法は、複数の変数に「同時に」代入するという機能を持ち合わせていません。例えば項\(o(x,y)\)の\(x,y\)にそれぞれ\(o_1(x, y),o_2(x,y)\)を代入して\(o(o_1(x,y),o_2(x,y))\)という2変数関数を作ろうと思っても、\[o(x,y)[o_1(x,y)/x][o_2(x,y)/y]\]と書いたのでは、先に代入された\(o_1(x,y)\)の\(y\)にも\(o_2(x,y)\)が代入されて\[o(o_1(x,o_2(x,y)),o_2(x,y))\]となってしまいます。また、逆順に代入すると\[o(o_1(x,y),o_2(o_1(x,y),y))\]となり、結果が異なってきます。しかし、\(x\)に代入する項に\(y\)が自由出現せず、\(y\)に代入する項に\(x\)が自由出現しないならば、代入結果は順序によらなくなります。例えば\(o(x,y)[o_1(x,z)/x][o_2(y,z)/y]\)は\[o(o_1(x,z),o_2(y,z))\]となりますが、逆順に代入しても結果は変わりません。
このように2つの代入が完全に分離独立していれば話は簡単ですが、例えば\(x,y\)にそれぞれ\(o_1(x,y),o_2(y,z)\)を代入する場合はどうでしょうか。つまり、\(x\)に代入する項には\(y\)が自由出現しているものの、\(y\)に代入する項には\(x\)が自由出現していないという、「半独立」的なケースです。\(x\)への代入を先にすると\[o(o_1(x,\underline{o_2(y,z)}),o_2(y,z))\]となる一方、\(y\)への代入を先にすれば\[o(o_1(x,\underline{y}),o_2(y,z))\]となり、やはり結果は異なります。しかし、後者でまず\(y\)への代入を行ったついでに\(o_1(x,y)\)の\(y\)にもあらかじめ\(o_2(y,z)\)を代入しておき、\(o_1(x,o_2(y,z))\)に変えてからこれを\(x\)に代入すれば、最終的な結果は前者と等しくなります。補題10.57は、このことを主張しています。
――教科書の証明では\(\tau'\)が名前または変項の場合しか証明されていませんが、項はそのいずれかであるとは限りません。証明を補ってください。
