平成１８年度修士論文題目

修飾変数が任意個の可変子をもつ形式言語の基礎理論

学生番号 56031
フリガナホリカワサトシ
氏名堀川智史

論文の要旨

本論文は数理心理学 (参考文献 [1]) の形式言語を一般化する研究を記載したものである。具体的には、可変子が複数個の修飾変数列をもち、その Dom が任意の集合であるような形式言語の研究をした。

可変子とは、ある記号と変数を並べることにより表される記号列のことであり、修飾変数とはその列にでてくる変数のことをいう。例えば、一階述語言語における可変子とは ∀x や ∃y のようなものであり、可変子 ∀x に対する修飾変数とは x のことである。つまり、表題の修飾変数が任意個の可変子を持つ形式言語とは、 ∀xyz や ∃yxy などという形の可変子をもつ形式言語のことである。

このような形式言語の必要性は、高岡洋介氏の研究活動から見出されたものである。高岡氏の研究によれば、修飾変数が複数個ある可変子をもつ形式言語と、可変子の Dom が単元集合ではない形式言語の２種類の形式言語が必要である。そこで、その二つの性質をもつ形式言語を参考文献 [1] の形式言語を拡張して作った。

次に、本論文の目標の説明をする。一般に形式言語の元は認識可能世界 W 上の関数を表現する。それでは逆に W 上のいかなる関数が A の元によって表現されるのだろうか。この問を、新たに作った形式言語において考察ことが本論文の目標である。結論は定理 4.3.1 によって与えられている。その定理によれば、 A の元により表現される W 上の関数とは、認識可能世界 W 上の 2 種類の関数 (射影、定値関数) と、それらからある二つの算法 (不変子から作られる算法と、可変子から作られる算法) の合成によって作られる関数全体である。 (不変子とは可変子でないものをさす。一階述語言語では ∧, ∨ や述語記号 p などである。 )

例えば、一階述語言語におけるその二つの算法とは以下のようなものである。まず、認識可能世界 W は空でない集合 W′ と集合 {0, 1} の直和とし、 (W′)^{n} から i 成分への射影を f_{i}(x_{1}, ..., x_{n})、 (W′)^{n} から W′ の一元 w への定値関数を f_{w}(x_{1}, ..., x_{n}) とする。ただし簡単のため x_{1}, ..., x_{n} は相異なるとする。

このとき、 f_{i}, f_{w} に不変子 p(述語記号) から作られる算法を作用させた関数 p(f_{i}, f_{w})(x_{1}, ..., x_{n}) とは、 (W′)^{n} の元 (w_{1}, ..., w_{n}) に p(f_{i}(w_{1}, ..., w_{n}), f_{w}(w_{1}, ..., w_{n})) を対応させるものである。従って、この関数は (W′)^{n} から {0, 1} への関数となる。また、 p(f_{i}(x_{1}, ..., x_{n}), f_{w}(x_{1}, ..., x_{n})) に可変子 ∀x_{n} からできる算法を作用させた関数とは、 (W′)^{n−1} の元 (w_{1}, ..., w_{n−1}) に inf {p(f_{i}, f_{w})(w_{1}, ..., w_{n−1}, u_{n}) | u_{n} ∈ W′} を対応させるものである。従って、この関数は (W′)^{n−1} から {0, 1} への関数となる。

この結果は、参考文献 [1] での結果と異なる。具体的には、必要な算法が三つから二つになっている点である。

なお、論理代数学は文法論、意味論、演繹論に分けられるが、本論文の目標は文法論と意味論だけにかかわる。従って、演繹論にあたることは追究しないことを注意しておく。

最後に各章の簡単な説明をする。第 1 章では、本論文を読むために必要な参考文献 [1] での知識を紹介する。第 2 章では、本論文で必要な概念で、参考文献 [1] には無いもの (基底や拡張された代入) を紹介する。第 3 章では、文法論、意味論にあたる形式言語、意味写像等の定義をおこなう。第 4 章では、本論文の目標である W 上のいかなる関数が A の元によって表現されるのかに答える。

目次

第 1 章序論 3 1.1 基礎概念の紹介 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

第 2 章基底と代入 9 2.1 基底 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2 代入 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

第 3 章論理体系 15 3.1 形式言語 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 3.2 認識可能世界 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 3.3 付値と意味写像 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

3.3.1 定付値と変付値 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.3.2 認識可能世界の V al 乗の T 型代数構造 . . . . . . . . . . . . . . . . . . . . 22 3.3.3 定付値が定める意味写像 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

第 4 章表現関数 27 4.1 表現関数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 4.2 代入値換定理 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 4.3 表現可能関数 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

第1章序論

概略

本論文は数理心理学 (参考文献 [1]) の形式言語を一般化する研究を記載したものである。具体的には、可変子が複数個の修飾変数列をもち、その Dom が任意の集合であるような形式言語の研究をした。

可変子とは、ある記号と変数を並べることにより表される記号列のことであり、修飾変数とはその列にでてくる変数のことをいう。例えば、一階述語言語における可変子とは ∀x や ∃y のようなものであり、可変子 ∀x に対する修飾変数とは x のことである。つまり、表題の修飾変数が任意個の可変子を持つ形式言語とは、 ∀xyz や ∃yxy などという形の可変子をもつ形式言語のことである。

このような形式言語の必要性は、高岡洋介氏の研究活動から見出されたものである。高岡氏の研究によれば、修飾変数が複数個ある可変子をもつ形式言語と、可変子の Dom が単元集合ではない形式言語の２種類の形式言語が必要である。そこで、その二つの性質をもつ形式言語を参考文献 [1] の形式言語を拡張して作った。

次に、本論文の目標の説明をする。一般に形式言語の元は認識可能世界 W 上の関数を表現する。それでは逆に W 上のいかなる関数が A の元によって表現されるのだろうか。この問を、新たに作った形式言語において考察ことが本論文の目標である。結論は

定理 4.3.1

[P F^{Φ}] = T F^{Φ}

によって与えられている。ただし、 P F^{Φ} は射影と定値関数全体の集合で、 [P F^{Φ}] は P F^{Φ} と、その元にある二つの算法を何回か用いてできる関数全体の集合、 T F^{Φ} は A の元によって表現される関数全体 (正確に言うと Φ によって表現される関数) の集合である。

従って、 P F^{Φ} の元と P F^{Φ} の元に二つの算法を何回か用いてできる関数のみが、 A の元によって表現されるということがわかる。

なお、論理代数学は文法論、意味論、演繹論に分けられるが、本論文の目標は文法論と意味論だけにかかわる。従って、演繹論にあたることは追究しないことを注意しておく。

また、本論文における独自の概念として基底というものがある。これは、重複を許したある列からある規則によって相異なるように取り出された列のことである。この概念は、可変子が複数個の修飾変数列をもつ形式言語の研究をしていく仮定で必要になったものである。可変子の修飾変数列を複数個とすることに伴い、 A の元によって表現される関数の自由変数列の重複を許したほうがいいということがわかった。しかし、そうすると関数の値が一意に定まらなくなる。そこで、関数の値を決める変数を定める必要性が見出され、基底という概念を作った。また基底の概念は代入の拡張の定義にも用いている。

なお、他の概念は参考文献 [1] の概念を拡張して作ったものである。

最後に各章の簡単な説明をする。第 1 章では、本論文を読むために必要な参考文献 [1] での知識を紹介する。第 2 章では、本論文で必要な概念で、参考文献 [1] には無いもの (基底や拡張された代入) を紹介する。第 3 章では、文法論、意味論にあたる形式言語、意味写像等の定義をおこなう。第 4 章では、本論文の目標である W 上のいかなる関数が A の元によって表現されるのかに答える。

謝辞修士 2 年間を通じてご指導いただき、本論文の作成に多くの助言を与えてくださった五味健作先生に深く感謝いたします。また、協力していただいたゼミの皆さんに感謝いたします。中でも、高岡洋介さんには有益なご意見をたくさんいただきました。

1.1 基礎概念の紹介

この節では基礎概念の紹介を行う。この概念は参考文献 [1] に記載されているものである。従って、定理、命題等の証明は記載しない。詳しくは、参考文献 [1] を参照していただきたい。

参考文献 [1] では、集合 A, B に対して、 A から B への写像全体を A → B で表す。これに伴い f が A から B への写像であることを f ∈ A → B と表す。また、 A → B について以下が成立する。

∅ → B = {∅}  A ≠ ∅ なら A → ∅ = ∅  (空集合律)

集合 A に対して、 ⋃_{n≥0} A^{n} を A^{∗} で表し、 ⋃_{n≥1} A^{n} を A^{+} で表す。また、 A^{∗} と A^{+} とを、列を「繋げる」という算法に関して乗法的な半群とみなす。

集合 A の直積 A^{n} の部分集合 D から A への写像 α を A 上の算法とよび (n = 1, 2, ...)。 D ≠ ∅ のとき n を α の項数という。 D = ∅ のとき α を空算法という。また、 A の部分集合 B が、

α(B^{n} ∩ D) ⊆ B

をみたすとき、 α は B を閉じ込めるという。このとき、 α の Dom を B^{n} に制限したものは、 B 上の算法とみなせる。これを α の制限という。また、算法が複数ある場合は、 α_{λ} のように添え字 λ で区別し、その項数を n_{λ} で表す。このとき、添え字の集合を Λ とおき、これを算法記号系といい、集合 A とその上の算法族 (α_{λ})_{λ∈Λ} の組 (A, (α_{λ})_{λ∈Λ}) を代数系という。そして、 (α_{λ})_{λ∈Λ} を代数構造という。また、二つの代数系 A, B が、共通の算法記号系 Λ をもち、任意の λ ∈ Λ に対応する A, B の算法が共通の項数をもつとき、 A と B は同類の代数系であるという。

代数系 (A, (α_{λ})_{λ∈Λ}) に対して、算法記号系 Λ をその部分集合 M に制限すれば、代数系 (A, (α_{μ})_{μ∈M}) ができる。これを元の代数系の算部分系とよび A_{M} で表す。

A の部分集合 B が任意の α_{λ} に対して α_{λ} は B を閉じ込めるとき、任意の α_{λ} に対して α_{λ} の制限の族を (β_{λ})_{λ∈Λ} とし、 (B, (β_{λ})_{λ∈Λ}) を A の台部分系という。さらに、 A の B を含む最小の台部分系を [B] で表し、これを算包という。 A の任意の集合 S に対して、 A の部分集合 S_{n} (n = 0, 1, ...) を次のように帰納的に定め、 S_{n} を S の n 圏とよび、 S_{0}, S_{1}, S_{2}, ... を S の圏列と呼ぶ。まず、 S_{0} = S と定め、 n ≥ 1 であって、 S_{0}, ..., S_{n−1} が定められたとき、 S_{n} を集合

{α_{λ}(a_{1}, ..., a_{n_{λ}}) | λ ∈ Λ, (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ}, a_{i} ∈ S_{l_{i}} (i = 1, ..., n_{λ}), n = ∑_{i=1}^{n_{λ}} l_{i} + 1}

と定める。このとき、 [S] = ⋃_{n≥0} S_{n} が成り立つ。

以下、 (A, (α_{λ})_{λ∈Λ}), (B, (β_{λ})_{λ∈Λ}) を同類の代数系とする。このとき、以下の二条件をみたす写像 σ ∈ A → B のことを準写という。

1. (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ} ならば、 (σa_{1}, ..., σa_{n_{λ}}) ∈ Dom β_{λ} であって、

σ(α_{λ}(a_{1}, ..., a_{n_{λ}})) = β_{λ}(σa_{1}, ..., σa_{n_{λ}})

が成り立つ。

2. (a_{1}, ..., a_{n_{λ}}) ∈ A^{n_{λ}} で (σa_{1}, ..., σa_{n_{λ}}) ∈ Dom β_{λ} ならば、 (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ} が成り立つ。

そして、 A, B, σ の三つ組を型付代数系という。

また、この型付代数系に対して、 A を台、 B を型代数系、 σ を型写像という。さらに、 a ∈ A に対して、 σa を a の型といい、 b ∈ B に対して、 b の逆像 σ^{−1}b の元を b 型という。他方、 A の部分集合 C と B の部分集合 D に対して、 C ∩ σ^{−1}(D) を C の D 部分といい、 C_{D} で表す。特に、 D = {d} のときは、 C_{D} を単に C_{d} と書く。

命題 1.1.1 (A, B, σ) を型付代数系とし、 A の算法記号系の任意の部分集合を M とする。このとき、 (A_{M}, B_{M}, σ) は型付代数系である。

同じ型代数系をもつ型付代数系を互いに同型であるという。そして、互いに同型の型付代数系 (A, T, σ), (B, T, τ) に対して、 a ∈ A と b ∈ B の型が等しいとき a, b は同型であるという。また、 A の部分集合 S と写像 f ∈ S → B に対して、 f が S から B への保型写像であるとは、 τf = σ|_{S} をみたすことをいう。そして、 A から B への保型写像で準写のものを保型準写という。型付代数系 (A, T, σ) と、 A の部分集合 S が以下二条件をみたすとする。

1. A = [S]

2. (A′, T, σ′) が型付代数系であって、 φ ∈ S → A′ が保型写像であれば、 φ は保型準写 f ∈ A → A′ に拡張される。

このとき、四つ組み (A, T, σ, S) を普遍型付代数系といい、 S の元を素元という。

定理 1.1.1 S を集合とし、 T を代数系、 τ ∈ S → T とする。このとき、普遍型付代数系 (A, T, σ, S) で、 σ|_{S} = τ なるものが存在する。こういう普遍型付代数系は次の意味で一意的に定まる。すなわち、普遍型付台数系 (A′, T′, σ′, S) も σ′|_{S} = τ を満たせば、保型同写 f ∈ A → A′ で、 f|_{S} = id_{S} なるものが唯一存在する。

つまり、 S, T, τ を定めれば普遍型付代数系ができるということである。代数系 (A, (α_{λ})_{λ∈Λ}) と A の部分集合 S に対して、以下の二条件をみたすとき、 (A, S) を有基代数系という。

1. A は S の n 圏 S_{n} (n = 0, 1, 2, ...) の直和である。

2. n = 1, 2, ... に対して、 S_{n} の元 a を S_{n} の定義に沿って

a = α_{λ}(a_{1}, ..., a_{n_{λ}}) (λ ∈ Λ, a_{i} ∈ S_{l_{i}}, n = ∑_{i=1}^{n_{λ}} l_{i} + 1)

と表すときの λ, a_{i}, l_{i} は a に対して一意に定まる。このとき、 A の任意の元 a に対して、 a ∈ S_{n} なる非負整数 n が唯一あるから、この n を a の S に関する階数とよび rk a で表す。また、型付代数系 (A, T, σ) と、 A の部分集合 S に対して、 (A, T, σ, S) が普遍型付代数系であることと、 (A, S) が有基代数系であることは同値であることが知られている。つまり、普遍型付代数系 (A, T, σ, S) に対して、 rk a (a ∈ A) を定義することができる。

型付代数系 (A, T, σ) と空でない集合 V に対して、同型の型付代数系 (⋃_{t∈T} (V → A_{t}), T, τ) を定義する。簡単のため B = ⋃_{t∈T} (V → A_{t}) とする。また、 A, T の代数構造を (α_{λ})_{λ∈Λ}, (t_{λ})_{λ∈Λ} とする。まず、 τ は b ∈ V → A_{t}, (t ∈ T) に対して、

τb = t

とする。次に、 ⋃_{t∈T} (V → A_{t}) の代数構造 (β_{λ})_{λ∈Λ} を定義する。

Dom β_{λ} = {(b_{1}, ..., b_{n_{λ}}) ∈ B^{n_{λ}} | (τb_{1}, ..., τb_{n_{λ}}) ∈ Dom t_{λ}}

とし、 β_{λ}(b_{1}, ..., b_{n_{λ}}) ∈ B を

(β_{λ}(b_{1}, ..., b_{n_{λ}}))v = α_{λ}(b_{1}v, ..., b_{n_{λ}}v)

とする。この定義により、 (⋃_{t∈T} (V → A_{t}), T, τ) が (A, T, σ) と同型の型付代数系であることが知られている。この型付代数系を巾代数系といい、 A^{V} で表す。また、任意の v ∈ V に対して、 b ∈ ⋃_{t∈T} (V → A_{t}) に、 bv ∈ A を対応させる写像を v の定める射影という。この射影は A^{V} から A への保型準写であることがわかっている。

(A, S) を有基代数系とし (α_{λ})_{λ∈Λ} を A の代数構造とする。そして、 n_{λ} を α_{λ} の項数とする。このとき、 A の二元 a, b に対して、 a = α_{λ}(..., b, ...) なる λ があるとき、 b は a に直接現れるといい、このことを b ≺ a で表す。また、 b ≺ a あるいは b = a であることを b ⪯ a で表す。そして、 A の元の列 b_{0}, ..., b_{n} (n ≥ 0) で

a = b_{0} ⪰ b_{1} ⪰ … ⪰ b_{n} = b

なる条件をみたすものが存在するとき b は a に現れるといいこれを b\underline{≺≺}a で表す。さらに、 b_{0}, ..., b_{n} を a への b の現れという。また、 A の元 a と部分集合 B に対し、 B の部分集合 B^{a} を次のように定義する。

B^{a} = \{b ∈ B | b\underline{≺≺}a\}

A の元 a と Λ の元 λ が (Im α_{λ})^{a} ≠ ∅ をみたすとき λ は a に算法記号として現れると呼ぶ。また、 A の元 a と Λ の部分集合 M に対して、 M^{a} を次のように定義する。

M^{a} = {μ ∈ M | (Im α_{μ})^{a} ≠ ∅}

定理 1.1.2 すべての a ∈ A に対して、 S^{a} は有限集合である。

定理 1.1.3 すべての a ∈ A に対して、 ♯(Λ^{a}) ≤ rk a が成立する。

以下、 A の算法記号系 Λ は、 S とある集合 Γ 上の普遍半群 (S ⨿ Γ)^{+} = ⋃_{n≥1}(S ⨿ Γ)^{n} に含まれるとする。半群 (S ⨿ Γ)^{+} において λ ∈ Λ に現れる S の元全体を S^{λ} によって表す。さらに、 Λ の部分集合 M に対して、 S^{M} = ⋃_{λ∈M} S^{λ} とする。

a ∈ A と s ∈ S に対して、 a への s の現れ s_{0}, ..., s_{n} が s ∈ S^{λ} なる任意の λ ∈ Λ に対して、 {s_{0}, ..., s_{n}} ∩ Im α_{λ} = ∅ をみたすとき、この現れは自由であるという。また、 a への s の自由な現れがあるとき、 s は a に自由に現れるといい、このことを s ≪ a で表す。そして、 a ∈ A, R ⊆ S のとき、 s ≪ a なる s ∈ R の全体を R_{F}^{a} であらわし、 B ⊆ A のとき、 R_{F}^{B} = ⋃_{a∈B} R_{F}^{a} と定める。

さらに、 a ∈ A, s ∈ S, B ⊆ A に対して、 a への s の現れ s_{0}, ..., s_{n} がB から自由であるとは、 S_{F}^{B} ∩ S^{λ} ≠ ∅ なる任意の λ ∈ Λ に対して、 {s_{0}, ..., s_{n}} ∩ Im α_{λ} = ∅ をみたすことをいう。また、 s は a に B から自由に現れるとは、 a への B から自由な s の現れが存在することをいい、このことを、 a ≪_{B} s で表す。そして、 a において s は B から自由であるとは、 a への s の自由な現れがどれも B から自由であることをいう。また、 a ∈ A, B ⊆ A に対して、 S_{F,B}^{a} = {s ∈ S | s ≪_{B} a} と定義する。最後に、 B が単元集合 {b} のときは、上の定義の B の部分を単に b と表記する。

定理 1.1.4 任意の s ∈ S に対して、 S_{F}^{s} = {s} が成立し、任意の B ⊆ A に対して、 S_{F,B}^{s} = {s} が成立する。

定理 1.1.5 a = α_{λ}(a_{1}, ..., a_{n_{λ}}) ∈ A, B ⊆ A のとき、次の等式が成立する。

S_{F,B}^{a} = \{ \begin{matrix}⋃_{k=1}^{n_{λ}} S_{F,B}^{a_{k}} & (if S_{F}^{B} ∩ S^{λ} = ∅) \\ ∅ & (if S_{F}^{B} ∩ S^{λ} ≠ ∅) \end{matrix}

定理 1.1.6 a = α_{λ}(a_{1}, ..., a_{n_{λ}}) ∈ A に対して、 S_{F}^{a} = ⋃_{k=1}^{n_{λ}} S_{F}^{a_{k}} − S^{λ} = S_{F}^{{a_{1},...,a_{n_{λ}} }} − S^{λ} が成立する。

定理 1.1.7 a ∈ A, s ∈ S, B ⊆ A であって次の三条件のいずれかが成り立てば、 a において s は B から自由である。

1. s ≪̸ a  2. a ∈ A  3. B = {s}

定理 1.1.8 a = α_{λ}(a_{1}, ..., a_{n_{λ}}) ∈ A, s ∈ S, B ⊆ A とするとき、 a において s は B から自由であるためには、 s ≪̸ a であるか、次の二条件が成立することが必要十分である。

\{ \begin{matrix}1. & 各 a_{k} において s は B から自由である (k = 1, 2, ..., n_{λ}) \\ 2. & S_{F}^{B} ∩ S^{λ} = ∅ \end{matrix}

系 1 a = α_{λ}(a_{1}, ..., a_{n_{λ}}) ∈ A, s ∈ S − S^{λ}, B ⊆ A であって a において s は B から自由であれば、 a_{k} において s は B から自由である (k = 1, 2, ..., n_{λ})。

定理 1.1.9 a ∈ A, B ⊆ A であって、 S_{F}^{B} ∩ S^{Λ^{a}} = ∅ が成り立てば、 a において任意の s ∈ S は B から自由である。

以下この節を通じて (A, T, σ, S) は (α_{λ})_{λ∈Λ} を代数構造とする普遍型付代数系とし、 Λ は S とある集合 Γ によって定まる普遍半群 (Γ ⨿ S)^{+} = ⋃_{n≥1}(Γ ⨿ S)^{n} に含まれるとする。このとき、代入を定義する。 s_{1}, ..., s_{n} を S の相̇異̇な̇る̇元の列、 c_{i} を s_{i} と同じ型の A の元 (i = 1, 2, ..., n) とし、 a ∈ A

に対して、 a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) ∈ A を n と rk a に関する帰納法で定義する。

n = 0

このときは恒等写像とする。つまり、 a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) = a とする。

n > 0 とする。 rk a = 0

a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) = \{ \begin{matrix}c_{i} & (if a = s_{i}のとき (i ∈ 1, 2, ..., n)) \\ a & (if a ∉ \{s_{1}, ..., s_{n}\}) \end{matrix}

rk a > 0 (a = α_{λ}(a_{1}, ..., a_{n_{λ}})) {s_{j_{1}}, ..., s_{j_{k}}} = {s_{1}, ..., s_{n}} − S^{λ} , j_{1} < ... < j_{k} なる番号 j_{1}, ..., j_{k} がある (0 ≤ k ≤ n)。このとき、

a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) = α_{λ}(a_{1}(\frac{s_{j_{1}}, ..., s_{j_{k}}}{c_{j_{1}}, ..., c_{j_{k}}} ), ..., a_{n_{λ}}(\frac{s_{j_{1}}, ..., s_{j_{k}}}{c_{j_{1}}, ..., c_{j_{k}}} ))

と定義する。

定理 1.1.10 s_{1}, ..., s_{n} を S の相̇異̇な̇る̇元の列、 c_{i} を s_{i} と同じ型の A の元 (i = 1, 2, ..., n) とし、 a ∈ A に対して、 s_{i} が a ∈ A に自由に現れなければ、次の式が成り立つ。

a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) = a(\frac{s_{1}, ..., s_{i−1}, s_{i+1}, ..., s_{n}}{c_{1}, ..., c_{i−1}, c_{i+1}, ..., c_{n}} )

定理 1.1.11 s_{1}, ..., s_{n} を S の相̇異̇な̇る̇元の列、 c_{i} を s_{i} と同じ型の A の元 (i = 1, 2, ..., n) とし、

a ∈ A に対して、 b = a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) とすると、

S_{F}^{b} ⊆ S_{F}^{{c_{1},...,c_{n}}} ∪ (S_{F}^{a} − {s_{1}, ..., s_{n}})

が成立する。

第2章基底と代入

2.1 基底

この節では基底の定義とその性質を調べる。集合 S に対して、 m ∈ S^{∗} → ℤ_{≥0} を

m(s) = ♯{s_{1}, ..., s_{n}} (s = s_{1}, ..., s_{n} ∈ S^{∗})

と定義する。そして、 s = s_{1}, ..., s_{n} ∈ S^{∗} と m(s) = m に対して、 i_{1}, i_{2}, ..., i_{m} ∈ {1, 2, ..., n} を以下のように帰納的に定義する。 (まず i_{m} を定め、 i_{k+1}, ..., i_{m} が定まったとしたときに i_{k} を定めるという方法で定義する。 )

k = m のとき i_{k} = n
m > k のとき i_{k} = max { u ∈ {1, 2, ..., n} | s_{u} ∉ {s_{i_{k+1}}, s_{i_{k+2}}, ..., s_{i_{m}}}}

注 (m > k のとき、 { u ∈ {1, 2, ..., n} | s_{u} ∉ {s_{i_{k+1}}, ..., s_{i_{m}}}} ≠ ∅ であること。 ) ♯{s_{i_{k+1}}, ..., s_{i_{m}}} = m − k < m = ♯{s_{1}, ..., s_{n}} より、 {s_{1}, ..., s_{n}} − {s_{i_{k+1}}, ..., s_{i_{m}}} ≠ ∅ となる。従って、 { u ∈ {1, 2, ..., n} | s_{u} ∉ {s_{i_{k+1}}, ..., s_{i_{m}}}} ≠ ∅

また、任意の s ∈ S^{∗} に i_{1}, ..., i_{m(s)} を対応させる写像を I とする。つまり、 I ∈ S^{∗} → ℕ^{∗} で

I(s) = i_{1}, ..., i_{m(s)} (s = s_{1}, ..., s_{n} ∈ S^{∗})

と定義する。また、 b ∈ S^{∗} → S^{∗} を、

b(s) = s_{i_{1}}, ..., s_{i_{m}} (s = s_{1}, ..., s_{n} ∈ S^{∗}, m = m(s), i_{1}, ..., i_{m} = I(s))

と定義する。このとき、 b(s) を s の基底といい、 I(s) を s の基底の位置という。

命題 2.1.1 s_{1}, ..., s_{n} を集合 S の元の列、 I(s_{1}, ..., s_{n}) = i_{1}, ..., i_{m} (m = m(s_{1}, ..., s_{n}))、 b(s_{1}, ..., s_{n}) = s_{i_{1}}, ..., s_{i_{m}} とすると以下のことが成立する。

(1) i_{1} < ... < i_{m}

(2) s_{i_{1}}, ..., s_{i_{m}} は相異なる列である。

(3) {s_{1}, ..., s_{n}} = {s_{i_{1}}, ..., s_{i_{m}}}

(4) i ∈ {1, 2, ..., n} に対して、 {i_{1}, ..., i_{m}} ∩ {i, i + 1, ..., n} = {j_{1}, ..., j_{k}} とすると、 {s_{i}, ..., s_{n}} = {s_{j_{1}}, ..., s_{j_{k}}} が成立する。

(5) i ∈ {1, 2, ..., n} に対して以下の二条件は同値である。

1. i ∈ {i_{1}, ..., i_{m}} 2. s_{i} ∉ {s_{i+1}, ..., s_{n}}

(1) の証明 k = 1, 2, ..., m − 1 に対して、 i_{k} < i_{k+1} を示せばよい。 k = m − 1 のときは、 i_{k+1} = i_{m} = n より i_{k} ≤ i_{k+1} となる。また、 i_{k} の定義より、 s_{i_{k}} ≠ s_{i_{k+1}} であるので、 i_{k} ≠ i_{k+1} が成立する。従って i_{k} < i_{k+1} となる。 k = 1, 2, ..., m − 2 のとき、 i_{k} = max { u ∈ {1, 2, ..., n} | s_{u} ∉ {s_{i_{k+1}}, s_{i_{k+2}}, ..., s_{i_{m}}}} より、 s_{i_{k}} ∉ {s_{i_{k+1}}, s_{i_{k+2}}, ..., s_{i_{m}}} となる。従って、 s_{i_{k}} ∉ {s_{i_{k+2}}, s_{i_{k+3}}, ..., s_{i_{m}}} が成立する。また、 i_{k+1} = max { u ∈ {1, 2, ..., n} | s_{u} ∉ {s_{i_{k+2}}, s_{i_{k+3}}, ..., s_{i_{m}}}} より、 i_{k} ≤ i_{k+1} が成立する。そして、 i_{k} の定義より、 s_{i_{k}} ≠ s_{i_{k+1}} であるので、 i_{k} ≠ i_{k+1} となる。従って、 i_{k} < i_{k+1} が成立する。

q.e.d.

(2) の証明 i ∈ {i_{1}, ..., i_{m}}, j ∈ {i_{1}, ..., i_{m}} − {i} とする。 i < j のとき i ∈ {i_{1}, ..., i_{m}} より、 i = i_{k} なる {i_{1}, ..., i_{m}} の元が存在する。このとき、 i_{k} の定義より、 s_{i} = s_{i_{k}} ∉ {s_{i_{k+1}}, s_{i_{k+2}}, ..., s_{i_{m}}} であり、 i_{1} < ..., < i_{m} より j ∈ {i_{k+1}, ..., i_{m}} となる。従って、 s_{i} ≠ s_{j} となる。 i > j のときも同様に示される。

q.e.d.

(3) の証明 {s_{1}, ..., s_{n}} ⊇ {s_{i_{1}}, ..., s_{i_{m}}} であることは自明。また、 ♯{s_{1}, ..., s_{n}} = m(s_{1}, ..., s_{n}) = m であり、 (2) から s_{i_{1}}, ..., s_{i_{m}} は相異なる列なので、 ♯{s_{i_{1}}, ..., s_{i_{m}}} = m となる。従って、 ♯{s_{1}, ..., s_{n}} = ♯{s_{i_{1}}, ..., s_{i_{m}}} より等号が示される。

q.e.d.

(4) の証明 i を {1, 2, ..., n} の元として {i_{1}, ..., i_{m}} ∩ {i, ..., n} = {j_{1}, ..., j_{k}} とする。 {s_{i}, ..., s_{n}} ⊇ {s_{j_{1}}, ..., s_{j_{k}}} であることは {i, ..., n} ⊇ {j_{1}, ..., j_{k}} から自明なので、 {s_{i}, ..., s_{n}} ⊆ {s_{j_{1}}, ..., s_{j_{k}}} を示せばよい。 h ∈ {i, ..., n} に対して、 (3) より、 s_{h} = s_{i′} をみたす i′ ∈ {i_{1}, ..., i_{m}} が存在する。このとき、基底の位置の定義より h ≤ i′ となる。従って、 i′ ∈ {j_{1}, ..., j_{k}} より s_{h} ∈ {s_{j_{1}}, ..., s_{j_{k}}} となる。ゆえに {s_{i}, ..., s_{n}} ⊆ {s_{j_{1}}, ..., s_{j_{k}}} が成立する。従って等号が成立する。

q.e.d.

(5) の証明 ( 1 ⇒ 2 ) i ∈ {i_{1}, ..., i_{m}} とすると i = i_{k} なる i_{k} ∈ {i_{1}, ..., i_{m}} が存在する。また、 (1) より、 i_{1} < ... < i_{m} なので、 {i_{1}, ..., i_{m}} ∩ {i + 1, ..., n} = {i_{k+1}, ..., i_{m}} となる。このとき、基底の位置の定義から s_{i} ∉ {s_{i_{k+1}}, ..., s_{i_{m}}} であり、 (4) から {s_{i_{k+1}}, ..., s_{i_{m}}} = {s_{i+1}, ..., s_{n}} より s_{i} ∉ {s_{i+1}, ..., s_{n}} が成立する。

( 2 ⇒ 1 ) 仮定より s_{i} ∉ {s_{i+1}, ..., s_{n}} であるので、 i = max {u ∈ {1, 2, ..., n} | s_{u} ∉ {s_{i+1}, ..., s_{n}}} となる。また、 {i_{1}, ..., i_{m}}∩{i+1, ..., n} = {j_{1}, ..., j_{k}} とすると、 (1) より、 i_{1} < ... < i_{m} なので、 {j_{1}, ..., j_{k}} = {i_{k}, ..., i_{m}} なる i_{k} ∈ {i_{1}, ..., i_{m}} が存在する。このとき、 (4) から {s_{i_{k}}, ..., s_{i_{m}}} = {s_{i+1}, ..., s_{n}} より i = max {u ∈ {1, 2, ..., n} | s_{u} ∉ {s_{i_{k}}, ..., s_{i_{m}}}} が成立する。従って、 i ∈ {i_{1}, ..., i_{m}} が成立する。

q.e.d.

2.2 代入

この節では、参考文献 [1] の代入の拡張をおこなう。またこの節を通じて (A, T, σ, S) は (α_{λ})_{λ∈Λ} を代数構造とする普遍型付代数系とし、 Λ は S とある集合 Γ によって定まる普遍半群 (Γ ⨿ S)^{+} = ⋃_{n≥1}(Γ ⨿ S)^{n} に含まれるとする。 s_{1}, ..., s_{n} を S の元の列、 I(s_{1}, ..., s_{n}) = i_{1}, ..., i_{m} (m = m(s_{1}, ..., s_{n})) とし、 c_{i} を s_{i} と同じ型の A

の元 (i = 1, 2, ..., n) とする。このとき、 a ∈ A に対して a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) ∈ A を以下のように定義

する。

a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) = a(\frac{s_{i_{1}}, ..., s_{i_{m}}}{c_{i_{1}}, ..., c_{i_{m}}} )

ただし、右辺の (\frac{s_{i_{1}}, ..., s_{i_{m}}}{c_{i_{1}}, ..., c_{i_{m}}} ) は 1.1 節での代入である。

( 命題 2.1.1 より s_{i_{1}}, ..., s_{i_{m}} は相異なるので (\frac{s_{i_{1}}, ..., s_{i_{m}}}{c_{i_{1}}, ..., c_{i_{m}}} ) を定義することができる。 )

定理 2.2.1 a ∈ A , b = a(\frac{s_{1}, ..., s_{n}}{c_{1}, ..., c_{n}} ) で、 I(s_{1}, ..., s_{n}) = i_{1}, ..., i_{m} (m = m(s_{1}, ..., s_{n})) とする。こ

のとき、

S_{F}^{b} ⊆ S_{F}^{{c_{i_{1}} ,...,c_{im} }} ∪ (S_{F}^{a} − {s_{i_{1}}, ..., s_{i_{m}}})

が成立する。

証明

代入の定義より、 b = a(\frac{s_{i_{1}}, ..., s_{i_{m}}}{c_{i_{1}}, ..., c_{i_{m}}} ) であり、命題 2.1.1 より s_{i_{1}}, ..., s_{i_{m}} は相異なる列なので定理

1.1.11 を用いると、

S_{F}^{b} ⊆ S_{F}^{{c_{i_{1}} ,...,c_{im} }} ∪ (S_{F}^{a} − {s_{i_{1}}, ..., s_{i_{m}}})

が成り立つ。

q.e.d.

定理 2.2.2 a_{1}, ..., a_{p} を A の元の列、 B ⊆ A、 C を A の有限部分集合とし、 s_{1}, ..., s_{n} を S の元の列で I(s_{1}, ..., s_{n}) = i_{1}, ..., i_{m} (m = m(s_{1}, ..., s_{n})) とする。そして、

\{ \begin{matrix}• & S_{F}^{b} ∩ S^{Λ} ⊆ \{s_{1}, ..., s_{n}\} (∀ b ∈ B) \\ • & t ∈ T に対して、 \{s_{1}, ..., s_{n}\}_{t} ∩ S^{Λ} ≠ ∅ ならばS_{t} ∩ S^{Λ}は可算個の元を含む \end{matrix}

を仮定すると、以下のことが成立する。 ∃ r_{1}, ..., r_{n} ∈ S^{Λ} ∪ ({s_{1}, ..., s_{n}} − S^{Λ}) s.t. 以下の七条件をみたす。

1. r_{i}は s_{i} と同型 (i = 1, 2, ..., n)

2. a_{k} において任意の s ∈ S は b(\frac{s_{1}, ..., s_{n}}{r_{1}, ..., r_{n}} ) から自由 (k = 1, 2, ..., p b ∈ B)

3. I(r_{1}, ..., r_{n}) = i1^{′}, ..., im′^{′} (m′ = m(r_{1}, ..., r_{n})) とすれば、 {i_{1}, ..., i_{m}} ⊆ {i1^{′}, ..., im′^{′} }

4. s_{i} ∈ S^{Λ} なる i に対して、 r_{i} ∈ S^{Λ}

5. ({r_{1}, ..., r_{n}} ∩ S^{Λ}) ∩ C = ∅

6. s_{i}, s_{i′} ∈ S^{Λ} なる i, i′ に対して、 i ≠ i′ ならば、 r_{i} ≠ r_{i′}

7. s_{i} ∈ S^{Λ} なる i に対して、 a_{k} において任意の s ∈ S は r_{i} から自由 (k = 1, 2, ..., p)

証明 (�) r_{1}, ..., r_{n} を決める

H = { k ∈ {1, 2, ..., n} | s_{k} ∈ S^{Λ}} とし、 H = {h_{1}, ..., h_{u}} とおく。 h_{l} ∈ H に対して、 rh_{l}^{′} を帰納

的に定義する。

l = 1 のとき、 rh_{1}^{′} ∈ (S_{σs_{h_{1}}} ∩ S^{Λ}) − (S^{∪_{k=1}^{p}Λ^{a_{k}}} ∪ C)
l > 1 のとき、 rh_{l}^{′} ∈ (S_{σs_{h_{l}}} ∩ S^{Λ}) − (S^{∪_{k=1}^{p}Λ^{a_{k}}} ∪ C ∪ {rh_{1}^{′}, ..., rh_{l−1}^{′}})

注 (rh_{1}^{′}, ..., rh_{u}^{′} が存在すること)

これを示すためには、 h_{l} ∈ H に対して、 S_{σs_{h_{l}}} ∩ S^{Λ} が可算個の元を含むことと、 (S^{∪_{k=1}^{p}Λ^{a_{k}}} ∪ C ∪ {rh_{1}^{′}, ..., rh_{l−1}^{′}}) が有限集合であることを示せばよい。なぜならば、それらが成り立てば、 (S_{σs_{h_{l}}} ∩

S^{Λ}) − (S^{∪_{k=1}^{p}Λ^{a_{k}}} ∪ C ∪ {rh_{1}^{′}, ..., rh_{l−1}^{′}}) が可算個の元を含むことがわかり、上のような rh_{1}^{′}, ..., rh_{u}^{′}

が存在することがわかるからである。 (注： l = 1 のときは、 {rh_{1}^{′}, ..., rh_{l−1}^{′}} = ∅ とする。 )

• S_{σs_{h_{l}}} ∩ S^{Λ} が可算個の元を含むこと h_{l} ∈ H は s_{h_{l}} ∈ S^{Λ} であるので s_{h_{l}} ∈ {s_{1}, ..., s_{n}}_{σs_{h_{l}}} ∩S^{Λ} となる。従って、 {s_{1}, ..., s_{n}}_{σs_{h_{l}}} ∩S^{Λ} ≠ ∅ より仮定から S_{σs_{h_{l}}} ∩ S^{Λ} は可算個の元を含む。

• (S^{∪_{k=1}^{p}Λ^{a_{k}}} ∪ C ∪ {rh_{1}^{′}, ..., rh_{l−1}^{′}}) が有限集合であること

定理 1.1.3 より ♯(Λ^{a_{k}}) ≤ rk a_{k} で p は有限より、 ⋃_{k=1}^{p} Λ^{a_{k}} は有限集合である。さらに、 μ ∈ ⋃_{k=1}^{p} Λ^{a_{k}} に対して、 μ は有限列より S^{μ} は有限集合となる。従って、 S^{∪_{k=1}^{p}Λ^{a_{k}}} は有限集合。そして、 H は有限集

合より、 {rh_{1}^{′}, ..., rh_{l−1}^{′}} も有限集合で、 C も仮定より有限集合なので、 (S^{∪_{k=1}^{p}Λ^{a_{k}}} ∪C∪{rh_{1}^{′}, ..., rh_{l−1}^{′}})

は有限集合。従って、 rh_{1}^{′}, ..., rh_{u}^{′} が上のように取れる。

このとき r_{1}, ..., r_{n} を以下のように定義する。 i = 1, 2, ..., n に対して

r_{i} = \{ \begin{matrix}ri^{′} & (if i ∈ H) \\ s_{i} & (if i ∉ H) \end{matrix}

(�) r_{1}, ..., r_{n} ∈ S^{Λ} ∪ ({s_{1}, ..., s_{n}} − S^{Λ}) であることを示す。

• i ∈ H のとき

r_{i} = ri^{′} で、 rh_{1}^{′}, ..., rh_{u}^{′} のとり方より、 ri^{′} ∈ S^{Λ} となる。従って、 r_{i} ∈ S^{Λ} ∪ ({s_{1}, ..., s_{n}} − S^{Λ})

• i ∉ H のとき i は H に属さないので、 s_{i} ∉ S^{Λ} となる。また、 r_{i} = s_{i} ∈ {s_{1}, ..., s_{n}} より、 r_{i} ∈ {s_{1}, ..., s_{n}} − S^{Λ} となる。従って、 r_{i} ∈ S^{Λ} ∪ ({s_{1}, ..., s_{n}} − S^{Λ})

(�) 1 が成立すること r_{1}, ..., r_{n} の決め方より明らか

(�) 2 が成立すること

b を B の元として、 d = b(\frac{s_{1}, ..., s_{n}}{r_{1}, ..., r_{n}} ) と定める。もし、 k = 1, 2, ..., p に対して S_{F}^{d} ∩ S^{Λ^{a_{k}}} = ∅ が

示せれば、定理 1.1.9 より a_{k} において任意の s ∈ S は d から自由であることがわかる。

今、 I(s_{1}, ..., s_{n}) = i_{1}, ..., i_{m} より、

S_{F}^{d} ∩ S^{Λ^{a_{k}}}

⊆ (S_{F}^{{r_{i_{1}} ,...,r_{im} }} ∪ (S_{F}^{b} − {s_{i_{1}}, ..., s_{i_{m}}}))∩S^{Λ^{a_{k}}}  (∵定理 2.2.1)
= ({r_{i_{1}}, ..., r_{i_{m}}} ∪ (S_{F}^{b} − {s_{i_{1}}, ..., s_{i_{m}}}))∩S^{Λ^{a_{k}}}  (∵定理 1.1.4 )
= ({r_{i_{1}}, ..., r_{i_{m}}} ∩ S^{Λ^{a_{k}}}) ∪ (S_{F}^{b} ∩ S^{Λ^{a_{k}}} − {s_{i_{1}}, ..., s_{i_{m}}})
⊆ ({r_{1}, ..., r_{n}} ∩ S^{Λ^{a_{k}}}) ∪ (S_{F}^{b} ∩ S^{Λ^{a_{k}}} − {s_{i_{1}}, ..., s_{i_{m}}}) (∵ {r_{i_{1}}, ..., r_{i_{m}}} ⊆ {r_{1}, ..., r_{n}})

となる。従って、 S_{F}^{d} ∩S^{Λ^{a_{k}}} = ∅ を示すには、 ({r_{1}, ..., r_{n}}∩S^{Λ^{a_{k}}}) = ∅ と (S_{F}^{b} ∩S^{Λ^{a_{k}}} −{s_{i_{1}}, ..., s_{i_{m}}}) = ∅ を示せばよい。

• ({r_{1}, ..., r_{n}} ∩ S^{Λ^{a_{k}}}) = ∅ であること r_{i} ∈ {r_{1}, ..., r_{n}} とする。

i ∈ H ならば、 rh_{1}^{′}, ..., rh_{u}^{′} の決め方より r_{i} = ri^{′} ∉ S^{∪_{k=1}^{p}Λ^{a_{k}}} で、 S^{Λ^{a_{k}}} ⊆ S^{∪_{k=1}^{p}Λ^{a_{k}}} なので、 r_{i} ∉ S^{Λ^{a_{k}}}

i ∉ H ならば r_{i} = s_{i} ∉ S^{Λ} より、 r_{i} ∉ S^{Λ^{a_{k}}} 従って、 {r_{1}, ..., r_{n}} ∩ S^{Λ^{a_{k}}} = ∅

• (S_{F}^{b} ∩ S^{Λ^{a_{k}}} − {s_{i_{1}}, ..., s_{i_{m}}}) = ∅ であること

S_{F}^{b} ∩ S^{Λ^{a_{k}}} ⊆ S_{F}^{b} ∩ S^{Λ}  (∵Λ^{a_{k}} ⊆ Λ)
⊆ {s_{1}, ..., s_{n}} (∵仮定)
= {s_{i_{1}}, ..., s_{i_{m}}} (∵命題 2.1.1)

より、 S_{F}^{b} ∩ S^{Λ^{a_{k}}} ⊆ {s_{i_{1}}, ..., s_{i_{m}}} となる。従って、 S_{F}^{b} ∩ S^{Λ^{a_{k}}} − {s_{i_{1}}, ..., s_{i_{m}}} = ∅ が成立する。

(�) 3 が成立すること 3 が成立することを示すためには、 i ∈ {i_{1}, ..., i_{m}} に対して、 r_{i} ≠ r_{k} (∀ k > i) を示せばよい。な

ぜならば、そうであれば r_{i} ∉ {r_{i+1}, ..., r_{n}} となり命題 2.1.1 より、 i ∈ {i1^{′}, ..., im′^{′} } が成立するから

である。

• i ∈ H のとき

k ∈ H ならば、 r_{k} = rk^{′} , r_{i} = ri^{′} より、 rh_{1}^{′}, ..., rh_{u}^{′} の決め方から、 r_{i} ≠ r_{k}

k ∉ H ならば、 r_{k} = s_{k} ∉ S^{Λ}, r_{i} = ri^{′} ∈ S^{Λ} より、 r_{i} ≠ r_{k}

• i ∉ H のとき

k ∈ H ならば、 r_{k} = rk^{′} ∈ S^{Λ}, r_{i} = s_{i} ∉ S^{Λ} より、 r_{i} ≠ r_{k}

k ∉ H ならば、 r_{k} = s_{k} ,r_{i} = s_{i} であり、 i ∈ {i_{1}, ..., i_{m}} より命題 2.1.1 から s_{i} ∉ {s_{i+1}, ..., s_{n}} なので、 r_{i} ≠ r_{k} 従って、 3 が成立する。

(�) 4 が成立すること i を s_{i} ∈ S^{Λ} をみたすものとすると、 i ∈ H なので、 r_{i} = ri^{′} となる。従って、 ri^{′} のとり方より、 r_{i} ∈ S^{Λ} が成立する。

(�) 5 が成立すること

r_{1}, ..., r_{n} の定義より、 {r_{1}, ..., r_{n}} ∩ S^{Λ} = {rh_{1}^{′}, ..., rh_{u}^{′}} となる。このとき、 rh^{′} ∈ {rh_{1}^{′}, ..., rh_{u}^{′}} に対

して、 rh^{′} のとり方から、 rh^{′} ∉ C より、 ({r_{1}, ..., r_{n}} ∩ S^{Λ}) ∩ C = ∅ が成立する。

(�) 6 が成立すること

i, i′ を s_{i}, s_{i′} ∈ S^{Λ} なるものとすると、 i, i′ ∈ H より r_{i} = ri^{′}, r_{i′} = ri′^{′} となる。このとき、

rh_{1}^{′}, ..., rh_{u}^{′} のとり方より rh_{1}^{′}, ..., rh_{u}^{′} は相異なる列なので、 i ≠ i′ ならば、 r_{i} ≠ r_{i′} が成立する。

(�) 7 が成立すること s_{i} ∈ S^{Λ} なる i と k = 1, 2, ..., p に対して、 S_{F}^{r_{i}} ∩ S^{Λ^{a_{k}}} = ∅ が示せれば、定理 1.1.9 より、 a_{k} において任意の s ∈ S は r_{i} から自由であることがわかる。そこで、これを示す。

S_{F}^{r_{i}} ∩ S^{Λ^{a_{k}}} = {r_{i}} ∩ S^{Λ^{a_{k}}}  (∵ r_{i} ∈ S より、定理 1.1.4 )
= {ri^{′}} ∩ S^{Λ^{a_{k}}}  (∵ i ∈ H よりr_{1}, ..., r_{n}の定義)
= ∅  (∵ ri^{′}のとり方からri^{′} ∉ S^{Λ^{a_{k}}})

従って、 7 が成立する。

q.e.d.

第3章論理体系

3.1 形式言語

この節では文法論すなわち形式言語の定義をする。定理 1.1.1 によれば集合 S と代数系 T そして S から T への写像 τ を定めれば、普遍型付代数系 (A, T, σ, S) で、 σ|_{S} = τ なるものが一意に存在する。このことを用いて形式言語を定義する。ただし、ここでは S にあたるものを P rm で表す。

次の三条件をみたす普遍型付代数系 (A, T, σ, P rm) を形式言語という。

(1) P rm は二つの部分集合 Con と V ar (≠ ∅) によって直和分割されている。

(2) T の算法記号系 Λ は、ある集合 Γ と V ar の直和 Γ ⨿ V ar 上の普遍半群 (Γ ⨿ V ar)^{+} の部分集合である。

(3) 任意の V ar^{λ} ≠ ∅ なる λ ∈ Λ に対して、 λ は単項算法記号である。 (空算法記号も単項算法記号とみなす。 )

(2) によれば λ ∈ Λ は Γ の元と V ar の元の「積」で表される。つまり、 λ = s_{1}, ..., s_{n} (s_{i} ∈ Γ ⨿ V ar (i = 1, 2, ..., n)) と表されている。しかし、このように λ を積の形で表す場合、 Γ の元を記述する必要があるところが少ないので、その必要性がないかぎり Γ に属する部分を省略して、 λ = ...y_{1}...y_{2}......y_{m}... (y_{i} ∈ V ar i = 1, 2, ..., m) と記述する。

Con の元を定数、 V ar の元を変数という。また、 {λ ∈ Λ | V ar^{λ} = ∅} の元を不変子といい、 {λ ∈ Λ | V ar^{λ} ≠ ∅} の元を可変子という。そして、可変子 λ = ...y_{1}...y_{2}......y_{m}... (y_{i} ∈ V ar i = 1, 2, ..., m) に対して、 λ に現れる V ar の元 y_{1}, y_{2}, ..., y_{m} を修飾変数列という。また V ar の部分集合 Qvar を Qvar = {x ∈ V ar | ∃ λ ∈ Λ s.t. x ∈ V ar^{λ}} と定める。不変子全体を Λ′ で表し、 T の算部分系 T_{Λ′} を T′ で表す。そして、 a ∈ A に対して V ar_{F}^{a} を F var^{a} と書くことにする。また、算法記号と算法を同一視する。

なお、演繹論の研究を推し進めていくには、形式言語の定義三条件に加えて条件

(4) 文型と呼ばれる T の特別な元 ϕ が指定されている。

をみたす普遍型付代数系を新たに形式言語と定義しなおさなければならない。 (詳しくは参考文献 [1] を参照していただきたい。 ) 従って、 (1),(2),(3) をみたす普遍型付代数系は『広義の形式言語』と呼ぶべきであるが、概略で書いたとおりこの論文では演繹論まで言及しないので『広義の』を省略する。

例 3.1.1 (一階述語言語) A を次のような形式言語と定義する。まず、素元系 P rm は任意とする。次に型付代数系 T については、台は {ε, ϕ} であり、算法記号系 Λ はブール子 ∧, ∨, ⇒, ⋄ と論理記号 ∀x_{1}...x_{n} (x_{1}, ..., x_{n} ∈ V ar), ∃x_{1}...x_{n} (x_{1}, ..., x_{n} ∈ V ar) があり、さらに、 n 変数関数記号 f と n 変数述語記号 p という名の n 項算法記号の零個以上幾つかからなるものとする (n = 1, 2, ...)。次に作用を定義する。

• ∧, ∨, ⇒ について、

\{ \begin{matrix}Dom ∧ = Dom ∨ = Dom ⇒ = \{ϕ\}^{2} \\ ϕ ∧ ϕ = ϕ ∨ ϕ = ϕ ⇒ ϕ = ϕ \end{matrix}

• ⋄ について、

\{ \begin{matrix}Dom ⋄ = \{ϕ\} \\ ϕ^{⋄} = ϕ \end{matrix}

• ∀x_{1}...x_{n} (x_{1}, ..., x_{n} ∈ V ar), ∃x_{1}...x_{n} (x_{1}, ..., x_{n} ∈ V ar) について、

\{ \begin{matrix}Dom ∀x_{1}...x_{n} = Dom ∃x_{1}...x_{n} = \{ϕ\} \\ ∀x_{1}...x_{n} ϕ = ∃x_{1}...x_{n} ϕ = ϕ \end{matrix}

• n 変数関数記号 f と n 変数述語記号 p について、

\{ \begin{matrix}Dom f = Dom p = \{ε\}^{n} \\ f(ε, ..., ε) = ε \\ p(ε, ..., ε) = ϕ \end{matrix}

とする。 Γ は ∧, ∨, ⇒, ⋄, ∀, ∃, n 変数関数記号 f, n 変数述語記号 p からなるものとする。 τ ∈ P rm → T は τx = ε (x ∈ P rm) とする。

命題 3.1.1 形式言語 (A, T, σ, P rm) に対して以下が成立する。

(1) λ ∈ Λ に対して、 P rm^{λ} = V ar^{λ} が成立する。従って、 λ が不変子ならば P rm^{λ} = ∅ となる。 (2) Qvar = P rm^{Λ}

(3) λ が不変子で a = α_{λ}(a_{1}, ..., a_{n_{λ}}) ならば F var^{a} = ⋃_{k=1}^{n_{λ}} F var^{a_{k}}

(4) λ が可変子で a = λa_{1} ならば F var^{a} ∪ V ar^{λ} ⊇ F var^{a_{1}}

証明

(1) の証明 λ ∈ Λ とする。形式言語の定義より、 λ ∈ (Γ ⨿ V ar)^{+} となる。さらに、 V ar ∩ Con = ∅ より Con^{λ} = ∅ が成立する。従って、 P rm^{λ} = V ar^{λ} ∪ Con^{λ} = V ar^{λ} となる。また、 λ が不変子ならば定義より V ar^{λ} = ∅ なので、 P rm^{λ} = ∅ が成立する。

q.e.d.

(2) の証明 Qvar ⊆ P rm^{Λ} であること x ∈ Qvar とすると定義より x ∈ V ar^{λ} なる λ ∈ Λ が存在する。このとき、 x ∈ V ar^{λ} ⊆ V ar^{Λ} ⊆ P rm^{Λ} より成立。 Qvar ⊇ P rm^{Λ} であること x ∈ P rm^{Λ} とすると定義より x ∈ P rm^{λ} なる λ ∈ Λ が存在する。このとき、 (1) より P rm^{λ} = V ar^{λ} なので ∃ λ ∈ Λ s.t. x ∈ V ar^{λ} となる。従って x ∈ Qvar であることがわかる。

q.e.d.

(3) の証明定理 1.1.6 と λ は不変子であることより、 P rm_{F}^{a} = ⋃_{k=1}^{n_{λ}} P rm_{F}^{a_{k}} となる。このことに注意して以下の式変形で (3) が成立することが示される。

F var^{a} = P rm_{F}^{a} ∩ V ar
= (⋃_{k=1}^{n_{λ}} P rm_{F}^{a_{k}})∩V ar
= ⋃_{k=1}^{n_{λ}}(P rm_{F}^{a_{k}} ∩ V ar)
= ⋃_{k=1}^{n_{λ}} F var^{a_{k}}

q.e.d.

(4) の証明定理 1.1.6 より、 P rm_{F}^{a} = P rm_{F}^{a_{1}} − P rm^{λ} が成立し、 (1) より P rm^{λ} = V ar^{λ} なので P rm_{F}^{a} = P rm_{F}^{a_{1}} − V ar^{λ} となる。このとき、

F var^{a} = P rm_{F}^{a} ∩ V ar
= (P rm_{F}^{a_{1}} − V ar^{λ}) ∩ V ar
= (P rm_{F}^{a_{1}} ∩ (V ar^{λ})^{∘}) ∩ V ar
= (P rm_{F}^{a_{1}} ∩ V ar) ∩ (V ar^{λ})^{∘}
= (F var^{a_{1}}) ∩ (V ar^{λ})^{∘}
= F var^{a_{1}} − V ar^{λ}

より、

\begin{aligned}F var^{a} ∪ V ar^{λ} & = & (F var^{a_{1}} − V ar^{λ}) ∪ V ar^{λ} \\ & ⊇ & F var^{a_{1}} \end{aligned}

が成立する。

q.e.d.

3.2 認識可能世界

ここの節では、形式言語 (A, T, σ, P rm) に対して意味論である認識可能世界を定義する。

次の二条件をみたす代数系 W を (A, T, σ, P rm) にとっての認識可能世界という。

\begin{matrix}(1) & W は T′ 型代数系 \\ (2) & 任意の t ∈ σ(P rm) に対して W_{t} ≠ ∅ をみたす \end{matrix}

例 3.2.1 A の算法記号系 Λ を Λ′ に制限した算部分系 A_{Λ′} は (A, T, σ, P rm) にとっての認識可能世界である。

A_{Λ′} が T′ 型代数系であることは命題 1.1.1 からわかる。また、任意の t ∈ σ(P rm) に対して、 t = σx なる P rm の元 x が存在し、 x ∈ A ∩ σ^{−1}(t) より A_{t} ≠ ∅ となるので、認識可能世界の定義をみたす。例 3.2.2 (A, T, σ, P rm) が一階述語言語のとき、 W を空でない集合 W′ と 𝕋 = {0, 1} の直和とし、 ρ ∈ W → T を以下のように定める。 w ∈ W に対して、

ρw = \{ \begin{matrix}ε & (if w ∈ W′) \\ ϕ & (if w ∈ 𝕋) \end{matrix}

と定義する。つまり、 W = W_{ε} ⨿ W_{ϕ} と定める。そして、算法記号系 Λ はブール子 ∧, ∨, ⇒, ⋄ と n 変数関数記号 f と n 変数述語記号 p という名の n 項算法記号の零個以上幾つかからなるものとする (n = 1, 2, ...)。次に作用を定義する。論理記号について、まず Dom は

Dom ∧ = Dom ∨ = Dom ⇒ = 𝕋^{2}
Dom ⋄ = 𝕋

であり、作用は u, v ∈ 𝕋^{2} に対して、

u ∧ v = inf {u, v}
u ∨ v = sup {u, v}
u^{⋄} = 1 − u
u ⇒ v = u^{⋄} ∨ v

ただし、 inf, sup は W_{ϕ}(= 𝕋) での順序に関する下限である。 n 変数関数記号 f と n 変数述語記号 p について、

\begin{matrix}f ∈ W_{ε}^{n} → W_{ε} \\ p ∈ W_{ε}^{n} → 𝕋 \end{matrix}

なるものとする。

この例が認識可能世界であることは以下の議論からわかる。

• W が T′ 型代数系であること W と T′ が同類の代数系であることは定義から自明なので、 ρ が準写の定義をみたすことを示せばよい。＜ ∧ について＞ ( T の算法 ∧ の Dom を Dom_{T} ∧ で表し、 W の算法 ∧ の Dom を Dom_{W} ∧ で表すことにする。 ) (w_{1}, w_{2}) ∈ Dom_{W} ∧ ならば (w_{1}, w_{2}) ∈ 𝕋^{2} より、 ρ の定義から (ρw_{1}, ρw_{2}) = (ϕ, ϕ) となる。従って、 (ρw_{1}, ρw_{2}) ∈ Dom_{T} ∧ が成立する。このとき、 w_{1} ∧ w_{2} ∈ 𝕋 より、 ρ(w_{1} ∧ w_{2}) = ϕ となる。さらに ρw_{1} ∧ ρw_{2} = ϕ ∧ ϕ = ϕ より ρ(w_{1} ∧ w_{2}) = ρw_{1} ∧ ρw_{2} が成立する。一方、 (ρw_{1}, ρw_{2}) ∈ Dom_{T} ∧ で w_{1}, w_{2} ∈ W とする。このとき、 Dom_{T} ∧ = {ϕ}^{2} より、 (ρw_{1}, ρw_{2}) = (ϕ, ϕ) となる。従って、 (w_{1}, w_{2}) ∈ W_{ϕ}^{2} が成立する。すなわち、 (w_{1}, w_{2}) ∈ Dom_{W} ∧ となる。ゆえに、 ρ は ∧ に関して準写の定義をみたす。他のブール子、関数記号、述語記号のときも同様に示せるので W が T′ 型代数系であることがわかる。

• 任意の t ∈ σ(P rm) に対して W_{t} ≠ ∅ をみたすこと σ(P rm) = {ε} で W_{ε} は空集合ではないので t ∈ σ(P rm) なら W_{t} ≠ ∅ となる。なお、演繹論の研究を推し進めていくには、形式言語の定義三条件に条件 (4) を付け加えたうえ、認識可能世界の定義二条件に

(3) 文型 ϕ について W_{ϕ} = 𝕋(= {0, 1}) をみたす。 (𝕋 の元 1, 0 をそれぞれ真、偽という。 )

をみたす代数系を新たに認識可能世界と定義しなおさなければならない。 (詳しくは参考文献 [1] を参照していただきたい。 ) 従って、 (1),(2) をみたす代数系は『真偽のない認識可能世界』と呼ぶべきであるが、概略で書いたとおりこの論文では演繹論まで言及しないので『真偽のない』を省略する。

3.3 付値と意味写像

この節を通じて、 (A, T, σ, P rm) を形式言語とし、 W をそれにとっての認識可能世界とする。ここでは、意味論である意味写像を定める。

3.3.1 定付値と変付値

Φ ∈ Con → W に対して、 Φ が A から W への定付値であるとは、

Φ(Con_{t}) ⊆ W_{t} (∀ t ∈ T)

をみたすことをいう。このような定付値 Φ の存在が以下の議論からわかる。

• Con = ∅ のとき Con → W は空集合律より {∅} となる。そこで、 Φ として空写像 ∅ をとる。また、 Con = ∅ より任意の t ∈ T に対して Con_{t} = ∅ となる。従って c ∈ Con_{t} なる c が存在しないことから、 Φ が定付値の条件をみたすことがわかる。

• Con ≠ ∅ のとき認識可能世界の定義より、任意の t ∈ σ(P rm) に対して W_{t} ≠ ∅ が成立するので、任意の c ∈ Con に対して W_{σc} ≠ ∅ となる。そこで、 c ∈ Con に対して存在の保証された W_{σc} の元 w_{σc} をとり、 Φ ∈ Con → W を Φc = w_{σc} (c ∈ Con) と定める。この Φ が定付値の定義をみたすことは自明なので、定付値の存在がわかる。

次に、 v ∈ V ar → W に対して、 v が A から W への変付値であるとは、

v(V ar_{t}) ⊆ W_{t} (∀ t ∈ T)

をみたすことをいう。このような変付値 v の存在が以下の議論からわかる。形式言語の定義より V ar ≠ ∅ である。また、認識可能世界の定義より、任意の t ∈ σ(P rm) に対して W_{t} ≠ ∅ が成立するので、任意の x ∈ V ar に対して W_{σx} ≠ ∅ となる。そこで、 x ∈ V ar に対して存在の保証された W_{σx} の元 w_{σx} をとり、 v ∈ V ar → W を vx = w_{σx} (x ∈ V ar) と定める。この v が変付値の定義をみたすことは自明なので、変付値が存在することがわかる。そして A から W への変付値全体を V al_{W} で表す。ただし、誤解の恐れがないときは、添え字の W を省略して V al で表す。また、変付値が存在することから、 V al ≠ ∅ であることがわかる。

次に、値換を定義する。変数 x とそれと同型の W の元 c に対して、値換 (\frac{x}{w} ) ∈ V al → V al を以下のように定義する。

v ∈ V al に対して (\frac{x}{w} )v ∈ V al を

((\frac{x}{w} )v)z = \{ \begin{matrix}w & (if z = x) \\ vz & (if z ≠ x) \end{matrix} (z ∈ V ar)

とする。この (\frac{x}{w} )v が V al の元であることは定義から自明である。

また、変数列 x_{1}, ..., x_{n} と、各 x_{i} と同型の W の元 w_{i} に対して、値換 (\frac{x_{i}}{w_{i}} ) (i = 1, 2, ..., n) の合

成を、 (\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} ) で表す。つまり、

(\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v = ((\frac{x_{n}}{w_{n}} )(...((\frac{x_{1}}{w_{1}} )v)...))

と定める。

命題 3.3.1 x_{1}, ..., x_{n} を変数列とし、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とする。また、 i = 1, 2, ..., n に対して w_{i} を W_{σx_{i}} の元とし、 v を V al の元とする。このとき、次のことが成立する。

(1) 任意の i ∈ \{i_{1}, ..., i_{s}\} に対して、 ((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)x_{i} = w_{i} が成立する。

(2) (\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v = (\frac{x_{i_{s}}}{w_{i_{s}}} )…(\frac{x_{i_{1}}}{w_{i_{1}}} )v

(1) の証明 i ∈ {i_{1}, ..., i_{s}} より、命題 2.1.1 から x_{i} ∉ {x_{i+1}, ..., x_{n}} が成立する。従って値換の定義から

((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)x_{i} = ((\frac{x_{i}}{w_{i}} )…(\frac{x_{1}}{w_{1}} )v)x_{i} = w_{i}

が成立する。

q.e.d.

(2) の証明 x を V ar の任意の元とする。 x ∉ {x_{1}, ..., x_{n}} であれば、命題 2.1.1 より {x_{1}, ..., x_{n}} = {x_{i_{1}}, ..., x_{i_{s}}} なので、 x ∉ {x_{i_{1}}, ..., x_{i_{s}}} となる。従って、値換の定義から

((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)x = vx = ((\frac{x_{i_{s}}}{w_{i_{s}}} )…(\frac{x_{i_{1}}}{w_{i_{1}}} )v)x

が成立する。 x ∈ {x_{1}, ..., x_{n}} であれば、 {x_{1}, ..., x_{n}} = {x_{i_{1}}, ..., x_{i_{s}}} より、 x = x_{i} をみたす i ∈ {i_{1}, ..., i_{s}} が存在する。従って (1) より、

((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)x = w_{i}

となる。一方、 {j_{1}, ..., j_{l}} = {k ∈ {i_{1}, ..., i_{s}} | k > i} とおくと、命題 2.1.1 より x_{i_{1}}, ..., x_{i_{s}} は相異なる列であるので、 x_{i} ∉ {x_{j_{1}}, ..., x_{j_{l}}} が成立する。従って、値換の定義より

((\frac{x_{i_{s}}}{w_{i_{s}}} )…(\frac{x_{i_{1}}}{w_{i_{1}}} )v)x = ((\frac{x_{i}}{w_{i}} )…(\frac{x_{i_{1}}}{w_{i_{1}}} )v)x

となる。さらに、 x = x_{i} より

((\frac{x_{i}}{w_{i}} )…(\frac{x_{i_{1}}}{w_{i_{1}}} )v)x = w_{i}

が成立する。従って、 (\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v = (\frac{x_{i_{s}}}{w_{i_{s}}} )…(\frac{x_{i_{1}}}{w_{i_{1}}} )v が成立する。

q.e.d.

命題 3.3.2 x_{1}, ..., x_{n},y_{1}, ..., y_{m} を変数列とし、 w_{i} ∈ W_{σx_{i}} (i = 1, 2, ..., n), u_{j} ∈ W_{σy_{j}} (j = 1, 2, ..., m) とする。このとき、 {x_{1}, ..., x_{n}} ∩ {y_{1}, ..., y_{m}} = ∅ ならば、任意の v ∈ V al に対して、

(\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )(\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v = (\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )(\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v

が成立する。

証明 {x_{1}, ..., x_{n}} ∩ {y_{1}, ..., y_{m}} = ∅ であるので、 z ∈ V ar ならば

\{ \begin{matrix}z ∈ \{x_{1}, ..., x_{n}\}, z ∉ \{y_{1}, ..., y_{m}\} \\ z ∈ \{y_{1}, ..., y_{m}\}, z ∉ \{x_{1}, ..., x_{n}\} \\ z ∈ V ar − (\{x_{1}, ..., x_{n}\} ∪ \{y_{1}, ..., y_{m}\}) \end{matrix}

のいずれかが成立する。

• z ∈ {x_{1}, ..., x_{n}}, z ∉ {y_{1}, ..., y_{m}} が成立するとき I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とすると、命題 2.1.1 より {x_{1}, ..., x_{n}} = {x_{i_{1}}, ..., x_{i_{s}}} が成り立つので、 z ∈ {x_{1}, ..., x_{n}} ならば z = x_{i} なる i ∈ {i_{1}, ..., i_{s}} が存在する。このとき、

v_{y} = (\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v とおけば、

((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )(\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)z = ((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v_{y})z
= w_{i}  (∵ z = x_{i}より命題 3.3.1)
((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )(\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)z = ((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)z (∵ z ∉ \{y_{1}, ..., y_{m}\})
= w_{i}  (∵ z = x_{i}より命題 3.3.1)

となり成立。

• z ∈ {y_{1}, ..., y_{m}}, z ∉ {x_{1}, ..., x_{n}} が成立するとき同様に示される。

• z ∈ V ar − ({x_{1}, ..., x_{n}} ∪ {y_{1}, ..., y_{m}}) が成立するとき z ∉ {x_{1}, ..., x_{n}, y_{1}, ..., y_{m}} より

\begin{aligned}((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )(\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)z & = & vz \\ ((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )(\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)z & = & vz \end{aligned}

となり成立。従って、

(\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )(\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v = (\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )(\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v

が成立する。

q.e.d.

3.3.2 認識可能世界の V al 乗の T 型代数構造

T の任意の可変子 λ (= ...y_{1}...y_{2}......y_{m}...) に対し、その Dom を D_{λ} とおく。このとき、写像

λ_{W} ∈ ( ⋃_{d∈D_{λ}}(W_{σy_{1}} → (... → (W_{σy_{m}} → W_{d})...)))→ W

で以下をみたすものを任意にとる。

λ_{W} f ∈ W_{λd} ( ∀ d ∈ D_{λ}, ∀ f ∈ W_{σy_{1}} → (... → (W_{σy_{m}} → W_{d})...) )

ただし、 λd は d に算法 λ を施してできる T の元である。そうすると、認識可能世界 W の V al 乗

W^{V al} = ⋃_{t∈T}(V al → W_{t})

に T 型代数構造を以下のように定めることができる。まず、認識可能世界の定義より W は T′ 型代数系なので巾代数系として W^{V al} を T′ 型代数系にする。 (この代数構造を (β_{λ})_{λ∈Λ′} とする。 ) 次に、 T′ 型代数構造から除かれていた T の可変子 λ (= ...y_{1}...y_{2}......y_{m}...) に対応する算法 β_{λ} を定義する。

そのために、 d ∈ D_{λ}, φ ∈ V al → W_{d}, v ∈ V al に対して、

φ((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v)∈ W_{σy_{1}} → (... → (W_{σy_{m}} → W_{d})...)

を以下のように定義する。 w_{j} ∈ W_{σy_{j}} (j = 1, 2, ..., m) に対して、

(...((φ((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v))w_{1})...)w_{m} = φ((\frac{y_{m}}{w_{m}} )…(\frac{y_{1}}{w_{1}} )v)

とする。ただし、右辺の (\frac{y_{m}}{w_{m}} )…(\frac{y_{1}}{w_{1}} ) は値換である。最後に、 λ に対応する算法 β_{λ} を以下のように定める。 Dom β_{λ} = ⋃_{d∈D_{λ}}(V al → W_{d}) とし、 φ ∈ Dom β_{λ} に対して、 β_{λ}φ ∈ ⋃_{d∈D_{λ}}(V al → W_{λd}) を

(β_{λ}φ)v = λ_{W} (φ((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v)) (∀ v ∈ V al)

とする。このとき、 φ ∈ V al → W_{d} (⊆ Dom β_{λ}) (d ∈ D_{λ}) なる φ に対して、

φ((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v)∈ W_{σy_{1}} → (... → (W_{σy_{m}} → W_{d})...)

より、 λ_{W} の定義から、

(β_{λ}φ)v = λ_{W} (φ((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v))∈ W_{λd}

となる。従って、

β_{λ}φ ∈ V al → W_{λd}

であることに注意する。また、 λ が空算法の場合は W^{V al} 上の算法 β_{λ} の Dom も ∅ となるので、 W^{V al} 上でも空算法である。以上より、 W^{V al} に T の可変子に対応する算法を定義することができた。

次に、 W^{V al} が T 型代数系であることを確認する。そこで、 W^{V al} から T′ への準写を τ とする^{1}。このとき、 W^{V al} が T 型代数系であることを示すためには、可変子 λ に対応する算法 β_{λ} に対し、 τ が準写の定義をみたすことを示せばよい。 ( 可変子 λ に対応する算法の定義から β_{λ} は単項算法であることに注意する。 )

• b ∈ Dom β_{λ} ならば、 τb ∈ Dom λ で τ(β_{λ}b) = λ(τb) が成立すること。 b ∈ Dom β_{λ} ならば b ∈ V al → W_{d} をみたす Dom λ の元 d が存在する。このとき、 τ の定義より τb = d なので τb ∈ Dom λ が成立する。また、可変子に対応する W^{V al} 上の算法の定義より、 β_{λ}b ∈ V al → W_{λd} なので τ(β_{λ}b) = λd = λ(τb) となる。

• b ∈ W^{V al} で τb ∈ Dom λ ならば、 b ∈ Dom β_{λ} が成立すること b ∈ W^{V al} より b ∈ V al → W_{d} なる T の元 d が存在する。このとき、 τb ∈ Dom λ であり、 τb = d より d ∈ Dom λ が成立する。従って、可変子に対応する W^{V al} 上の算法の定義より、 b ∈ V al → W_{d} ⊆ Dom β_{λ} が成立する。以上より、 W^{V al} は T 型代数系であることが確かめられた。なお、ここで使った写像 λ_{W} を λ の W 上での意味とよび、 T の可変子 λ にその W 上での意味 λ_{W} を対応させる写像 λ ↦ λ_{W} を可変子の W への意味付けという。

1τ の具体的な定義は 1.1 節 (巾代数系の定義) 参照

例 3.3.1 (A, T, σ, P rm) を一階述語言語とし W を例 3.2.2 で定めた一階述語言語の認識可能世界とする。 T の可変子 ∀x_{1}...x_{n} に対して写像 (∀x_{1}...x_{n})_{W} ∈ (W_{σx_{1}} → (... → (W_{σx_{n}} → W_{ϕ})...))→ W_{ϕ} を以下のように定める。 f ∈ W_{σx_{1}} → (... → (W_{σx_{n}} → W_{ϕ})...) に対して、

(∀x_{1}...x_{n})_{W} f = inf {(...((fw_{1})w_{2})...)w_{n} | w_{i} ∈ W_{σx_{i}} (i = 1, 2, ..., n)}

とする。ただし、 inf は W_{ϕ}(= 𝕋) での順序に関する下限である。このとき、 (∀x_{1}...x_{n})_{W} は ∀x_{1}...x_{n} に対する意味であることが以下の議論からわかる。 Dom ∀x_{1}...x_{n} = {ϕ} であるので、

(∀x_{1}...x_{n})_{W} ∈ ( ⋃_{d∈{ϕ}}(W_{σx_{1}} → (... → (W_{σx_{n}} → W_{d})...)))→ W

となる。また、 ∀x_{1}...x_{n} ϕ = ϕ より、 f ∈ W_{σx_{1}} → (... → (W_{σx_{n}} → W_{ϕ})...) に対して、 (∀x_{1}...x_{n})_{W} f ∈ 𝕋 = W_{ϕ} = W_{(∀x_{1}...x_{n} ϕ)} が成立する。従って、 (∀x_{1}...x_{n})_{W} が ∀x_{1}...x_{n} に対する意味であることがわかる。同様に、 ∃x_{1}...x_{n} の意味付けを

(∀x_{1}...x_{n})_{W} f = sup {(...((fw_{1})w_{2})...)w_{n} | w_{i} ∈ W_{σx_{i}} (i = 1, 2, ..., n)}

とする。この意味付けにより W^{V al} を T 型代数系とできる。このとき、可変子 ∀x_{1}...x_{n} に対する W^{V al} の算法の Dom は V al → W_{ϕ} となり、 Dom は V al → W_{(∀x_{1}...x_{n} ϕ)}(= W_{ϕ}) となる。

また、以下のことが成立する。

(1) φ ∈ V al → W_{ϕ} と x_{1}, x_{2} ∈ V ar に対して、 (∀x_{1}x_{2} φ) = (∀x_{1}(∀x_{2} φ))

(2) x ∈ V ar に対して、 ∀xx = ∀x

(3) φ ∈ V al → W_{ϕ} と x_{1}, x_{2} ∈ V ar に対して、 (∃x_{1}x_{2} φ) = (∃x_{1}(∃x_{2} φ))

(4) x ∈ V ar に対して、 ∃xx = ∃x

(1) の証明 v ∈ V al とする。

(∀x_{1}x_{2} φ)v = inf \{φ((\frac{x_{2}}{w_{2}} )(\frac{x_{1}}{w_{1}} )v) | w_{1} ∈ W_{σx_{1}}, w_{2} ∈ W_{σx_{2}}\}

(∀x_{1}(∀x_{2} φ))v = inf \{(∀x_{2} φ)((\frac{x_{1}}{w_{1}} )v) | w_{1} ∈ W_{σx_{1}}\}
= inf \{inf \{φ((\frac{x_{2}}{w_{2}} )(\frac{x_{1}}{w_{1}} )v) | w_{2} ∈ W_{σx_{2}}\} | w_{1} ∈ W_{σx_{1}}\}

よりわかる。

q.e.d.

(2) の証明 φ ∈ Dom ∀xx (= Dom ∀x), v ∈ V al に対して、

(∀xx φ)v = inf \{φ((\frac{x}{w_{2}} )(\frac{x}{w_{1}} )v) | w_{1}, w_{2} ∈ W_{σx}\}

である。このとき、命題 3.3.1 より (\frac{x}{w_{2}} )(\frac{x}{w_{1}} ) = (\frac{x}{w_{2}} ) なので、

(∀xx φ)v = inf \{φ((\frac{x}{w_{2}} )v) | w_{1}, w_{2} ∈ W_{σx}\}
= inf \{φ((\frac{x}{w_{2}} )v) | w_{2} ∈ W_{σx}\}
= (∀x φ)v

となる。

q.e.d.

同様に (3),(4) が示せる

3.3.3 定付値が定める意味写像

Φ を A から W への定付値とし、 T の可変子の W への意味付け λ ↦ λ_{W} を定めることにより W^{V al} の T 型代数構造が定めてあるものとする。そうすると、 (A, T, σ, P rm) が T 型の普遍型付代数系であることを使って、 A から W^{V al} への保型準写 Φ^{∗} を以下のように作ることができる。まず、任意の t ∈ T に対して写像

Φ_{t} ∈ P rm_{t} → (V al → W_{t})

を次のように定めることができる。すなわち、 a ∈ P rm_{t} (= Con_{t} ⨿ V ar_{t}) と v ∈ V al に対して

(Φ_{t}a)v = \{ \begin{matrix}Φa & (if a ∈ Con_{t}) \\ va & (if a ∈ V ar_{t}) \end{matrix}

従って、写像の族 (Φ_{t})_{t∈T} が出来るが P rm = ∐_{t∈T} P rm_{t} なので、これらすべてが一写像

Φ′ ∈ P rm → W^{V al}

に一意に拡張され、 Φ′(P rm_{t}) ⊆ V al → W_{t} が成り立つ (t ∈ T)。つまり、 Φ′ は P rm から W^{V al} への保型写像である。従って、 A の普遍性により Φ′ はさらに保型準写

Φ^{∗} ∈ A → W^{V al}

に一意に拡張される。こうして出来る Φ^{∗} を定付値 Φ の定める意味写像という。

この意味写像は、以下の二条件をみたす写像として特徴付けられる。

(1) Φ^{∗} は A から W^{V al} への保型準写

(2) a ∈ P rm, v ∈ V al に対して (Φ^{∗}a)v = \{ \begin{matrix}Φa & (if a ∈ Con) \\ va & (if a ∈ V ar) \end{matrix}

注意 3.3.1 任意の t ∈ σ(A) に対して、 W_{t} ≠ ∅ であることが以下の議論から示される。 t ∈ σ(A) とする。このとき t = σa なる A の元 a が存在する。そして、 Φ^{∗} は保型準写であることから、 Φ^{∗}a ∈ V al → W_{σa} が成立する。また、 V al ≠ ∅ より v ∈ V al に対して (Φ^{∗}a)v ∈ W_{σa} が存在する。従って、 W_{t} ≠ ∅ であることがわかる。

第4章表現関数

4.1 表現関数

この節では、 A の元によって表現される関数 (表現関数) の定義をする。また、この節を通じて、 (A, T, σ, P rm) を形式言語として、 W をそれにとっての認識可能世界、 Φ を A から W への定付値とする。 V al は V al_{W} を表し、 T の可変子の W への意味付け λ ↦ λ_{W} により、 W^{V al} の T 型代数構造が定めてあるものとし、 A, W^{V al}, W の代数構造を (α_{λ})_{λ∈Λ}, (β_{λ})_{λ∈Λ}, (ω_{λ})_{λ∈Λ′} とする。ただし、可変子 λ に対しては、 α_{λ}, β_{λ} を λ で表す。

まず、 a の自由変数列を定義する。 A の元 a に対して、変数列 x_{1}, ..., x_{n} が a の自由変数列であるとは

F var^{a} ⊆ {x_{1}, ..., x_{n}}

をみたすことをいう。注 (自由変数列の存在) 定理 1.1.2 より、 P rm^{a} は有限集合で、 F var^{a} ⊆ P rm_{F}^{a} ⊆ P rm^{a} なので、 F var^{a} は有限集合である。従って、 F var^{a} ⊆ {x_{1}, ..., x_{n}} をみたす変数列が存在する。

次に、表現関数の定義をする。 a を A の元とし、その元の自由変数列を x_{1}, ..., x_{n} とする。そして、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とする。このとき、表現関数 a^{Φ}(x_{1}, ..., x_{n}) ∈ W_{σx_{1}} ×…× W_{σx_{n}} → W_{σa} を以下のように定義する。任意の (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} に対して、 v ∈ V al を vx_{i} = w_{i} (i ∈ {i_{1}, ..., i_{s}}) をみたすものとし ( このような v ∈ V al は一意には決まらないがその中の一つをとる)

(a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{n}) = (Φ^{∗}a)v

と定義する。このとき、 a^{Φ}(w_{1}, ..., w_{n}) が vx_{i} = w_{i} (i ∈ {i_{1}, ..., i_{s}}) なる v ∈ V al のとり方に依らないことを示す。

定理 4.1.1 (意味写像定理)a ∈ A, v, v′ ∈ V al とし、任意の x ∈ F var^{a} に対して vx = v′x が成り立つと仮定する。このとき、 (Φ^{∗}a)v = (Φ^{∗}a)v′ が成立する。

証明 rk a に関する帰納法で示す。

(1) rk a = 0 (i.e. a ∈ P rm) (1.1) a ∈ Con のとき a ∈ Con なので意味写像の定義より (Φ^{∗}a)v, (Φ^{∗}a)v′ ともに Φa となり成立。 (1.2) a ∈ V ar のとき a ∈ V ar なので意味写像の定義より (Φ^{∗}a)v = va, (Φ^{∗}a)v′ = v′a となる。このとき、 a ∈ {a} = F var^{a} より仮定から va = v′a となり、 (Φ^{∗}a)v = (Φ^{∗}a)v′ が成立する。

(2) rk a > 0 (a = α_{λ}(a_{1}, ..., a_{n_{λ}}) とする。 ) (2.1) λ が不変子のとき

\begin{aligned}(Φ^{∗}a)v & = & (Φ^{∗}(α_{λ}(a_{1}, ..., a_{n_{λ}})))v \\ & = & (β_{λ}(Φ^{∗}a_{1}, ..., Φ^{∗}a_{n_{λ}}))v & (∵ Φ^{∗} は A から W^{V al} への保型準写) \\ & = & ω_{λ}((Φ^{∗}a_{1})v, ..., (Φ^{∗}a_{n_{λ}})v) & (∵射影 v は T′ 型代数系として準写) \end{aligned}

となる。同様に

(Φ^{∗}a)v′ = ω_{λ}((Φ^{∗}a_{1})v′, ..., (Φ^{∗}a_{n_{λ}})v′)

が成立する。このとき、 λ は不変子より命題 3.1.1 から F var^{a} = ∪_{k=1}^{n_{λ}}F var^{a_{k}} となる。従って、 k = 1, 2, ..., n_{λ} に対して、 ∀ x ∈ F var^{a_{k}} ⇒ x ∈ F var^{a} なので仮定より、 vx = v′x となる。さらに、 rk a > rk a_{k} なので、 rk a に関する帰納法の仮定より (Φ^{∗}a_{k})v = (Φ^{∗}a_{k})v′ となる。従って、 (Φ^{∗}a)v = (Φ^{∗}a)v′ が成立する。

(2.2) λ が可変子のとき ( λ = ...y_{1}...y_{2}......y_{m}... とする。 ) λ は可変子より単項算法 (空算法も単項算法とみなしている) で、 a = λ(a_{1}, ..., a_{n_{λ}}) より λ は空算法でない。そこで、 a = λa_{1} とする。 Φ^{∗} は A から W^{V al} への保型準写なので、

\begin{aligned}(Φ^{∗}a)v & = & (Φ^{∗}(λa_{1}))v \\ & = & (λ(Φ^{∗}a_{1}))v \end{aligned}

となる。このとき、 W^{V al} 上の T の可変子に対応する算法の定義から、

(Φ^{∗}a)v = λ_{W} ((Φ^{∗}a_{1})((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v))

が成立する。同様に、 (Φ^{∗}a)v′ = λ_{W} ((Φ^{∗}a_{1})((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v′)) となる。

従って、 (Φ^{∗}a)v = (Φ^{∗}a)v′ を示すには、

(Φ^{∗}a_{1})((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v)= (Φ^{∗}a_{1})((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v′)

を示せばよい。つまり、 u_{j} = W_{σy_{j}}(j = 1, 2, ..., m) に対して、

(Φ^{∗}a_{1})((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)= (Φ^{∗}a_{1})((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v′)

を示す。これを示すには、 ∀ x ∈ F var^{a_{1}} に対して

((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)x = ((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v′)x

が成立することを示せばよい。なぜならば、上の等式が成立すれば、 rk a > rk a_{1} なので、帰納法

の仮定から (Φ^{∗}a_{1})((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)= (Φ^{∗}a_{1})((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v′) であることがわかるから

である。そこで、 ∀ x ∈ F var^{a_{1}} とすると、命題 3.1.1 から F var^{a_{1}} ⊆ F var^{a}∪V ar^{λ} なので、 x ∈ F var^{a}∪V ar^{λ} となる。このとき、 x ∈ V ar^{λ}, x ∈ F var^{a} − V ar^{λ} で場合わけをする。

• x ∈ V ar^{λ} のとき V ar^{λ} = {y_{1}, ..., y_{m}} より、 I(y_{1}, ..., y_{m}) = j_{1}, ..., j_{t} (t = m(y_{1}, ..., y_{m})) とすると、 V ar^{λ} = {y_{j_{1}}, ..., y_{j_{t}}} となる。従って、 x = y_{j} なる j ∈ {j_{1}, ..., j_{t}} が存在する。このとき命題 3.3.1 から

\begin{aligned}((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)x & = & u_{j} \\ ((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v′)x & = & u_{j} \end{aligned}

となる。従って x ∈ V ar^{λ} のときは等号成立。

• x ∈ F var^{a} − V ar^{λ} のとき x ∉ V ar^{λ} = {y_{1}, ..., y_{m}} より値換の定義から

\begin{aligned}((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)x & = & vx \\ ((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v′)x & = & v′x \end{aligned}

となる。また、 x ∈ F var^{a} より仮定から vx = v′x が成立するので、 x ∈ F var^{a} − V ar^{λ} のときも等号成立。

以上より、題意が成立する。

q.e.d.

意味写像定理により、表現関数が定義できることがわかった。また以下では、誤解の恐れがない場合 (a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{n}) を a^{Φ}(w_{1}, ..., w_{n}) で表すことにする。

4.2 代入値換定理

この節では、本論文の目標のために必要な諸定理を証明する。また、この節を通じて、 (A, T, σ, P rm) を形式言語として、 W をそれにとっての認識可能世界とし、 Φ を A から W への定付値とする。 V al は V al_{W} を表し、 T の可変子の W への意味付け λ ↦ λ_{W} により、 W^{V al} の T 型代数構造が定めてあるものとし、 A, W^{V al}, W の代数構造を (α_{λ})_{λ∈Λ}, (β_{λ})_{λ∈Λ}, (ω_{λ})_{λ∈Λ′} とする。ただし、可変子 λ に対しては、 α_{λ}, β_{λ} を λ で表す。

定理 4.2.1 (代入値換定理)a ∈ A, x_{1}, ..., x_{n} を変数列、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とし、 i ∈ {1, 2, ..., n} に対して、 c_{i} を x_{i} と同型の A の元とする。そして、 k ∈ {i_{1}, ..., i_{s}} に対して、 a において x_{k} が c_{k} から自由であると仮定すると、任意の v ∈ V al について次の式が成り立つ

(Φ^{∗}(a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )))v = (Φ^{∗}a)((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)

証明 n と rk a に関する帰納法で証明していく。

(1)n = 0

定義より、代入 (\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) は恒等写像で、値換 (\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )は恒等変換なので、左

辺、右辺ともに (Φ^{∗}a)v となる。従って成立。

(2)n > 0 とする。 x_{1}, ..., x_{n} の中に重複するものがあるとき (i.e. m(x_{1}, ..., x_{n}) < n) 代入の定義より、

a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) = a(\frac{x_{i_{1}}, ..., x_{i_{s}}}{c_{i_{1}}, ..., c_{i_{s}}} )

なので、

左辺 = (Φ^{∗}(a(\frac{x_{i_{1}}, ..., x_{i_{s}}}{c_{i_{1}}, ..., c_{i_{s}}} )))v

となる。一方、右辺は命題 3.3.1 より

(\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v = (\frac{x_{i_{s}}}{(Φ^{∗}c_{i_{s}})v} )…(\frac{x_{i_{1}}}{(Φ^{∗}c_{i_{1}})v} )v

なので

右辺 = (Φ^{∗}a)((\frac{x_{i_{s}}}{(Φ^{∗}c_{i_{s}})v} )…(\frac{x_{i_{1}}}{(Φ^{∗}c_{i_{1}})v} )v)

となる。このとき、 ♯{x_{i_{1}}, ..., x_{i_{s}}} = m(x_{1}, ..., x_{n}) < n で、仮定より、『a ∈ A において x_{k} が c_{k} から自由』 (k ∈ {i_{1}, ..., i_{s}}) であることから、 n に関する帰納法の仮定より、

(Φ^{∗}(a(\frac{x_{i_{1}}, ..., x_{i_{s}}}{c_{i_{1}}, ..., c_{i_{s}}} )))v = (Φ^{∗}a)((\frac{x_{i_{s}}}{(Φ^{∗}c_{i_{s}})v} )…(\frac{x_{i_{1}}}{(Φ^{∗}c_{i_{1}})v} )v)

となる。従って、左辺 = 右辺が成立する。そこで、 x_{1}, ..., x_{n} を相異なる変数列とする。このとき、 I(x_{1}, ..., x_{n}) = 1, 2, ..., n より仮定の『a ∈ A において x_{k} が c_{k} から自由』 (k ∈ {i_{1}, ..., i_{s}}) は、『a ∈ A において x_{i} が c_{i} から自由』 (i = 1, 2, ..., n) となる。

(2.1) rk a = 0 (i.e. a ∈ P rm)

(2.1.1) a ∈ Con のとき＜左辺＞

Con ⨿ V ar より a ∉ \{x_{1}, ..., x_{n}\} となる。従って、 a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) = a より左辺 = (Φ^{∗}a)v が成立

する。このとき、 a ∈ Con なので Φ^{∗} の定義より、左辺 = Φa となる。＜右辺＞ a ∈ Con なので、 Φ^{∗} の定義より、右辺 = Φa となる。従って、左辺=右辺

(2.1.2) a ∈ {x_{1}, ..., x_{n}} (a = x_{i}) のとき＜左辺＞

代入の定義より、 a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) = c_{i} なので、左辺 = (Φ^{∗}c_{i})v が成立する。

＜右辺＞

a ∈ V ar なので Φ^{∗} の定義より右辺 = ((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)a が成立する。さらに、 a = x_{i}

より、右辺 = (Φ^{∗}c_{i})v となる。従って、左辺=右辺

(2.1.3) a ∈ V ar − {x_{1}, ..., x_{n}} のとき＜左辺＞

代入の定義より、 a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) = a なので、左辺 = (Φ^{∗}a)v が成立する。さらに a ∈ V ar より Φ^{∗}

の定義から左辺 = va となる。＜右辺＞

a ∈ V ar なので Φ^{∗} の定義より右辺 = ((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)a が成立する。さらに a ∉

{x_{1}, ..., x_{n}} より、右辺 = va となる。従って、左辺=右辺

(2.2) rk a > 0 (∃ λ ∈ Λ s.t. a = α_{λ}(a_{1}, a_{2}, ..., a_{n_{λ}}))

(2.2.1)∃ h ∈ {1, 2, ..., n} s.t. x_{h} ≪̸ a (x_{h} は a に自由に現れない) ＜左辺＞ x_{1}, ..., x_{n} は相異なる列で x_{h} ≪̸ a より、定理 1.1.10 から、

a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) = a(\frac{x_{1}, ..., x_{h−1}, x_{h+1}, ..., x_{n}}{c_{1}, ..., c_{h−1}, c_{h+1}, ..., c_{n}} )

となる。従って、

左辺 = Φ^{∗}(a(\frac{x_{1}, ..., x_{h−1}, x_{h+1}, ..., x_{n}}{c_{1}, ..., c_{h−1}, c_{h+1}, ..., c_{n}} ))v

となる。このとき、 ♯{1, ..., h − 1, h + 1, ..., n} < n で、仮定より『a において x_{i} が c_{i} から自由』 (i = 1, 2, ..., n) なので、 ∀ j ∈ {1, ..., h − 1, h + 1, ..., n} に対して『a において x_{j} が c_{j} から自由』が成立する。従って n に関する帰納法の仮定から、

左辺 = (Φ^{∗}a)((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{h+1}}{(Φ^{∗}c_{h+1})v} )(\frac{x_{h−1}}{(Φ^{∗}c_{h−1})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)

となる。＜右辺＞ x_{h} ≪̸ a より x_{h} ∉ F var^{a} となる。従って、任意の x ∈ F var^{a} に対して、

((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)x = ((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{h+1}}{(Φ^{∗}c_{h+1})v} )(\frac{x_{h−1}}{(Φ^{∗}c_{h−1})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)x

が成立するので、定理 4.1.1(意味写像定理) から

右辺 = (Φ^{∗}a)((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{h+1}}{(Φ^{∗}c_{h+1})v} )(\frac{x_{h−1}}{(Φ^{∗}c_{h−1})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)

となる。従って、左辺＝右辺

(2.2.2) ∀ h ∈ {1, 2, ..., n} x_{h} ≪ a ＜左辺＞任意の h ∈ {1, 2, ..., n} に対して、 x_{h} ≪ a より、 x_{h} ∈ P rm_{F}^{a} = ⋃_{k=1}^{n_{λ}} P rm_{F}^{a_{k}} − P rm^{λ} (∵定理 1.1.6) となる。従って、 x_{h} ∉ P rm^{λ} (h = 1, 2, ..., n) なので、 {x_{1}, ..., x_{n}} − P rm^{λ} = {x_{1}, ..., x_{n}} が成立する。従って、代入の定義から、

a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) = α_{λ}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ), ..., a_{n_{λ}}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ))

となる。

\begin{aligned}∴左辺 & = & (Φ^{∗}(α_{λ}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ), ..., a_{n_{λ}}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ))))v \\ & = & (β_{λ}(Φ^{∗}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )), ..., Φ^{∗}(a_{n_{λ}}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ))))v & (∵Φ^{∗} : 保型準写) \end{aligned}

＜右辺＞

右辺 = (Φ^{∗}(α_{λ}(a_{1}, ..., a_{n_{λ}})))((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)
= (β_{λ}(Φ^{∗}a_{1}, ..., Φ^{∗}a_{n_{λ}}))((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v) (∵Φ^{∗} : 保型準写)

このとき、 λ が不変子、可変子で場合わけをして等式を示す。

その前に準備として次のことを示す。 ∀ v ∈ V al , ∀ k ∈ {1, 2, ..., n_{λ}} に対して、

(Φ^{∗}(a_{k}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )))v = (Φ^{∗}a_{k})((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v) ……(∗)

rk a_{k} < rk a (∀ k) より i = 1, 2, ..., n に対して、『a_{k} において x_{i} が c_{i} から自由』であることが示せれば、 rk a に関する帰納法の仮定から (∗) が示せる。そこで、これを定理 1.1.8 系 1 を用いて示す。 i = 1, 2, ..., n に対して、 (2.2.2) から x_{i} ≪ a より x_{i} ∈ P rm_{F}^{a} となる。また、定理 1.1.6 より P rm_{F}^{a} = ⋃_{k=1}^{n_{λ}} P rm_{F}^{a_{k}} − P rm^{λ} なので x_{i} ∉ P rm^{λ} となる。従って x_{i} ∈ P rm − P rm^{λ} が成り立つ。また、 {c_{i}} ⊆ A で仮定より、『a において x_{i} は c_{i} から自由』なので、定理 1.1.8 系 1 より、『a_{k} において x_{i} は c_{i} から自由』 (k = 1, 2, ..., n_{λ}) がわかる。 i の任意性より、 i = 1, 2, ..., n に対して、『a_{k} において x_{i} は c_{i} から自由』 (k = 1, 2, ..., n_{λ}) より (∗) が成立注 : (∗) は λ が可変子、不変子いずれでも成立

CASE 1 λ が不変子

左辺 = (β_{λ}(Φ^{∗}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )), ..., Φ^{∗}(a_{n_{λ}}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ))))v

このとき、射影は T′ 型代数系として保型準写なので、

左辺 = ω_{λ}(Φ^{∗}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ))v, ..., Φ^{∗}(a_{n_{λ}}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ))v)

となる。また、 (∗) より

左辺 = ω_{λ}((Φ^{∗}a_{1})((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v), ..., (Φ^{∗}a_{n_{λ}})((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v))

が成立する。さらに、 (\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v ∈ V al よりこれを射影とみると、

左辺 = (β_{λ}(Φ^{∗}a_{1}, ..., Φ^{∗}a_{n_{λ}}))((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)

より、左辺 = 右辺がわかる。 CASE 2 λ が可変子 (λ = ...y_{1}...y_{2}......y_{m}...) λ は可変子より単項算法 (空算法も単項算法とみなしている) で、 a = λ(a_{1}, ..., a_{n_{λ}}) より λ は空算法でない。そこで、 a = λa_{1} とすると

左辺 = (λ(Φ^{∗}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ))))v

となり、 W^{V al} 上の可変子に対応する算法の定義から、

左辺 = λ_{W} ((Φ^{∗}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )))((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v))

となる。一方、右辺は

右辺 = (λ(Φ^{∗}a_{1}))((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)

より、 W^{V al} 上の可変子に対応する算法の定義から

右辺 = λ_{W} ((Φ^{∗}a_{1})((\frac{y_{m}}{□})…(\frac{y_{1}}{□})(\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v))

となる。従って、左辺＝右辺を示すには、

(Φ^{∗}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )))((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v)= (Φ^{∗}a_{1})((\frac{y_{m}}{□})…(\frac{y_{1}}{□})(\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)

を示せばよい。つまり、 ∀ u_{j} ∈ W_{σy_{j}} (j = 1, 2, ..., m) に対して

(Φ^{∗}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )))((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)= (Φ^{∗}a_{1})((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )(\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)

を示す。この式を�とする。

そこで、 v′ = (\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v とおけば

\begin{aligned}�の左辺 & = & (Φ^{∗}(a_{1}(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )))v′ \\ & = & (Φ^{∗}a_{1})((\frac{x_{n}}{(Φ^{∗}c_{n})v′} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v′} )v′) & (∵ v′に対して (∗) を使う) \end{aligned}

が成立する。次に、 (Φ^{∗}c_{i})v′ = (Φ^{∗}c_{i})v (i = 1, 2, ..., n) が成立することを示す。そのためには、 ∀ z ∈ F var^{c_{i}} に対して v′z = vz を示せばよい。なぜならば、そうであれば定理 4.1.1(意味写像定理) から等式が成立することがわかるからである。

そこで、 ∀ z ∈ F var^{c_{i}} とする。このとき、 v′ = (\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v より、 z ∉ \{y_{1}, ..., y_{m}\} が示せれ

ば、値換の定義から v′z = vz がわかる。今、仮定より『a(= λa_{1}) において x_{i} は c_{i} から自由』なので、定理 1.1.8 から、以下のどちらかが成立する。

• x_{i} ≪̸ a

• 『a_{1} において x_{i} は c_{i} から自由』で、 P rm_{F}^{c_{i}} ∩ P rm^{λ} = ∅ このとき (2.2.2) より、 x_{i} ≪ a だったので、『a_{1} において x_{i} は c_{i} から自由』で P rm_{F}^{c_{i}} ∩ P rm^{λ} = ∅ が成立することがわかる。さらに、 {y_{1}, ..., y_{m}} = V ar^{λ} = P rm^{λ} (∵命題 3.1.1) で、 z ∈ F var^{c_{i}} ⊆ P rm_{F}^{c_{i}} より、 {z} ∩ {y_{1}, ..., y_{m}} ⊆ P rm_{F}^{c_{i}} ∩ P rm^{λ} となる。そして、 P rm_{F}^{c_{i}} ∩ P rm^{λ} = ∅ だったので、 z ∉ {y_{1}, ..., y_{m}} となる。従って、 (Φ^{∗}c_{i})v′ = (Φ^{∗}c_{i})v (i = 1, 2, ..., n) が成立する。このことから、

�の左辺= (Φ^{∗}a_{1})((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v′)

となる。さらに、 v′ = (\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v だったので

�の左辺= (Φ^{∗}a_{1})((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )(\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)

が成立する。従って、�式が成立することを示すためには、

(\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )(\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v = (\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )(\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v……�

が成立することを示せばよい。この等式は、 {x_{1}, ..., x_{n}} ∩ {y_{1}, ..., y_{m}} = ∅ が示せれば、命題 3.3.2 から成立することがわかる。今 (2.2.2) より i = 1, 2, ..., n に対して、 x_{i} ≪ a なので、 x_{i} ∈ P rm_{F}^{a} = P rm_{F}^{a_{1}} − P rm^{λ} となる。従って、 x_{i} ∉ P rm^{λ} である。また、命題 3.1.1 より P rm^{λ} = V ar^{λ} で V ar^{λ} = {y_{1}, ..., y_{m}} なので、 x_{i} ∉ {y_{1}, ..., y_{m}} が成り立つ。従って {x_{1}, ..., x_{n}} ∩ {y_{1}, ..., y_{m}} = ∅ より�が成立する。すなわち、可変子の場合も成立。以上より、代入値換定理が成立することがわかる。

q.e.d.

命題 4.2.1 a ∈ A で、 x_{1}, ..., x_{n} を a の自由変数列とする。このとき、任意の (w_{1}, ..., w_{n}) ∈ W_{σx_{1}} ×…× W_{σx_{n}} と v ∈ V al に対して、以下の等式が成立する。

(a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{n}) = (Φ^{∗}a)((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)

証明 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とし、 v′ ∈ V al を v′x_{i} = w_{i} (i ∈ {i_{1}, ..., i_{s}}) をみたすものとする。このとき、表現関数の定義より a^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}a)v′ なので、 y ∈ F var^{a} に対して、

v′y = ((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)y ……�

が示せれば、定理 4.1.1 (意味写像定理) により、

a^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}a)((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)

が示される。そこで、 y ∈ F var^{a} とする。このとき、 x_{1}, ..., x_{n} は a の自由変数列であるので F var^{a} ⊆ {x_{1}, ..., x_{n}} が成立し、命題 2.1.1 より {x_{1}, ..., x_{n}} = {x_{i_{1}}, ..., x_{i_{s}}} なので、 F var^{a} ⊆ {x_{i_{1}}, ..., x_{i_{s}}} となる。従って y = x_{i} なる i ∈ {i_{1}, ..., i_{s}} が存在する。このとき、 v′ の定義より、�の左辺 = v′x_{i} = w_{i} である。また、命題 3.3.1 より�の右辺 = ((\frac{x_{n}}{w_{n}} )…(\frac{x_{1}}{w_{1}} )v)x_{i} = w_{i} となるので、�が成立する。

q.e.d.

定理 4.2.2 a を A の元、 x_{1}, ..., x_{n} を a の自由変数列、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とする。また、 i = 1, 2, ..., n に対して c_{i} を x_{i} と同型の A の元、 y_{1}, ..., y_{m} を各 c_{i} の自由変数列とする。そして、

b = a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )

と定めると以下が成立する。

(1) y_{1}, ..., y_{m} は b の自由変数列

(2) a において x_{l} が c_{l} から自由 (l ∈ {i_{1}, ..., i_{s}}) ならば、任意の (w_{1}, ..., w_{m}) ∈ W_{σy_{1}}×…× W_{σy_{m}} に対して、

(b^{Φ}(y_{1}, ..., y_{m}))(w_{1}, ..., w_{m}) = (a^{Φ}(x_{1}, ..., x_{n}))(c_{1}^{Φ}(w_{1}, ..., w_{m}), ..., c_{n}^{Φ}(w_{1}, ..., w_{m}))

が成立する。ただし、 c_{i}^{Φ}(w_{1}, ..., w_{m}) = (c_{i}^{Φ}(y_{1}, ..., y_{m}))(w_{1}, ..., w_{m}) である。

(1) の証明

b = a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) より定理 2.2.1 を用いると、 P rm_{F}^{b} ⊆ P rm_{F}^{\{c_{i_{1}} ,...,c_{is} \}} ∪ (P rm_{F}^{a} − \{x_{i_{1}}, ..., x_{i_{s}}\})

となる。従って、

\begin{aligned}F var^{b} & = & P rm_{F}^{b} ∩ V ar \\ & ⊆ & (P rm_{F}^{\{c_{i_{1}} ,...,c_{is} \}} ∪ (P rm_{F}^{a} − \{x_{i_{1}}, ..., x_{i_{s}}\}))∩V ar \end{aligned}

が成立し、さらに変形すると、

(P rm_{F}^{{c_{i_{1}} ,...,c_{is} }} ∪ (P rm_{F}^{a} − {x_{i_{1}}, ..., x_{i_{s}}}))∩V ar
= (P rm_{F}^{{c_{i_{1}} ,...,c_{is} }} ∩ V ar) ∪ ((P rm_{F}^{a} − {x_{i_{1}}, ..., x_{i_{s}}}) ∩ V ar)
= F var^{{c_{i_{1}} ,...,c_{is} }} ∪ (F var^{a} − {x_{i_{1}}, ..., x_{i_{s}}})
= (⋃_{l∈{i_{1},...,i_{s}}} F var^{c_{l}}) ∪ (F var^{a} − {x_{i_{1}}, ..., x_{i_{s}}})

となる。そして、仮定から y_{1}, ..., y_{m} は各 c_{l} の自由変数列で、 x_{1}, ..., x_{n} は a の自由変数列なので、

F var^{b} ⊆ {y_{1}, ..., y_{m}} ∪ ({x_{1}, ..., x_{n}} − {x_{i_{1}}, ..., x_{i_{s}}})

が成立する。このとき、命題 2.1.1 より {x_{1}, ..., x_{n}} = {x_{i_{1}}, ..., x_{i_{s}}} なので、

F var^{b} ⊆ {y_{1}, ..., y_{m}}

となる。従って y_{1}, ..., y_{m} は b の自由変数列である。

q.e.d.

(2) の証明 (�) (a^{Φ}(x_{1}, ..., x_{n}))(c_{1}^{Φ}(w_{1}, ..., w_{m}), ..., c_{n}^{Φ}(w_{1}, ..., w_{m})) を定義することができること表現関数の定義より、 i = 1, 2, ..., n に対して、 Im c_{i}^{Φ}(y_{1}, ..., y_{m}) ⊆ W_{σc_{i}} より

(c_{1}^{Φ}(w_{1}, ..., w_{m}), ..., c_{n}^{Φ}(w_{1}, ..., w_{m}))∈ W_{σc_{1}}×…× W_{σc_{n}}

となる。さらに仮定から各 c_{i} と x_{i} は同型なので、

W_{σc_{1}}×…× W_{σc_{n}} = W_{σx_{1}}×…× W_{σx_{n}}

が成立する。また表現関数の定義から、

Dom a^{Φ}(x_{1}, ..., x_{n}) = W_{σx_{1}}×…× W_{σx_{n}}

より、 (c_{1}^{Φ}(w_{1}, ..., w_{m}), ..., c_{n}^{Φ}(w_{1}, ..., w_{m}))∈ Dom a^{Φ}(x_{1}, ..., x_{n}) が成立する。従って、 (a^{Φ}(x_{1}, ..., x_{n})) (c_{1}^{Φ}(w_{1}, ..., w_{m}), ..., c_{n}^{Φ}(w_{1}, ..., w_{m})) を定義することができる。

(�) (b^{Φ}(y_{1}, ..., y_{m}))(w_{1}, ..., w_{m}) = (a^{Φ}(x_{1}, ..., x_{n}))(c_{1}^{Φ}(w_{1}, ..., w_{m}), ..., c_{n}^{Φ}(w_{1}, ..., w_{m})) まず、左辺を計算する。そのために I(y_{1}, ..., y_{m}) = j_{1}, ..., j_{t} (t = m(y_{1}, ..., y_{m})) とし、 v ∈ V al を vy_{h} = w_{h} (h ∈ {j_{1}, ..., j_{t}}) をみたすものとすると、表現関数の定義より左辺 = (Φ^{∗}b)v となる。

そして、 b = a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} ) だったので、

左辺 = (Φ^{∗}(a(\frac{x_{1}, ..., x_{n}}{c_{1}, ..., c_{n}} )))v

が成立する。このとき、仮定から a において x_{l} が c_{l} から自由 (l ∈ {i_{1}, ..., i_{s}}) が成り立っているので、定理 4.2.1(代入値換定理) より

左辺 = (Φ^{∗}a)((\frac{x_{n}}{(Φ^{∗}c_{n})v} )…(\frac{x_{1}}{(Φ^{∗}c_{1})v} )v)

となる。さらに、命題 4.2.1 から

左辺 = (a^{Φ}(x_{1}, ..., x_{n}))((Φ^{∗}c_{1})v, ..., (Φ^{∗}c_{n})v)

が成立する。次に右辺の計算をする。 v ∈ V al は vy_{h} = w_{h} (h ∈ {j_{1}, ..., j_{t}}) をみたすものだったので表現関数の定義より

c_{i}^{Φ}(w_{1}, ..., w_{m}) = (c_{i}^{Φ}(y_{1}, ..., y_{m}))(w_{1}, ..., w_{m}) = (Φ^{∗}c_{i})v

が成立する。従って、

右辺 = (a^{Φ}(x_{1}, ..., x_{n}))((Φ^{∗}c_{1})v, ..., (Φ^{∗}c_{n})v)

となり、左辺と右辺が等しいことがわかる。

q.e.d.

系 1 a を A の元、 x_{1}, ..., x_{n} を a の自由変数列、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とする。また、 y_{1}, ..., y_{n} を変数列、 I(y_{1}, ..., y_{n}) = j_{1}, ..., j_{t} (t = m(y_{1}, ..., y_{n}))、 h = 1, 2, ..., n に対して y_{h} と x_{h} は同型であるとする。そして、

b = a(\frac{x_{1}, ..., x_{n}}{y_{1}, ..., y_{n}} )

と定め、 {i_{1}, ..., i_{s}} ⊆ {j_{1}, ..., j_{t}} が成立していると仮定すると、以下のことが成立する。

(1) y_{1}, ..., y_{n} は b の自由変数列

(2) a において x_{l} が y_{l} から自由 (l ∈ {i_{1}, ..., i_{s}}) ならば

b^{Φ}(y_{1}, ..., y_{n}) = a^{Φ}(x_{1}, ..., x_{n})

が成立する。

証明まず、定理 4.2.2 の仮定をみたすことを示す。 i = 1, 2, ..., n に対して、 F var^{y_{i}} = {y_{i}} ⊆ {y_{1}, ..., y_{n}} より、 y_{1}, ..., y_{n} は各 y_{i} の自由変数列である。従って、定理 4.2.2 において、 m = n, c_{i} = y_{i} (i = 1, 2, ..., n) としたときの仮定をみたすので、以下のことが成立する。 (1)′ y_{1}, ..., y_{n} は b の自由変数列 (2)′ a において x_{l} が y_{l} から自由 (l ∈ {i_{1}, ..., i_{s}}) ならば、任意の (w_{1}, ..., w_{n}) ∈ W_{σy_{1}}×…× W_{σy_{n}} に対して、

(b^{Φ}(y_{1}, ..., y_{n}))(w_{1}, ..., w_{n}) = (a^{Φ}(x_{1}, ..., x_{n}))(y_{1}^{Φ}(w_{1}, ..., w_{n}), ..., y_{n}^{Φ}(w_{1}, ..., w_{n}))

が成立する。ただし、 y_{i}^{Φ}(w_{1}, ..., w_{n}) = (y_{i}^{Φ}(y_{1}, ..., y_{n}))(w_{1}, ..., w_{n}) である。

(�) (1) が成立すること

(1) は (1)′ そのものなので成立。

(�) (2) が成立すること仮定から h = 1, 2, ..., n に対して y_{h} と x_{h} は同型なので、 W_{σy_{1}}×…× W_{σy_{n}} = W_{σx_{1}}×…× W_{σx_{n}} となる。従って、 (2) を示すためには、任意の (w_{1}, ..., w_{n}) ∈ W_{σy_{1}}×…× W_{σy_{n}} に対して、

(b^{Φ}(y_{1}, ..., y_{n}))(w_{1}, ..., w_{n}) = (a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{n}) ……�

を示せばよい。そこでまず、�の左辺を計算する。仮定から、 a において x_{l} が y_{l} から自由 (l ∈ {i_{1}, ..., i_{s}}) なので、 (2)′ より

�の左辺 = (a^{Φ}(x_{1}, ..., x_{n}))(y_{1}^{Φ}(w_{1}, ..., w_{n}), ..., y_{n}^{Φ}(w_{1}, ..., w_{n}))

が成立する。このとき、 v ∈ V al を l ∈ {i_{1}, ..., i_{s}} に対して、 vx_{l} = y_{l}^{Φ}(w_{1}, ..., w_{n}) をみたすものとすると、

�の左辺 = (Φ^{∗}a)v

となる。次に、�の右辺を計算する。 v′ ∈ V al を l ∈ {i_{1}, ..., i_{s}} に対して、 v′x_{l} = w_{l} をみたすものとすると、

�の右辺= (Φ^{∗}a)v′

となる。従って、 z ∈ F var^{a} に対して、 vz = v′z が示せれば、定理 4.1.1 (意味写像定理) より、

(Φ^{∗}a)v = (Φ^{∗}a)v′

が示せる。そこで、 z ∈ F var^{a} とする。このとき、 x_{1}, ..., x_{n} は a の自由変数列より、 F var^{a} ⊆ {x_{1}, ..., x_{n}} が成り立ち、命題 2.1.1 から {x_{1}, ..., x_{n}} = {x_{i_{1}}, ..., x_{i_{s}}} より、 ∃ l ∈ {i_{1}, ..., i_{s}} s.t. z = x_{l} となる。従って、 v の決め方から、

vz = vx_{l} = y_{l}^{Φ}(w_{1}, ..., w_{n})

となる。このとき、 v′′ ∈ V al を h ∈ {j_{1}, ..., j_{t}} に対して、 vy_{h} = w_{h} なるものとすると表現関数の定義から

y_{l}^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}y_{l})v′′

が成立する。そして、 y_{l} ∈ V ar より Φ^{∗} の定義から、

(Φ^{∗}y_{l})v′′ = v′′y_{l}

となる。さらに、仮定より {i_{1}, ..., i_{s}} ⊆ {j_{1}, ..., j_{t}} なので、 l ∈ {j_{1}, ..., j_{t}} が成立する。従って、 v′′ の決め方から、

v′′y_{l} = w_{l}

が成立する。ゆえに、

vz = w_{l}

となる。一方、 l ∈ {i_{1}, ..., i_{s}} より v′ の決め方から、

v′z = v′x_{l} = w_{l}

となる。従って、 vz = v′z が成立する。

q.e.d.

4.3 表現可能関数

この節では、本論文の目標である、『W 上のいかなる関数が A の元によって表現されるのだろうか。』という問について考察する。まず、 W 上の関数を定義し、その後必要な諸定理を示す。また、この節を通じて、 (A, T, σ, P rm) を形式言語として、 W をそれにとっての認識可能世界とし、 Φ を A から W への定付値とする。 V al は V al_{W} を表し、 T の可変子の W への意味付け λ ↦ λ_{W} により、 W^{V al} の T 型代数構造が定めてあるものとし、 A, W^{V al}, W の代数構造を (α_{λ})_{λ∈Λ}, (β_{λ})_{λ∈Λ}, (ω_{λ})_{λ∈Λ′} とする。ただし、可変子 λ に対しては、 α_{λ}, β_{λ} を λ で表す。

ある t_{1}, ..., t_{n}, t ∈ T に対し、 W の t_{i} 部分 W_{t_{i}} (i = 1, 2, ..., n) の直積 W_{t_{1}}×…× W_{t_{n}} 上で定義され W の t 部分 W_{t} の中にに値をもつ関数を型関数という。

例えば以下のようなものがある。

• 定値関数 x_{1}, ..., x_{n} ∈ V ar , w ∈ W_{t} (t ∈ T) に対して、定値関数 (σx_{1}, ..., σx_{n})/w ∈ W_{σx_{1}}×…× W_{σx_{n}} → W_{t} を以下のように定義する。任意の (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} に対して、

((σx_{1}, ..., σx_{n})/w)(w_{1}, ..., w_{n}) = w

と定める。定値関数が型関数であることは自明。

• 射影 x_{1}, ..., x_{n} ∈ V ar , i ∈ {1, 2, ..., n} に対して、射影 (σx_{1}, ..., σx_{n}) ↓ i ∈ W_{σx_{1}}×…× W_{σx_{n}} → W_{σx_{i}} を以下のように定義する。任意の (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} に対して、

((σx_{1}, ..., σx_{n}) ↓ i)(w_{1}, ..., w_{n}) = w_{i}

と定める。射影が型関数であることは自明。

• 表現関数 a ∈ A で、 x_{1}, ..., x_{n} を a の自由変数列とする。このとき、表現関数 a^{Φ}(x_{1}, ..., x_{n}) は定義から a^{Φ}(x_{1}, ..., x_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} → W_{σa} より型関数である。

また型関数の合成も型関数である。つまり、 H_{i} ∈ W_{t_{1}}×…× W_{t_{n}} → W_{u_{i}} (i = 1, 2, ..., m) と G ∈ W_{u_{1}}×…× W_{u_{m}} → W_{t} に対して合成関数

G(H_{1}(w_{1}, ..., w_{n}), ..., H_{m}(w_{1}, ..., w_{n})) ((w_{1}, ..., w_{n}) ∈ W_{t_{1}}×…× W_{t_{n}})

は、 W_{t_{1}}×…× W_{t_{n}} → W_{t} の元となる。従って型関数である。以後、型関数に関わらず上記のような合成を

G ∘ (H_{1}, ..., H_{m})

で表す。ただし、 m ≥ 1 とする。

型関数 F に対して A の元 a とその自由変数列 x_{1}, ..., x_{n} で、 F = a^{Φ}(x_{1}, ..., x_{n}) をみたすものがあるとき Φ の下で a は F を表現するという。また、型関数 F が Φ の下で A のある元によって表現されるとき、 F は Φ の下で表現可能であるという。なお、誤解の恐れがない場合は『Φ の下で』は省略する。

また、表現関数 a^{Φ}(x_{1}, ..., x_{n}) と (w_{1}, ..., w_{i}) ∈ W_{σx_{1}}×…× W_{σx_{i}} (1 ≤ i ≤ n) に対して、

(a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{i}, □, ..., □) ∈ W_{σx_{i+1}} → (... → (W_{σx_{n}} → W_{σa})...)

を w_{j} ∈ W_{σx_{j}} (j = i + 1, ..., n) に対して、

(...(((a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{i}, □, ..., □))w_{i+1})...)w_{n} = (a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{n})

と定める。 (...(((a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{i}, □, ..., □))w_{i+1})...)w_{n} ∈ W_{σa} であることは、表現関数の定義からわかる。なお、誤解の恐れがないときは、 (a^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{i}, □, ..., □) を a^{Φ}(w_{1}, ..., w_{i}, □, ..., □) で表す。

補題 4.3.1 λ ∈ Λ′ でその項数を n_{λ} とする。このとき、 a_{1}, ..., a_{n_{λ}} ∈ A なら、次の二条件は同値である。

1. (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ}, 2. W_{σa_{1}}×…× W_{σa_{n_{λ}}} ⊆ Dom ω_{λ}

証明 W は T′ 型代数系だったので W から T′ への準写 τ が存在する。

(1 ⇒ 2) (w_{1}, ..., w_{n_{λ}}) ∈ W_{σa_{1}}×…× W_{σa_{n_{λ}}} とする。このとき、 W_{σa_{i}} の定義から τw_{i} = σa_{i} (i = 1, 2, ..., n_{λ}) となる。また、 1 より (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ} なので、準写 σ の定義から (σa_{1}, ..., σa_{n_{λ}}) ∈ Dom λ となる。従って、 (τw_{1}, ..., τw_{n_{λ}}) ∈ Dom λ が成立する。このとき、 λ ∈ Λ′ で τ は W から T′ への準写であることから、 (w_{1}, ..., w_{n_{λ}}) ∈ Dom ω_{λ} となり、 W_{σa_{1}}×…× W_{σa_{n_{λ}}} ⊆ Dom ω_{λ} が成立する。

(2 ⇒ 1) 注意 3.3.1 より、任意の t ∈ σ(A) に対して W_{t} ≠ ∅ となる。従って W_{σa_{1}}×…× W_{σa_{n_{λ}}} の元 (w_{1}, ..., w_{n_{λ}}) が存在する。このとき、 2 から (w_{1}, ..., w_{n_{λ}}) ∈ Dom ω_{λ} となるので、 (τw_{1}, ..., τw_{n_{λ}}) ∈ Dom λ が成立する。また、 W_{σa_{i}} の定義から、 τw_{i} = σa_{i} (i = 1, 2, ..., n_{λ}) なので、 (σa_{1}, ..., σa_{n_{λ}}) ∈ Dom λ となる。そして、 σ は準写より (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ} が成立する。

q.e.d.

補題 4.3.2 a ∈ A とし、 x_{1}, ..., x_{n} を a の自由変数列とする。このとき、表現関数 a^{Φ}(x_{1}, ..., x_{n}) に対して、次の二つのことが成立する。

1. a = α_{λ}(a_{1}, ..., a_{n_{λ}}), λ ∈ Λ′ なら

\begin{matrix}(1) & x_{1}, ..., x_{n} は a_{k} の自由変数列 (k = 1, 2, ..., n_{λ}) \\ (2) & a^{Φ}(x_{1}, ..., x_{n}) = ω_{λ} ∘ (a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})) \end{matrix}

2. a = λb, λ が T の可変子 λ(= ...y_{1}......y_{m}...) に対応する A の算法であるなら

\begin{matrix}(1) & x_{1}, ..., x_{n}, y_{1}, ..., y_{m} は b の自由変数列 \\ (2) & (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}}に対してa^{Φ}(w_{1}, ..., w_{n}) = λ_{W} (b^{Φ}(w_{1}, ..., w_{n}, □, ..., □)) \end{matrix}

1 の証明

(1) を示す k = 1, 2, ..., n_{λ} に対して、

\begin{aligned}F var^{a_{k}} & ⊆ & ⋃_{k=1}^{n_{λ}} F var^{a_{k}} \\ & = & F var^{a} & (∵命題 3.1.1) \\ & ⊆ & \{x_{1}, ..., x_{n}\} & (∵仮定より x_{1}, ..., x_{n} は a の自由変数列) \end{aligned}

より、 x_{1}, ..., x_{n} は a_{k} の自由変数列であることがわかる。

(2) を示す

• ω_{λ} ∘ (a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})) を定義することができること。 k = 1, 2, ..., n_{λ} に対して、 a_{k}^{Φ}(x_{1}, ..., x_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} → W_{σa_{k}} より、 W_{σa_{1}}×…× W_{σa_{n_{λ}}} ⊆ Dom ω_{λ} であることを示せばよい。これは、 λ が不変子で (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ} より、補題 4.3.1 から成立する。

• a^{Φ}(x_{1}, ..., x_{n}) = ω_{λ} ∘ (a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})) であること。 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とする。そして、 (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} に対して、 v ∈ V al を vx_{l} = w_{l} (l ∈ {i_{1}, ..., i_{s}}) なるものとすると、

a^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}a)v  (∵表現関数の定義)
= (Φ^{∗}α_{λ}(a_{1}, ..., a_{n_{λ}}))v  (∵ a = α_{λ}(a_{1}, ..., a_{n_{λ}}))
= (β_{λ}(Φ^{∗}a_{1}, ..., Φ^{∗}a_{n_{λ}}))v (∵Φ^{∗}は A からW^{V al}への保型準写)

となる。さらに v の定める射影は、 T′ 型代数系として W^{V al} から W への準写より

a^{Φ}(w_{1}, ..., w_{n}) = ω_{λ}((Φ^{∗}a_{1})v, ..., (Φ^{∗}a_{n_{λ}})v)

が成立する。一方、

(ω_{λ} ∘ (a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})))(w_{1}, ..., w_{n}) = ω_{λ}(a_{1}^{Φ}(w_{1}, ..., w_{n}), ..., a_{n_{λ}}^{Φ}(w_{1}, ..., w_{n}))

であり、 v ∈ V al は vx_{l} = w_{l} (l ∈ {i_{1}, ..., i_{s}}) をみたすものだったので、 i = 1, 2, ..., n_{λ} に対して、 (a_{i}^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{n}) = (Φ^{∗}a_{i})v となる。ゆえに

(ω_{λ} ∘ (a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})))(w_{1}, ..., w_{n}) = ω_{λ}((Φ^{∗}a_{1})v, ..., (Φ^{∗}a_{n_{λ}})v)

従って、 a^{Φ}(x_{1}, ..., x_{n}) = ω_{λ} ∘ (a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})) が成立する。

q.e.d.

2 の証明

(1) を示す

F var^{b} ⊆ F var^{a} ∪ V ar^{λ}  (∵命題 3.1.1)
= F var^{a} ∪ {y_{1}, ..., y_{m}}  (∵λ = ...y_{1}......y_{m}...)
⊆ {x_{1}, ..., x_{n}} ∪ {y_{1}, ..., y_{m}} (∵ x_{1}, ..., x_{n} は a の自由変数列)
= {x_{1}, ..., x_{n}, y_{1}, ..., y_{m}}

より、 x_{1}, ..., x_{n}, y_{1}, ..., y_{m} は b の自由変数列であることがわかる。

(2) を示す (�) b^{Φ}(w_{1}, ..., w_{n}, □, ..., □) ∈ Dom λ_{W} であること。 b^{Φ}(w_{1}, ..., w_{n}, □, ..., □) ∈ W_{σy_{1}} → (... → (W_{σy_{m}} → W_{σb})...) より、 W_{σy_{1}} → (... → (W_{σy_{m}} → W_{σb})...) ⊆ Dom λ_{W} を示せばよい。今、 b ∈ Dom λ であり、 σ は A から T への準写なので、 σb が T の可変子 λ の Dom に属する。従って、 W_{σy_{1}} → (... → (W_{σy_{m}} → W_{σb})...) ⊆ Dom λ_{W} が成立する。

(�) a^{Φ}(w_{1}, ..., w_{n}) = λ_{W} (b^{Φ}(w_{1}, ..., w_{n}, □, ..., □)) I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とし、 v ∈ V al を vx_{l} = w_{l} (l ∈ {i_{1}, ..., i_{s}}) なるものとすると

a^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}a)v  (∵表現関数の定義)
= (Φ^{∗}(λb))v (∵ a = λb)
= (λ(Φ^{∗}b))v (∵Φ^{∗} は A から W^{V al} への準写)

となる。このとき、可変子 λ に対応する W^{V al} 上の算法の定義より、

(λ(Φ^{∗}b))v = λ_{W} ((Φ^{∗}b)((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v))

が成立する。従って、 a^{Φ}(w_{1}, ..., w_{n}) = λ_{W} (b^{Φ}(w_{1}, ..., w_{n}, □, ..., □)) を示すためには、

(Φ^{∗}b)((\frac{y_{m}}{□})…(\frac{y_{1}}{□})v)= b^{Φ}(w_{1}, ..., w_{n}, □, ..., □)

を示せばよい。つまり、 u_{j} ∈ W_{σy_{j}} (j = 1, ..., m) に対して、

(Φ^{∗}b)((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)= b^{Φ}(w_{1}, ..., w_{n}, u_{1}, ..., u_{m}) ……�

を示す。便宜上 x_{1}, ..., x_{n}, y_{1}, ..., y_{m} を p_{1}, ..., p_{n+m} とおく。つまり、 i = 1, 2, ..., n + m に対して

p_{i} = \{ \begin{matrix}x_{i} & (if 1 ≤ i ≤ n) \\ y_{(i−n)} & (if n + 1 ≤ i ≤ n + m) \end{matrix}

とする。同様に、 w_{1}, ..., w_{n}, u_{1}, ..., u_{m} を q_{1}, ..., q_{n+m} とおく。このとき、 I(p_{1}, ..., p_{n+m}) = j_{1}, ..., j_{t} (t = m(p_{1}, ..., p_{n+m})) とし、 v′ ∈ V al を v′p_{l} = q_{l} (l ∈ {j_{1}, ..., j_{t}}) とすると、

b^{Φ}(w_{1}, ..., w_{n}, u_{1}, ..., u_{m}) = b^{Φ}(q_{1}, ..., q_{n+m}) = (Φ^{∗}b)v′

となるので、�を示すには以下の等式を示せばよい

(Φ^{∗}b)((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)= (Φ^{∗}b)v′

そこで、これを定理 4.1.1 (意味写像定理) を用いて示す。今 F var^{b} ⊆ {x_{1}, ..., x_{n}, y_{1}, ..., y_{m}} = {p_{1}, ..., p_{n+m}} = {p_{j_{1}}, ..., p_{j_{t}}} より、 z ∈ F var^{b} ならば z = p_{h} なる h ∈ {j_{1}, ..., j_{t}} が存在する。 • h ≤ n のとき h は I(p_{1}, ..., p_{n+m}) に現れるので、命題 2.1.1 から p_{h} ∉ {p_{h+1}, ..., p_{n+m}} が成立する。さらに、 h ≤ n より p_{1}, ..., p_{n+m} の決め方から、 p_{h} ∉ {x_{h+1}, ..., x_{n}, y_{1}, ..., y_{m}} となる。従って、 z = p_{h} ∉ {y_{1}, ..., y_{m}} より、

((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)z = vz

が成立する。また、 h ≤ n より p_{h} = x_{h} で、 p_{h} ∉ {x_{h+1}, ..., x_{n}, y_{1}, ..., y_{m}} より x_{h} ∉ {x_{h+1}, ..., x_{n}} が成立する。従って、命題 2.1.1 より h は I(x_{1}, ..., x_{n}) に現れることがわかる。ゆえに v の定義から vx_{h} = w_{h} となる。このことに注意して以下の式変形で ((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)z = v′z がわかる。

((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)z = vz
= vx_{h} (∵ z = p_{h} = x_{h})
= w_{h} (∵ h ∈ {i_{1}, ..., i_{s}} より v の定義)
= q_{h} (∵h ≤ n より q_{1}, ..., q_{n+m} の決め方)
= v′p_{h} (∵ h ∈ {j_{1}, ..., j_{t}} より v′の定義)
= v′z

• h > n のとき h は I(p_{1}, ..., p_{n+m}) に現れるので、命題 2.1.1 より p_{h} ∉ {p_{h+1}, ..., p_{n+m}} となる。そして、 h > n より p_{1}, ..., p_{n+m} の決め方から、 p_{h} ∉ {y_{(h+1−n)}, ..., y_{m}} が成立する。また p_{h} = y_{(h−n)} なので、 y_{(h−n)} ∉ {y_{(h+1−n)}, ..., y_{m}} となり命題 2.1.1 から h − n は I(y_{1}, ..., y_{m}) に現れることがわかる。このとき

((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)z = ((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)y_{(h−n)}
= u_{(h−n)}  (∵命題 3.3.1)
= q_{h}  (∵h > n より q_{1}, ..., q_{n+m} の決め方)
= v′p_{h}  (∵ h ∈ {j_{1}, ..., j_{t}} より v′の定義)
= v′z

より、 ((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)z = v′z

従って、定理 4.1.1 (意味写像定理) により

(Φ^{∗}b)((\frac{y_{m}}{u_{m}} )…(\frac{y_{1}}{u_{1}} )v)= (Φ^{∗}b)v′

が成立する。

q.e.d.

次に、修飾変数条件、可変子条件、意味条件を定義する。 (A, T, σ, P rm) が修飾変数条件をみたすとは、任意の t ∈ T に対して、 Qvar_{t} が空集合か可算個の元を含むことをいう (A, T, σ, P rm) が可変子条件をみたすとは、任意の可変子の修飾変数を Qvar の勝手な元に変えたものも可変子になることをいう二つの可変子 λ = a_{1}a_{2}...a_{n}, λ′ = b_{1}b_{2}...b_{m} (a_{i}, b_{j} ∈ Γ ⨿ V ar) が同類であるとは、以下の三条件をみたすことをいう。

\{ \begin{matrix}• n = m \\ • a_{i} ∈ Γ ⇒ b_{i} ∈ Γ, a_{i} = b_{i} \\ • a_{i} ∈ V ar ⇒ b_{i} ∈ V ar, σa_{i} = σb_{i} \end{matrix}

また、 (A, T, σ, P rm) , W が意味条件をみたすとは、同類の可変子の W 上での意味が等しいことをいう。

命題 4.3.1 a を A の元とし、 λ と λ′ を同類の T の可変子とする。そして、意味条件を仮定し、 σa ∈ Dom λ とすると、 σa ∈ Dom λ′ が成立する。

証明

λ = ...y_{1}......y_{m}... とし、その Dom を D_{λ} とする。同様に λ′ = ...y1^{′}......ym^{′}... で、その Dom を D_{λ′}

とする。このとき、意味条件より λ と λ′ の W 上での意味が等しいので、 Dom λ_{W} = Dom λW^{′} となる。従って、

⋃_{d∈D_{λ}}(W_{σy_{1}} → (... → (W_{σy_{m}} → W_{d})...))= ⋃_{d′ ∈D_{λ′}} (W_{σy′_{1}} → (... → (W_{σy′_{m}} → W_{d′})...))……�

が成立する。また仮定から σa ∈ D_{λ} より、

W_{σy_{1}} → (... → (W_{σy_{m}} → W_{σa})...) ⊆ ⋃_{d∈D_{λ}}(W_{σy_{1}} → (... → (W_{σy_{m}} → W_{d})...))

となる。このとき、注意 3.3.1 から W_{σy_{i}} ≠ ∅ (i = 1, 2, ..., n), W_{σa} ≠ ∅ より、

W_{σy_{1}} → (... → (W_{σy_{m}} → W_{σa})...) ≠ ∅

となる。そこで、存在の保証された W_{σy_{1}} → (... → (W_{σy_{m}} → W_{σa})...) の元を f とする。このとき、�より、

f ∈ ⋃_{d′ ∈D_{λ′}} (W_{σy′_{1}} → (... → (W_{σy′_{m}} → W_{d′})...))

となるので、 f ∈ W_{σy′_{1}} → (... → (W_{σy′_{m}} → W_{d′})...) なる d′ ∈ D_{λ′} が存在する。さらに、 λ と λ′ は同類より、 i = 1, 2, ..., m に対して、 W_{σy_{i}} = W_{σy′_{i}} なので u_{i} ∈ W_{σy_{i}} (i = 1, 2, ..., m) とすれば、 (...(fu_{1})...)u_{m} ∈ W_{σa} ∩ W_{d′} となる。従って W_{σa} ∩ W_{d′} ≠ ∅ より、 σa = d′ となる。つまり、 σa ∈ D_{λ′} が成立する。

q.e.d.

補題 4.3.3 a_{1}, ..., a_{m} ∈ A、 B ⊆ A とし、 x_{1}, ..., x_{n} を任意の b ∈ B の自由変数列、 C を A の有限部分集合とする。そして、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とする。このとき、修飾変数条件を仮定すると以下のことが成立する。 ∃ y_{1}, ..., y_{n} ∈ V ar s.t. 以下の七条件をみたす。

1. y_{i} は x_{i} と同型 (i = 1, 2, ..., n)

2. a_{k} において任意の s ∈ P rm は b(\frac{x_{1}, ..., x_{n}}{y_{1}, ..., y_{n}} ) から自由 (k = 1, 2, ..., m b ∈ B)

3. I(y_{1}, ..., y_{n}) = j_{1}, ..., j_{t} (t = m(y_{1}, ..., y_{n})) とすれば、 {i_{1}, ..., i_{s}} ⊆ {j_{1}, ..., j_{t}}

4. x_{i} ∈ Qvar なる i に対して、 y_{i} ∈ Qvar

5. ({y_{1}, ..., y_{n}} ∩ Qvar) ∩ C = ∅

6. x_{i}, x_{i′} ∈ Qvar なる i, i′ に対して、 i ≠ i′ ならば、 y_{i} ≠ y_{i′}

7. x_{i} ∈ Qvar なる i に対して、 a_{k} において任意の s ∈ P rm は y_{i} から自由 (k = 1, 2, ..., m)

証明定理 2.2.2 を用いて示す。そのために、定理 2.2.2 の仮定をみたすことを示す。

• P rm_{F}^{b} ∩ P rm^{Λ} ⊆ {x_{1}, ..., x_{n}} (∀ b ∈ B) が成立すること

P rm_{F}^{b} ∩ P rm^{Λ} = P rm_{F}^{b} ∩ Qvar (∵命題 3.1.1 よりQvar = P rm^{Λ})
= Qvar_{F}^{b}
⊆ F var^{b}  (∵ Qvar ⊆ V ar)
⊆ {x_{1}, ..., x_{n}}  (∵ x_{1}, ..., x_{n}は b ∈ B の自由変数列)

より成立する。

• {x_{1}, ..., x_{n}}_{t} ∩ P rm^{Λ} ≠ ∅ なる t ∈ T に対して、 P rm_{t} ∩ P rm^{Λ} が可算個の元を含むこと t ∈ T を {x_{1}, ..., x_{n}}_{t} ∩ P rm^{Λ} ≠ ∅ なるものとすると

{x_{1}, ..., x_{n}}_{t} ∩ P rm^{Λ} ⊆ P rm_{t} ∩ P rm^{Λ} (∵ {x_{1}, ..., x_{n}} ⊆ P rm)
= P rm_{t} ∩ Qvar (∵命題 3.1.1)
= Qvar_{t}

より、 Qvar_{t} ≠ ∅ となる。従って修飾変数条件から、 Qvar_{t} は可算個の元を含む。そして、 Qvar_{t} = P rm_{t} ∩ P rm^{Λ} より P rm_{t} ∩ P rm^{Λ} が可算個の元を含むことがわかる。

従って、定理 2.2.2 より、以下の七条件をみたす y_{1}, ..., y_{n} ∈ P rm^{Λ} ∪ ({x_{1}, ..., x_{n}} − P rm^{Λ}) が存在する。

1. y_{i} は x_{i} と同型 (i = 1, 2, ..., n)

2. a_{k} において任意の s ∈ P rm は b(\frac{x_{1}, ..., x_{n}}{y_{1}, ..., y_{n}} ) から自由 (k = 1, 2, ..., m b ∈ B)

3. I(y_{1}, ..., y_{n}) = j_{1}, ..., j_{t} (t = m(y_{1}, ..., y_{n})) とすれば、 {i_{1}, ..., i_{s}} ⊆ {j_{1}, ..., j_{t}}

4. x_{i} ∈ P rm^{Λ} なる i に対して、 y_{i} ∈ P rm^{Λ}

5. ({y_{1}, ..., y_{n}} ∩ P rm^{Λ}) ∩ C = ∅

6. x_{i}, x_{i′} ∈ P rm^{Λ} なる i, i′ に対して、 i ≠ i′ ならば、 y_{i} ≠ y_{i′}

7. x_{i} ∈ P rm^{Λ} なる i に対して、 a_{k} において任意の s ∈ P rm は y_{i} から自由 (k = 1, 2, ..., m)

このとき、命題 3.1.1 より P rm^{Λ} = Qvar で、

P rm^{Λ} ∪ ({x_{1}, ..., x_{n}} − P rm^{Λ}) ⊆ Qvar ∪ V ar
= V ar

より

1. y_{i} は x_{i} と同型 (i = 1, 2, ..., n)

2. a_{k} において任意の s ∈ P rm は b(\frac{x_{1}, ..., x_{n}}{y_{1}, ..., y_{n}} ) から自由 (k = 1, 2, ..., m b ∈ B)

3. I(y_{1}, ..., y_{n}) = j_{1}, ..., j_{t} (t = m(y_{1}, ..., y_{n})) とすれば、 {i_{1}, ..., i_{s}} ⊆ {j_{1}, ..., j_{t}}

4. x_{i} ∈ Qvar なる i に対して、 y_{i} ∈ Qvar

5. ({y_{1}, ..., y_{n}} ∩ Qvar) ∩ C = ∅

6. x_{i}, x_{i′} ∈ Qvar なる i, i′ に対して、 i ≠ i′ ならば、 y_{i} ≠ y_{i′}

7. x_{i} ∈ Qvar なる i に対して、 a_{k} において任意の s ∈ P rm は y_{i} から自由 (k = 1, 2, ..., m) をみたす、 y_{1}, ..., y_{n} ∈ V ar が存在することがわかる。

q.e.d.

系 1 a_{1}, ..., a_{m} ∈ A とし、 x_{1}, ..., x_{n} ∈ V ar で、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とする。さらに、 C を A の有限部分集合とし、修飾変数条件を仮定すると以下が成立する。 ∃ y_{1}, ..., y_{n} ∈ V ar s.t. 以下の七条件をみたす。

1. y_{i} は x_{i} と同型 (i = 1, 2, ..., n)

2. a_{k} において任意の s ∈ P rm は y_{l} から自由 (k = 1, 2, ..., m , l ∈ {i_{1}, ..., i_{s}})

3. I(y_{1}, ..., y_{n}) = j_{1}, ..., j_{t} (t = m(y_{1}, ..., y_{n})) とすれば、 {i_{1}, ..., i_{s}} ⊆ {j_{1}, ..., j_{t}}

4. x_{i} ∈ Qvar なる i に対して、 y_{i} ∈ Qvar

5. ({y_{1}, ..., y_{n}} ∩ Qvar) ∩ C = ∅

6. x_{i}, x_{i′} ∈ Qvar なる i, i′ に対して、 i ≠ i′ ならば、 y_{i} ≠ y_{i′}

7. x_{i} ∈ Qvar なる i に対して、 a_{k} において任意の s ∈ P rm は y_{i} から自由 (k = 1, 2, ..., m)

証明補題 4.3.3 において、 B = {x_{1}, ..., x_{n}} とすると、 x_{j} ∈ B に対して F var^{x_{j}} = {x_{j}} ⊆ {x_{1}, ..., x_{n}} より、補題 4.3.3 の仮定をみたす。従って、以下の七条件をみたす y_{1}, ..., y_{n} ∈ V ar が存在する。 1′. y_{i} は x_{i} と同型 (i = 1, 2, ..., n)

2′. a_{k} において任意の s ∈ P rm は x_{j}(\frac{x_{1}, ..., x_{n}}{y_{1}, ..., y_{n}} ) から自由 (k = 1, 2, ..., m x_{j} ∈ B)

3′. I(y_{1}, ..., y_{n}) = j_{1}, ..., j_{t} (t = m(y_{1}, ..., y_{n})) とすれば、 {i_{1}, ..., i_{s}} ⊆ {j_{1}, ..., j_{t}} 4′. x_{i} ∈ Qvar なる i に対して、 y_{i} ∈ Qvar 5′. ({y_{1}, ..., y_{n}} ∩ Qvar) ∩ C = ∅ 6′. x_{i}, x_{i′} ∈ Qvar なる i, i′ に対して、 i ≠ i′ ならば、 y_{i} ≠ y_{i′} 7′. x_{i} ∈ Qvar なる i に対して、 a_{k} において任意の s ∈ P rm は y_{i} から自由 (k = 1, 2, ..., m)

このとき、条件 1, 3, ..., 7 は条件 1′, 3′, ..., 7′ と同じなので、題意を示すためには 2 が成立することを示せばよい。そこで、 l ∈ {i_{1}, ..., i_{s}} とする。このとき 2′ の x_{j} ∈ B として、 x_{l} をとると、代入の定義より

x_{l}(\frac{x_{1}, ..., x_{n}}{y_{1}, ..., y_{n}} ) = x_{l}(\frac{x_{i_{1}}, ..., x_{i_{s}}}{y_{i_{1}}, ..., y_{i_{s}}} ) = y_{l}

となる。従って、 a_{k} において任意の s ∈ P rm は y_{l} から自由 (k = 1, 2, ..., m , l ∈ {i_{1}, ..., i_{s}}) が成立する。

q.e.d.

以下、修飾変数条件、可変子条件、意味条件をみたす形式言語を考える。そして型関数の部分集合 T F^{Φ}, P F^{Φ} を以下のように定める。

T F^{Φ} = {a^{Φ}(x_{1}, ..., x_{n}) | a ∈ A, x_{1}, ..., x_{n} は a の自由変数列}
P F^{Φ} = {(σx_{1}, ..., σx_{n})/w | x_{1}, ..., x_{n} は変数列, w ∈ Φ(Con)}
∪ {(σx_{1}, ..., σx_{n}) ↓ i | x_{1}, ..., x_{n} は変数列, i は I(x_{1}, ..., x_{n}) に現れる}

次に T F^{Φ} 上に算法を定義する。 (�) λ ∈ Λ′(不変子) から作られる算法 n_{λ} を λ の項数とする。まず、この算法の Dom を以下の条件をみたす T F^{Φ} の組 (a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}})) とする。

\{ \begin{matrix}• k, k′ ∈ \{1, 2, ..., n_{λ}\}, i ∈ \{1, 2, ..., n\} に対して、 x_{i}^{k}と x_{i}^{k′} は同型 \\ • W_{σa_{1}}×…× W_{σa_{n_{λ}}} ⊆ Dom ω_{λ} \\ • k, k′ ∈ \{1, 2, ..., n_{λ}\} に対して、 I(x_{1}^{k}, ..., x_{n}^{k}) = I(x_{1}^{k′} , ..., x_{n}^{k′}) \end{matrix}

次に、この算法の作用を定義する。 ( k, k′ ∈ {1, 2, ..., n_{λ}}, i ∈ {1, 2, ..., n} に対して、 x_{i}^{k}と x_{i}^{k′} は同型なので、 t_{i} = σx_{i}^{k} = σx_{i}^{k′} とおく。 ) λ(a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}}))∈ W_{t_{1}}×…× W_{t_{n}} → W_{λ(σa_{1},...,σa_{n_{λ}})} を以下のように定義する。 (w_{1}, ..., w_{n}) ∈ W_{t_{1}}×…× W_{t_{n}} に対して

\begin{matrix}(λ(a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}})))(w_{1}, ..., w_{n}) \\ = & (ω_{λ} ∘ (a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}})))(w_{1}, ..., w_{n}) \end{matrix}

とする。このとき、右辺が定義できることは (a_{1}^{Φ}(w_{1}, ..., w_{n}), ..., a_{n_{λ}}^{Φ}(w_{1}, ..., w_{n}))∈ W_{σa_{1}}×…× W_{σa_{n_{λ}}} ⊆ Dom ω_{λ} よりわかる。

(�) T の可変子 λ( = ...y_{1}......y_{m}...) から作られる算法まず、この算法の Dom を以下の条件をみたす T F^{Φ} の元 b^{Φ}(x_{1}, ..., x_{n+m}) の集合とする。

\{ \begin{matrix}• σb ∈ Dom λ \\ • σy_{j} = σx_{n+j} (j = 1, 2, ..., m) \end{matrix}

次に、この算法の作用を定義する。 ♭_{λ}(b^{Φ}(x_{1}, ..., x_{n+m}))∈ W_{σx_{1}}×…× W_{σx_{n}} → W_{λσb} を以下のように定義する。 (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} に対して

(♭_{λ}(b^{Φ}(x_{1}, ..., x_{n+m})))(w_{1}, ..., w_{n}) = λ_{W} (b^{Φ}(w_{1}, ..., w_{n}, □, ..., □))

とする。次に、右辺が定義できることを示す。 b^{Φ}(w_{1}, ..., w_{n}, □, ..., □) ∈ W_{σx_{i+1}} → (... → (W_{σx_{n}} → W_{σb})...) で、 σy_{j} = σx_{n+j} (j = 1, 2, ..., m) より、 b^{Φ}(w_{1}, ..., w_{n}, □, ..., □) ∈ W_{σy_{1}} → (... → (W_{σy_{m}} → W_{σb})...) となる。さらに、 σb ∈ Dom λ より、 λ_{W} の定義から、 b^{Φ}(w_{1}, ..., w_{n}, □, ..., □) ∈ Dom λ_{W} が成立する。従って、右辺を定義することができる。

また λ が空算法なら、 Dom λ = ∅ より Dom ♭_{λ} = ∅ となる。従って、 ♭_{λ} は空算法となる。

最後に、これらの算法が T F^{Φ} 上の算法であることを確かめる。

• 不変子から作られる算法が T F^{Φ} 上の算法であること (a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}})) を不変子から作られる算法の Dom とする。 I(x_{1}^{1}, ..., x_{n}^{1}) = j_{1}, ..., j_{u} (u = m(x_{1}^{1}, ..., x_{n}^{1})) とすれば、 Dom の定義より、 k, k′ ∈ {1, 2, ..., n_{λ}} に対して、 I(x_{1}^{k}, ..., x_{n}^{k}) = I(x_{1}^{k′} , ..., x_{n}^{k′}) なので、任意の k ∈ {1, 2, ..., n_{λ}} に対して、 I(x_{1}^{k}, ..., x_{n}^{k}) = j_{1}, ..., j_{u} となる。また、 k , k′ ∈ {1, 2, ..., n_{λ}}, i ∈ {1, 2, ..., n} に対して、 x_{i}^{k} と x_{i}^{k′} は同型なので、 t_{i} = σx_{i}^{k} = σx_{i}^{k′} とおく。このとき、不変子から作られる算法が T F^{Φ} 上の算法であることを示すためには、

λ(a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}}))= a^{Φ}(x_{1}, ..., x_{n})

をみたす a ∈ A とその自由変数列 x_{1}, ..., x_{n} が存在することを示せばよい。

(�) x_{1}, ..., x_{n} を決める。今、修飾変数条件が仮定されているので、 a_{1}, ..., a_{n_{λ}} ∈ A, x_{1}^{1}, ..., x_{n}^{1} ∈ V ar, C = ∅ に補題 4.3.3 系 1 を用いると以下が成立する。 ∃ x_{1}, ..., x_{n} ∈ V ar s.t. 以下の七条件をみたす。

1. x_{i} は x_{i}^{1} と同型 (i = 1, 2, ..., n)

2. a_{k} において任意の s ∈ P rm は x_{l} から自由 (k = 1, 2, ..., n_{λ} , l ∈ {j_{1}, ..., j_{u}})

3. I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とすれば、 {j_{1}, ..., j_{u}} ⊆ {i_{1}, ..., i_{s}}

4. x_{i}^{1} ∈ Qvar なる i に対して、 x_{i} ∈ Qvar

5. ({x_{1}, ..., x_{n}} ∩ Qvar) ∩ ∅ = ∅

6. x_{i}^{1}, x_{i′}^{1} ∈ Qvar なる i, i′ に対して、 i ≠ i′ ならば、 x_{i} ≠ x_{i′}

7. x_{i}^{1} ∈ Qvar なる i に対して、 a_{k} において任意の s ∈ P rm は x_{i} から自由 (k = 1, 2, ..., n_{λ}) となる。そこで、この変数列 x_{1}, ..., x_{n} を使う。

(�) a を決める。 i = 1, 2, ..., n と k = 1, 2, ..., n_{λ} に対して、 1. より x_{i}^{1} と x_{i} は同型で、仮定より x_{i}^{k} と x_{i}^{1} は同型な

ので、 x_{i} と x_{i}^{k} が同型となる。従って、 k = 1, 2, ..., n_{λ} に対して、代入 (\frac{x_{1}^{k}, ..., x_{n}^{k}}{x_{1}, ..., x_{n}} ) を定義するこ

とができる。そこで、 k = 1, 2, ..., n_{λ} に対して、

b_{k} = a_{k}(\frac{x_{1}^{k}, ..., x_{n}^{k}}{x_{1}, ..., x_{n}} )

と定め、 a ∈ A を

a = α_{λ}(b_{1}, ..., b_{n_{λ}})

とする。注 ( α_{λ}(b_{1}, ..., b_{n_{λ}}) を定義することができること) W_{σa_{1}}×…× W_{σa_{n_{λ}}} ⊆ Dom ω_{λ} なので、補題 4.3.1 を用いると (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ} が成立する。従って、準写 σ の定義より (σa_{1}, ..., σa_{n_{λ}}) ∈ Dom λ となる。また、代入は型を保つので、 (σa_{1}, ..., σa_{n_{λ}}) = (σb_{1}, ..., σb_{n_{λ}}) となり、 (σb_{1}, ..., σb_{n_{λ}}) ∈ Dom λ が成立する。ゆえに、準写 σ の定義より (b_{1}, ..., b_{n_{λ}}) ∈ Dom α_{λ} となる。

(�) x_{1}, ..., x_{n} が a の自由変数列であることまず k = 1, 2, ..., n_{λ} に対して、 x_{1}, ..., x_{n} が b_{k} の自由変数列であることを示す。 x_{1}^{k}, ..., x_{n}^{k} は a_{k} の自由変数列で、 x_{i}^{k} と x_{i} は同型である。さらに、任意の k ∈ {1, 2, ..., n_{λ}} に対して I(x_{1}^{k}, ..., x_{n}^{k}) = j_{1}, ..., j_{u} であり {j_{1}, ..., j_{u}} ⊆ {i_{1}, ..., i_{s}} が成り立っている。このとき、定理 4.2.2

系 1 を用いると b_{k} = a_{k}(\frac{x_{1}^{k}, ..., x_{n}^{k}}{x_{1}, ..., x_{n}} ) に対して、以下のことが成立する。

(1) x_{1}, ..., x_{n} は b_{k} の自由変数列

(2) a_{k} において x_{l}^{k} が x_{l} から自由 (l ∈ {j_{1}, ..., j_{u}}) ならば b_{k}^{Φ}(x_{1}, ..., x_{n}) = a_{k}^{Φ}(x_{1}^{k}, ..., x_{n}^{k}) ゆえに、 x_{1}, ..., x_{n} が b_{k} の自由変数列であることがわかる。

次に、 x_{1}, ..., x_{n} が a の自由変数列であることを示す。 a = α_{λ}(b_{1}, ..., b_{n_{λ}}) で λ は不変子より命題 3.1.1 から、 F var^{a} = ⋃_{k=1}^{n_{λ}} F var^{b_{k}} となる。そして、 x_{1}, ..., x_{n} が b_{k} の自由変数列であることから、 F var^{a} = ⋃_{k=1}^{n_{λ}} F var^{b_{k}} ⊆ {x_{1}, ..., x_{n}} が成立する。従って、 x_{1}, ..., x_{n} が a の自由変数列であることがわかる。

(�) λ(a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}}))= a^{Φ}(x_{1}, ..., x_{n}) 準備として、以下の二つの等式を示す。

\begin{aligned}� & b_{k}^{Φ}(x_{1}, ..., x_{n}) & = & a_{k}^{Φ}(x_{1}^{k}, ..., x_{n}^{k}) (k = 1, 2, ..., n_{λ}) \\ � & a^{Φ}(x_{1}, ..., x_{n}) & = & ω_{λ} ∘ (b_{1}^{Φ}(x_{1}, ..., x_{n}), ..., b_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})) \end{aligned}

�が成立すること。 a_{k} において x_{l}^{k} が x_{l} から自由 (l ∈ {j_{1}, ..., j_{u}}) であることが示せれば、 (2) より�が成立することがわかる。今、 2. より a_{k} において、任意の s ∈ P rm は x_{l} から自由 (k = 1, 2, ..., n_{λ} , l ∈ {j_{1}, ..., j_{u}}) が成立しているので、 s として x_{l}^{k} をとればよい。

�が成立すること。 x_{1}, ..., x_{n} が a の自由変数列であり、 a = α_{λ}(b_{1}, ..., b_{n_{λ}}) で、 λ は不変子より補題 4.3.2 を用いると a^{Φ}(x_{1}, ..., x_{n}) = ω_{λ} ∘ (b_{1}^{Φ}(x_{1}, ..., x_{n}), ..., b_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})) が成立する。

最後に、 λ(a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}}))= a^{Φ}(x_{1}, ..., x_{n}) を示す。 (w_{1}, ..., w_{n}) ∈ W_{t_{1}}×… × W_{t_{n}} に対して、

(λ(a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}})))(w_{1}, ..., w_{n})

= (ω_{λ} ∘ (a_{1}^{Φ}(x_{1}^{1}, ..., x_{n}^{1}), ..., a_{n_{λ}}^{Φ}(x_{1}^{n_{λ}}, ..., x_{n}^{n_{λ}})))(w_{1}, ..., w_{n})
= (ω_{λ} ∘ (b_{1}^{Φ}(x_{1}, ..., x_{n}), ..., b_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})))(w_{1}, ..., w_{n})  (∵�)
= a^{Φ}(w_{1}, ..., w_{n})  (∵�)

以上より、不変子から作られる算法が T F^{Φ} 上の算法であることがわかる。

• 可変子から作られる算法が T F^{Φ} 上の算法であること λ = ...y_{1}......y_{m}... を T の可変子とし、 b^{Φ}(x_{1}, ..., x_{n+m}) ∈ Dom ♭_{λ} とする。このとき、 ♭_{λ} が T F^{Φ} 上の算法であることを示すためには、

♭_{λ}(b^{Φ}(x_{1}, ..., x_{n+m}))= a^{Φ}(z_{1}, ..., z_{n})

なる a ∈ A とその自由変数列 z_{1}, ..., z_{n} が存在することを示せばよい。

(�) z_{1}, ..., z_{n} を決める。 z_{1}, ..., z_{n} として、 x_{1}, ..., x_{n} をとる。

(�) a を決める。今、修飾変数条件が満たされているので、 b ∈ A, y_{1}, ..., y_{m} ∈ V ar, I(y_{1}, ..., y_{m}) = j_{1}, ..., j_{u} (u = m(y_{1}, ..., y_{m})), A の有限部分集合 {x_{1}, ..., x_{n}} に対して、補題 4.3.3 系 1 を用いると以下が成立する。

∃ y1^{′}, ..., ym^{′} ∈ V ar s.t. 以下の七条件をみたす。

1. yj^{′} は y_{j} と同型 (j = 1, ..., m)

2. b において任意の s ∈ P rm は yl^{′} から自由 (l ∈ {j_{1}, ..., j_{u}})

3. I(y1^{′}, ..., ym^{′}) = j1^{′}, ..., ju′^{′} (u′ = m(y1^{′}, ..., ym^{′})) とすると、 {j_{1}, ..., j_{u}} ⊆ {j1^{′}, ..., ju′^{′} }

4. y_{j} ∈ Qvar なる j に対して、 yj^{′} ∈ Qvar

5. ({y1^{′}, ..., ym^{′}} ∩ Qvar) ∩ {x_{1}, ..., x_{n}} = ∅

6. y_{j}, y_{j′} ∈ Qvar なる j, j′ に対して、 j ≠ j′ ならば、 yj^{′} ≠ yj′^{′}

7. y_{j} ∈ Qvar なる j に対して、 b において任意の s ∈ P rm は yj^{′} から自由

さらに、 λ = ...y_{1}......y_{m}... なので、 {y_{1}, ..., y_{m}} ⊆ Qvar が成立する。従って、条件 4,6,7 は

4. yj^{′} ∈ Qvar (j = 1, ..., m)

6. y1^{′}, ..., ym^{′} は相異なる列

7. b において任意の s ∈ P rm は yj^{′} から自由 (j = 1, ..., m)

となる。

そして、条件 4 より条件 5 は、 {y1^{′}, ..., ym^{′}} ∩ {x_{1}, ..., x_{n}} = ∅ となる。

このとき、 z1^{′}, ..., zn+m^{′} を以下のように定義する。

zi^{′} = \{ \begin{matrix}x_{i} & (if 1 ≤ i ≤ n) \\ yi−n^{′} & (if n + 1 ≤ i ≤ n + m) \end{matrix}

次に、代入 (\frac{x_{1}, ..., x_{n+m}}{z1^{′}, ..., zn+m^{′}} ) を定義したいので、 x_{i} と zi^{′} が同型であることを示す。

1 ≤ i ≤ n のときは、 zi^{′} の定義より zi^{′} = x_{i} なので x_{i} と zi^{′} は同型である。 n + 1 ≤ i ≤ n + m のときは、 zi^{′} の定義より zi^{′} = yi−n^{′} であり、 1 より yi−n^{′} と y_{i−n} は同型で、仮定より σy_{i−n} = σx_{i} なので、 x_{i} と zi^{′} が同型であることがわかる。従って、代入を定義することができる。そこで、 c ∈ A を、

c = b(\frac{x_{1}, ..., x_{n+m}}{z1^{′}, ..., zn+m^{′}} )

と定める。このとき、 4 より、 y1^{′}, ..., ym^{′} ∈ Qvar なので、 λ の修飾変数列 y_{1}, ..., y_{m} を y1^{′}, ..., ym^{′} に

変えたものを λ′ とすれば、可変子条件から λ′ ∈ Λ となる。 ( λ′ は可変子である。 ) そこで、

a = λ′c

と定める。

注 (c ∈ Dom λ′であること) λ′ の作り方と、 1 より y_{j} と yj^{′} は同型 (j = 1, ..., m) なので、 λ と λ′ は同類の可変子である。さらに、意味条件が仮定され、 σb ∈ Dom λ なので命題 4.3.1 を用いると、 σb ∈ Dom λ′ となる。このとき、代入は型を保つから σc = σb ∈ Dom λ′ が成立する。従って、 c ∈ Dom λ′

(�) z_{1}, ..., z_{n} が a の自由変数列であることまず、 z1^{′}, ..., zn+m^{′} が c の自由変数列であることを定理 4.2.2 系 1 を用いて示す。

b ∈ A, x_{1}, ..., x_{n+m} は b の自由変数列, z1^{′}, ..., zn+m^{′} ∈ V ar, h = 1, 2, ..., n + m に対して、 x_{h} と zh^{′}

が同型であることがわかっているので、 I(x_{1}, ..., x_{n+m}) に現れる任意の元 i が I(z1^{′}, ..., zn+m^{′}) に現れることを示せば、定理 4.2.2 系 1 の仮定をみたすことがわかる。そこで、 I(x_{1}, ..., x_{n+m}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n+m})) とし i ∈ {i_{1}, ..., i_{s}} とする。

このとき、 zi^{′} ∉ {zi+1^{′}, ..., zn+m^{′}} が成立することを示せば、命題 2.1.1 より i が I(z1^{′}, ..., zn+m^{′}) に

現れることがわかる。

• i ≤ n のとき (zi^{′} = x_{i})

このとき、 {zi+1^{′}, ..., zn+m^{′}} = {x_{i+1}, ..., x_{n}, y1^{′}, ..., ym^{′}} となる。今、 i ∈ {i_{1}, ..., i_{s}} より x_{i} ∉

{x_{i+1}, ..., x_{n+m}} なので、 x_{i} ∉ {x_{i+1}, ..., x_{n}} が成立する。また、 5 より {y1^{′}, ..., ym^{′}}∩{x_{1}, ..., x_{n}} = ∅

なので x_{i} ∉ {y1^{′}, ..., ym^{′}} となる。従って、 zi^{′} = x_{i} ∉ {zi+1^{′}, ..., zn+m^{′}}

• n < i のとき (zi^{′} = yi−n^{′})

このとき、 {zi+1^{′}, ..., zn+m^{′}} = {yi+1−n^{′}, ..., ym^{′}} となる。 6 より y1^{′}, ..., ym^{′} は相異なる列なので、

yi−n^{′} ∉ {yi+1−n^{′}, ..., ym^{′}} が成立する。ゆえに、 zi^{′} = yi−n^{′} ∉ {zi+1^{′}, ..., zn+m^{′}}

従って、定理 4.2.2 系 1 より、

(1) z1^{′}, ..., zn+m^{′} は c の自由変数列

(2) b において x_{i} が z′_{i} から自由 (i ∈ {i_{1}, ..., i_{s}}) ならば

c^{Φ}(z1^{′}, ..., zn+m^{′}) = b^{Φ}(x_{1}, ..., x_{n+m})

が成立する。次に、 z_{1}, ..., z_{n} が a の自由変数列であることを示す。

F var^{a} = P rm_{F}^{a} ∩ V ar

であり、 a = λ′c より定理 1.1.6 を用いると

F var^{a} = (P rm_{F}^{c} − P rm^{λ′}) ∩ V ar = F var^{c} − P rm^{λ′}

となる。また、 λ′ = ...y1^{′}......ym^{′}... より

F var^{a} = F var^{c} − {y1^{′}, ..., ym^{′}}

が成立し、 z1^{′}, ..., zn+m^{′} は c の自由変数列なので

F var^{a} ⊆ {z1^{′}, ..., zn+m^{′}} − {y1^{′}, ..., ym^{′}}

となる。このとき、 z1^{′}, ..., zn+m^{′} のとり方から、

F var^{a} ⊆ {x_{1}, ..., x_{n}, y1^{′}, ..., ym^{′}} − {y1^{′}, ..., ym^{′}}

が成立する。従って、

F var^{a} ⊆ {x_{1}, ..., x_{n}}

となる。さらに、 z_{1}, ..., z_{n} のとり方から、

F var^{a} ⊆ {z_{1}, ..., z_{n}}

が成立する。従って、 z_{1}, ..., z_{n} が a の自由変数列であることがわかる。

(�) ♭_{λ}(b^{Φ}(x_{1}, ..., x_{n+m}))= a^{Φ}(z_{1}, ..., z_{n}) であること準備として、以下の等式を示す。

� λ_{W} = λW^{′}
� (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}}に対して、

(c^{Φ}(z1^{′}, ..., zn+m^{′}))(w_{1}, ..., w_{n}, □, ..., □) = (b^{Φ}(x_{1}, ..., x_{n+m}))(w_{1}, ..., w_{n}, □, ..., □)

� (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}}に対して、

a^{Φ}(w_{1}, ..., w_{n}) = λW^{′} (c^{Φ}(w_{1}, ..., w_{n}, □, ..., □))

�について、 λ と λ′ が同類であるので、意味条件により、 λ_{W} = λW^{′} が成立する。従って�は成立。

�について、

まず、 c^{Φ}(z1^{′}, ..., zn+m^{′}) = b^{Φ}(x_{1}, ..., x_{n+m}) であることを示す。

これは b において x_{i} が z′_{i} から自由 (i ∈ {i_{1}, ..., i_{s}}) ならば (2) より示されるので、それを示す。 i ∈ {i_{1}, ..., i_{s}} に対して、 i ≤ n のとき (zi^{′} = x_{i})、定理 1.1.7 より b において x_{i} は x_{i} から自由である。 n < i のとき (zi^{′} = yi−n^{′})、 7 より b において任意の s ∈ P rm は yi−n^{′} から自由である。従って、 s として x_{i} をとればよい。

ゆえに、 (2) より c^{Φ}(z1^{′}, ..., zn+m^{′}) = b^{Φ}(x_{1}, ..., x_{n+m}) が成立する。

次に�が成立することを示す。 c^{Φ}(z1^{′}, ..., zn+m^{′}) = b^{Φ}(x_{1}, ..., x_{n+m}) に注意して以下の式変形で�が成立することが示せる。 u_{l} ∈ W_{σx_{l}} (l = n + 1, ..., n + m) に対して、

(...(((c^{Φ}(z1^{′}, ..., zn+m^{′}))(w_{1}, ..., w_{n}, □, ..., □))u_{n+1})...)u_{n+m}

= (c^{Φ}(z1^{′}, ..., zn+m^{′}))(w_{1}, ..., w_{n}, u_{n+1}, ..., u_{n+m})
= (b^{Φ}(x_{1}, ..., x_{n+m}))(w_{1}, ..., w_{n}, u_{n+1}, ..., u_{n+m})
= (...(((b^{Φ}(x_{1}, ..., x_{n+m}))(w_{1}, ..., w_{n}, □, ..., □))u_{n+1})...)u_{n+m}

�について、

a = λ′c で、 z_{1}, ..., z_{n} が a の自由変数列であり、 λ′ = ...y1^{′}......ym^{′}... なので補題 4.3.2 より (w_{1}, ..., w_{n}) ∈

W_{σz_{1}}×…× W_{σz_{n}}(= W_{σx_{1}}×…× W_{σx_{n}}) に対して、 a^{Φ}(w_{1}, ..., w_{n}) = λW^{′} (c^{Φ}(w_{1}, ..., w_{n}, □, ..., □

)) が成立する。

最後に、 ♭_{λ}(b^{Φ}(x_{1}, ..., x_{n+m}))= a^{Φ}(z_{1}, ..., z_{n}) であることを示す。 (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} に対して

\begin{aligned}(♭_{λ}(b^{Φ}(x_{1}, ..., x_{n+m})))(w_{1}, ..., w_{n}) & = & λ_{W} (b^{Φ}(w_{1}, ..., w_{n}, □, ..., □)) \\ & = & λW^{′} (b^{Φ}(w_{1}, ..., w_{n}, □, ..., □)) & (∵�) \\ & = & λW^{′} (c^{Φ}(w_{1}, ..., w_{n}, □, ..., □)) & (∵�) \\ & = & a^{Φ}(w_{1}, ..., w_{n}) & (∵�) \end{aligned}

従って、可変子から作られる算法が T F^{Φ} 上の算法であることがわかる。

次に、 P F^{Φ} ⊆ T F^{Φ} であることを示す。

• (σx_{1}, ..., σx_{n})/w (x_{1}, ..., x_{n}は変数列 , w ∈ Φ(Con)) について、 w ∈ Φ(Con) より、 ∃ c ∈ Con s.t. w = Φc となる。このとき、 (σx_{1}, ..., σx_{n})/w = c^{Φ}(x_{1}, ..., x_{n}) であることを示す。

(�) x_{1}, ..., x_{n} が c の自由変数列であること c ∈ Con より P rm_{F}^{c} = {c} が成立し、 c ∉ V ar より、 F var^{c} = ∅ ⊆ {x_{1}, ..., x_{n}} となる。従って成立。

(�) (σx_{1}, ..., σx_{n})/w = c^{Φ}(x_{1}, ..., x_{n}) であること (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} とする。また、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とし、 v ∈ V al を vx_{l} = w_{l} (l ∈ {i_{1}, ..., i_{s}}) なるものとすれば、

c^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}c)v  (∵表現関数の定義)
= Φc  (∵ c ∈ Con)
= w  (∵ w = Φc)
= ((σx_{1}, ..., σx_{n})/w)(w_{1}, ..., w_{n})

従って、 (σx_{1}, ..., σx_{n})/w = c^{Φ}(x_{1}, ..., x_{n}) ∈ T F^{Φ} となる。

• (σx_{1}, ..., σx_{n}) ↓ i ( x_{1}, ..., x_{n} は変数列, i は I(x_{1}, ..., x_{n}) に現れる ) について、このとき、 (σx_{1}, ..., σx_{n}) ↓ i = x_{i}^{Φ}(x_{1}, ..., x_{n}) であることを示す。

(�) x_{1}, ..., x_{n} が x_{i} の自由変数列であること。 x_{i} ∈ V ar より、 F var^{x_{i}} = {x_{i}} であるので、 F var^{x_{i}} ⊆ {x_{1}, ..., x_{n}} となる。従って成立。

(�) (σx_{1}, ..., σx_{n}) ↓ i = x_{i}^{Φ}(x_{1}, ..., x_{n}) であること。 (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} とする。また、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とし、 v ∈ V al を vx_{l} = w_{l} (l ∈ {i_{1}, ..., i_{s}}) なるものとすれば、

x_{i}^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}x_{i})v  (∵表現関数の定義)
= vx_{i}  (∵ x_{i} ∈ V ar)
= w_{i}  (∵i ∈ {i_{1}, ..., i_{s}} より v の定義)
= ((σx_{1}, ..., σx_{n}) ↓ i)(w_{1}, ..., w_{n})

従って、 (σx_{1}, ..., σx_{n}) ↓ i = x_{i}^{Φ}(x_{1}, ..., x_{n}) ∈ T F^{Φ} となる。 ∴ P F^{Φ} ⊆ T F^{Φ}

そこで、 [P F^{Φ}] を T F^{Φ} における P F^{Φ} の算包とする。

定理 4.3.1 [P F^{Φ}] = T F^{Φ}

証明 [P F^{Φ}] ⊆ T F^{Φ} は自明なので、 [P F^{Φ}] ⊇ T F^{Φ} を示せばよい。そこで、 a^{Φ}(x_{1}, ..., x_{n}) ∈ T F^{Φ} とし、 I(x_{1}, ..., x_{n}) = i_{1}, ..., i_{s} (s = m(x_{1}, ..., x_{n})) とする。また、 i = 1, 2, ..., n に対して、 t_{i} = σx_{i} とする。このとき、 a^{Φ}(x_{1}, ..., x_{n}) ∈ [P F^{Φ}] であることを rk a に関する帰納法で証明する。

(�) rk a = 0

• a ∈ Con のとき a^{Φ}(x_{1}, ..., x_{n}) = (t_{1}, ..., t_{n})/Φa を示す。 (w_{1}, ..., w_{n}) ∈ W_{t_{1}}×…× W_{t_{n}} に対して、 v ∈ V al を vx_{l} = w_{l} (l ∈ {i_{1}, ..., i_{s}}) なるものとすると、

a^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}a)v  (∵表現関数の定義)
= Φa  (∵ a ∈ Con)
= ((t_{1}, ..., t_{n})/Φa)(w_{1}, ..., w_{n})

より、 a^{Φ}(x_{1}, ..., x_{n}) = ((t_{1}, ..., t_{n})/Φa) ∈ P F^{Φ} ⊆ [P F^{Φ}]

• a ∈ V ar のとき F var^{a} = {a} で、 F var^{a} ⊆ {x_{1}, ..., x_{n}} = {x_{i_{1}}, ..., x_{i_{s}}} より、 a = x_{i} なる i ∈ {i_{1}, ..., i_{s}} が存在するこのとき、 a^{Φ}(x_{1}, ..., x_{n}) = (t_{1}, ..., t_{n}) ↓ i を示す。 (w_{1}, ..., w_{n}) ∈ W_{t_{1}}×…× W_{t_{n}} に対して、 v ∈ V al を vx_{l} = w_{l} (l ∈ {i_{1}, ..., i_{s}}) なるものとすると、

a^{Φ}(w_{1}, ..., w_{n}) = (Φ^{∗}a)v  (∵表現関数の定義)
= va  (∵ a ∈ V ar)
= w_{i}  (∵a = x_{i} で i ∈ {i_{1}, ..., i_{s}} より v の定義)
= ((t_{1}, ..., t_{n}) ↓ i)(w_{1}, ..., w_{n})

より、 a^{Φ}(x_{1}, ..., x_{n}) = ((t_{1}, ..., t_{n}) ↓ i) ∈ P F^{Φ} ⊆ [P F^{Φ}] 従って、 rk a = 0 の場合は成立する。 (�) rk a > 0 とする。 (a = α_{λ}(a_{1}, ..., a_{n_{λ}}))

• λ が不変子のとき a = α_{λ}(a_{1}, ..., a_{n_{λ}}) で、 x_{1}, ..., x_{n} は a の自由変数列より、補題 4.3.2 を用いると、

(1) x_{1}, ..., x_{n} は a_{k} の自由変数列 (k = 1, 2, ..., n_{λ})

(2) a^{Φ}(x_{1}, ..., x_{n}) = ω_{λ} ∘ (a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n}))……� が成立する。このとき、 (a_{1}, ..., a_{n_{λ}}) ∈ Dom α_{λ} なので、補題 4.3.1 より、 W_{σa_{1}}×…× W_{σa_{n_{λ}}} ⊆ Dom ω_{λ} となる。また、各 a_{k} の自由変数列は x_{1}, ..., x_{n} より (各 a_{k} に対して同じ自由変数列となっている)、それぞれの自由変数列の基底の位置も等しくなる。従って、 a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n}) に対して、 T F^{Φ} 上の算法 λ を定義することができる。このとき、 a^{Φ}(x_{1}, ..., x_{n}) = λ(a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})) が成立することを示す。 (w_{1}, ..., w_{n}) ∈ W_{t_{1}}×…× W_{t_{n}} に対して、

λ(a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n}))(w_{1}, ..., w_{n})
= (ω_{λ} ∘ (a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n})))(w_{1}, ..., w_{n}) (∵λの定義)
= a^{Φ}(w_{1}, ..., w_{n})  (∵�)

さらに、 k = 1, 2, ..., n_{λ} に対して rk a > rk a_{k} より、帰納法の仮定から、 a_{k}^{Φ}(x_{1}, ..., x_{n}) ∈ [P F^{Φ}] 従って、 a^{Φ}(x_{1}, ..., x_{n}) = λ(a_{1}^{Φ}(x_{1}, ..., x_{n}), ..., a_{n_{λ}}^{Φ}(x_{1}, ..., x_{n}))∈ [P F^{Φ}]

• λ が可変子のとき ( λ = ...y_{1}......y_{m}... とする。 ) λ は可変子より単項算法 (空算法も単項算法とみなしている) で、 a = λ(a_{1}, ..., a_{n_{λ}}) より λ は空算法でない。そこで、 a = λa_{1} とする。このとき、 x_{1}, ..., x_{n} は a の自由変数列より、補題 4.3.2 から (1) x_{1}, ..., x_{n}, y_{1}, ..., y_{m} は a_{1} の自由変数列

(2) (w_{1}, ..., w_{n}) ∈ W_{σx_{1}}×…× W_{σx_{n}} に対して、 a^{Φ}(w_{1}, ..., w_{n}) = λ_{W} (a_{1}^{Φ}(w_{1}, ..., w_{n}, □, ..., □)) が成立する。このとき、 rk a > rk a_{1} より帰納法の仮定から、 a_{1}^{Φ}(x_{1}, ..., x_{n}, y_{1}, ..., y_{m}) ∈ [P F^{Φ}] となる。また、 t_{n+j} = σy_{j} (j = 1, 2, ..., m) とすれば、 a_{1}^{Φ}(x_{1}, ..., x_{n}, y_{1}, ..., y_{m}) ∈ W_{t_{1}}×…× W_{t_{n+m}} → W_{σa_{1}} となる。さらに、 σa_{1} ∈ Domλ であり、 σy_{j} = t_{n+j} より ♭_{λ}(a_{1}^{Φ}(x_{1}, ..., x_{n}, y_{1}, ..., y_{m})) を定義することができる。このとき、 (w_{1}, ..., w_{n}) ∈ W_{t_{1}}×…× W_{t_{n}} に対して、

\begin{aligned}(♭_{λ}(a_{1}^{Φ}(x_{1}, ..., x_{n}, y_{1}, ..., y_{m})))(w_{1}, ..., w_{n}) & = & λ_{W} (a_{1}^{Φ}(w_{1}, ..., w_{n}, □, ..., □)) \\ & = & a^{Φ}(w_{1}, ..., w_{n}) & (∵ (2)) \end{aligned}

従って、 a^{Φ}(w_{1}, ..., w_{n}) = (♭_{λ}(a_{1}^{Φ}(x_{1}, ..., x_{n}, y_{1}, ..., y_{m})))∈ [P F^{Φ}] 以上より、 [P F^{Φ}] = T F^{Φ} がわかる。

q.e.d.

参考文献

[1] 五味健作著、『数理心理学‐思考機械・論理・言語・代数系‐』 (WWW 出版、 2006 年 8 月 27 日版) ( http://homepage3.nifty.com/gomiken/mathpsy/index.htm で入手可能)

[2] 金子洋之著、『記号論理入門』 (産業図書)