. T ::= x f n t 1 t n F n,m (x(t 1 t n )t 1 t m) x, f n n, F n,m n, m-., F n,m (x(t 1 t n )t 1 t m), x, t 1,..., t n, t 1,..., t m. F n,m (x(t 1 t n )

項内に束縛関係を持つ一階述語論理の構成

東京工業大学 情報理工学院 中村 知己

Kazuki Nakamura

Department of Mathematical and Computing Science,

Tokyo Institute of Technology

東京工業大学 情報理工学院 鹿島 亮

*1

Kashima Ryo

Department of Mathematical and Computing Science,

Tokyo Institute of Technology

1

はじめに

一階述語論理では_{∀, ∃}によって, 論理式中の変数記号を束縛する. 一方で項について考えると, 一般に数学 では総和記号Σや積分記号∫ を使って表されるような項内に束縛関係を持つ項を考えるのに対し, 一階述語 論理における項の定義はこのような項を許していない. 本研究の目的はこのような項を自然に表現できるよう に一階述語論理を拡張することである. また,拡張体系と二階述語論理との関係について考察する. 本稿における通常の一階述語論理に関する記法や議論は主に文献[1]に基づく．

2

構文論

2.1

言語と文法

本論文にて一階述語論理の言語は以下の記号を持つ. 変数記号 x, y, z, ...で表す. 関数記号 f, g, h, ...で表す. 束縛演算子記号 F, G, ...で表す.（これが本稿で拡張されたものである） 述語記号 p, q, ...で表す. 論理記号 =,⊥, ∧, ∨, →, ¬, ∀, ∃ 補助記号 (, ) 関数記号,述語記号には1つの，束縛演算子記号には2つの，アリティと呼ばれる自然数(0を含む)がそれぞ れ定まっており, 明示的にアリティを示す際にはn-引数関数記号, n-引数述語記号n, m-引数束縛演算子記号 と呼ぶ. 特に0-引数関数記号を定数記号と呼びcを使って表すことにする. 変数記号の集合をV arとする. ま た,変数記号は可算無限個, その他の記号は高々可算個存在するものとする. 定義 2.1 *1 _{kashima@is.titech.ac.jp (代表著者)}

項の定義を次のように拡張する. T ::= x| fnt1· · · tn| Fn,m(x(t1· · · tn)t′1· · · t′m) ここでxは変数記号, fnはn引数関数記号, Fn,mはn, m-引数束縛演算子とする. また, Fn,m(x(t1· · · tn)t′1· · · t′m)という形の項に対して, xを束縛変数記号, t1, ..., tnを束縛項, t′1, ..., t′mを自 由項と呼ぶことにする. 項Fn,m(x(t1· · · tn)t′1· · · t′m)では束縛項t1, ..., tnが変数記号xで束縛されており,自由項t′1, ..., t′mは束縛 されていない. 例えば, 総和∑n k=1(k + c)は1, 2-引数束縛演算子記号Σを用いてΣ(k(k + c)1 n)のように書 く. 以下,項をs, t等を用いて表す. 定義 2.2 論理式を以下で定義する. φ ::=⊥ | t = s | pt1· · · tn| (¬φ) | (φ ∧ ψ) | (φ ∨ ψ) | (φ → ψ) | (∀xφ) | (∃xφ) 以下,論理式をφ, ψ, ρを使って表す. また括弧については誤解の余地がない場合は省略する. 束縛演算子記号からなる項以外の項および論理式の束縛関係は通常通りである. 束縛演算子記号からなる項 については以下のように定義する. 定義 2.3 tがF (x(t1· · · tn)t′1· · · t′m)のときt1, ..., tn, t′1, ..., t′mの束縛出現および, t1′, ..., t′m以外に出現するxがtの束 縛出現である. 項または論理式で束縛されていない変数の出現を自由出現といい, 項t,論理式φに対して,束縛出現する変 数の集合をBV ar(t), BV ar(φ),自由出現する変数の集合をF V ar(t), F V ar(φ)と書く. 自由出現する変数記 号が存在しない項や論理式を閉項,閉論理式という. 定義 2.4 項tまたは論理式φの変数記号xに項sが代入可能であるとは, t, φのxの自由出現を項sに書き換えた際に 新たな束縛関係が生じないことをいう. 代入可能であるとき, 代入した結果をt[s/x], φ[s/x]と書く.

2.2

演繹体系

束縛演算子記号の導入に対して,演繹体系を拡張することを考える. 等号記号を含む自然演繹に対して束縛 演算子記号に関する規則を加える. ∀x(t1= s1) ∀x(t2= s2) · · · ∀x(tn= sn)

F (x(t1· · · tn)t′1· · · t′m) = F (y(s1[y/x]· · · sn[y/x])t′1· · · t′m)

(束縛代入) (ただしyはxであるか, s1, ..., snのxに代入可能かつ自由出現しない変数記号である) (束縛代入)は総和記号Σの例で表すと 任意のxに対してf (x) = g(x) から n ∑ x=1 f (x) = n ∑ y=1 g(y) を導くような推論規則である.

また,論理式の集合Γと論理式φについて解消されていない仮定がすべてΓの要素であるようなφの導出 図が存在することをΓ⊢ φと書く.

3

意味論

3.1

ストラクチャー

この体系に対してのストラクチャーを以下のように定める. 定義 3.1 ストラクチャーとは以下の組である. ・対象領域D (Dの要素を個体と呼ぶ) ・関数記号f 束縛演算子記号F 述語記号pの解釈fM_{, F}M_{, p}M 束縛演算子記号の解釈を除けば通常の古典論理のストラクチャーである. n, m-引数束縛演算子記号F のス トラクチャーM での解釈FM を考える. 例えば,総和記号Σは束縛項の束縛変数に幾つかの整数を代入して 得られた結果を足し合わせたものであるように一般に束縛項の束縛変数記号に複数の個体を代入したものを考 える必要がある. すなわち束縛項の解釈は関数としての性質を持つべきであり,束縛演算子記号の解釈は個体 だけでなく, 関数を引数に取ることが求められる. そこでn, m-束縛演算子記号Fn,mの解釈Fn,mM を以下のよ うな関数とする. F_n,mM : (D→ D)n× Dm→ D このように定義することにより,束縛演算子の性質を満たすことができる. 項や論理式の解釈は, 個体それぞれを示す名前と呼ばれる定数記号を言語に加えることにより, 閉論理式や 閉項についてのみ帰納的に定義する手法がある. しかしこの手法は束縛演算子を含む項を解釈するには適当で はない. 実際にΣ(k(k + c)1 n)の例においてk + cがある個体に解釈されたとすると,束縛変数記号であるk の情報が消えてしまい, k + cをkについての関数と解釈することができない. これを解決するため, 文献[2] で用いられる方法を採用する. 個体割り当てというV arからDへの写像を考え, ストラクチャーと個体割り 当ての組によって項の解釈を定義することを考える. 以下個体割り当てはσを使って表す. 項の解釈を定義する前に1つ準備をする. 定義 3.2 個体割り当てσとx∈ V ar, a ∈ Dに対して,個体割り当てσ(x→ a)を以下のように定義する. σ(x→ a)(y) = { a (y = x) σ(y) (y̸= x) これは個体割り当てについてある変数記号に対する割り当てを指定したものである. このとき明らかに以下 の2つが成り立つ. σ(x→ a)(x → b) = σ(x → b) σ(x→ a)(y → b) = σ(y → b)(x → a) これらは今後断りなく用いることにする. ストラクチャーとこの個体割り当てを用いて項の解釈を定義する. 定義 3.3 ストラクチャーM と個体割り当てσに対する項tの解釈Mσ(t)∈ Dを以下のように帰納的に定義する.

(1) t = x(xは変数記号)のとき, Mσ_{(x) = σ(x)} (2) t = f t1· · · tnのとき, Mσ(f t1· · · tn) = fM(Mσ(t1), ..., Mσ(tn)) (3) t = Fn,m(x(t1· · · tn)t′1· · · t′m)のとき, Mσ(Fn,m(x(t1· · · tn)t′1· · · t′m)) = F M n,m((M σ x(t1), ..., Mxσ(tn)), (Mσ(t′1), ..., M σ_(t′ m))) ただしMxσ(t)は任意の個体aに対してMxσ(t)(a) = Mσ(x→a)(t)をみたすD上の関数である. 項の解釈と同様にストラクチャーM と個体割り当てσに対して論理式の解釈を定義する. 定義 3.4 ストラクチャーM と個体割り当てσに対する論理式φの解釈Mσ_{(φ)∈ {T rue, F alse}を以下のように定} める Mσ(⊥) = F alse Mσ(t = s) = T rue ⇐⇒ Mσ(t) = Mσ(s) Mσ(pnt1· · · tn) = T rue ⇐⇒ pMn (M σ_(t 1), ..., Mσ(tn)) Mσ(¬ψ) = T rue ⇐⇒ Mσ(ψ) = F alse

Mσ(ψ1∧ ψ2) = T rue ⇐⇒ Mσ(ψ1) = T rueかつMσ(ψ2) = T rue

Mσ(ψ1∨ ψ2) = T rue ⇐⇒ Mσ(ψ1) = T rueまたはMσ(ψ2) = T rue

Mσ(ψ1→ ψ2) = T rue ⇐⇒ Mσ(ψ1) = T rueならばMσ(ψ2) = T rue

Mσ(∃xψ) = T rue ⇐⇒ ∃a ∈ D Mσ(x→a)(ψ) = T rue Mσ(∀xψ) = T rue ⇐⇒ ∀a ∈ D Mσ(x→a)(ψ) = T rue このように定義された解釈に対して,モデルという概念と_|=の使い方を定義する. 定義 3.5 論理式の集合Γに対して, ストラクチャーM とその個体割り当てσが存在して, 任意のψ ∈ Γ に対して Mσ(ψ) = T rueが成り立つとき, Γはモデルを持つといい,このM, σの組をモデルという. 定義 3.6 Γを論理式の集合, φを論理式とする. Γ|= φとは以下が成り立っていることをいう. ΓのすべてのモデルM, σに対してMσ(φ) = T rue

3.2

意味論の性質

前節で定義した意味論に関するいくつかの性質を示す. すべて項や論理式の構成に関する帰納法により示 せる. 定理 3.7 M を任意のストラクチャー, σをM の任意の個体割り当てとする. (1) 項tとtに自由出現しない変数xに対して以下が成り立つ. 任意の個体aに対してMσ(t) = Mσ(x→a)(t) (2) 論理式φとφに自由出現しない変数xに対して以下が成り立つ.

定理 3.8

M, σを任意のストラクチャーとその個体割り当てとする. 項sに対してMσ_{(s) = aとする.}

(1) 項tについて以下が成り立つ.

Mσ(t[s/x])＝Mσ(x→a)(t)

(2) 論理式φについて以下が成り立つ.

Mσ(φ[s/x])＝T rue⇐⇒ Mσ(x→a)(φ) = T rue 定理 3.9 M を任意のストラクチャー, σをM の任意の個体割り当てとする. (1) 項tとtのxに代入可能な項s1, s2について以下が成り立つ. Mσ(s1) = Mσ(s2)ならばMσ(t[s1/x]) = Mσ(t[s2/x]) (2) 論理式φとφのxに代入可能な項s1, s2について以下が成り立つ. Mσ(s1) = Mσ(s2)ならば, (Mσ(φ[s1/x]) = T rue⇐⇒ Mσ(φ[s2/x]) = T rue) 定理 3.10 M を任意のストラクチャー, σをM の任意の個体割り当てとする. (1) 項tとtに自由出現しない変数記号yおよび個体aに対して以下が成り立つ.

Mσ(x→a)(t) = Mσ(y→a)(t[y/x])

(2) 論理式φとφに自由出現しない変数記号yおよび個体aに対して以下が成り立つ.

Mσ(x→a)(φ) = T rue⇐⇒ Mσ(y→a)(φ[y/x]) = T rue

4

健全性と完全性

4.1

健全性

定理 4.1 (健全性定理) Γを論理式の集合, φを論理式としたとき以下が成り立つ. Γ⊢ φ =⇒ Γ |= φ Proof. Γ⊢ φのときφを導く証明図_Aが存在する. Aの大きさによる帰納法で示す. 証明図の最後に使われた規則 で場合分けを行う. ∃, ∀に関する規則と束縛代入以外については定理3.9より通常のNKと同様の方法で示せる. (∃I) 帰納法の仮定よりΓ |= ψ[t/x]すなわちΓのモデルM, σに対してMσ_{(ψ[t/x]) = T rue. M}σ_{(t) = a}

(∃E) このとき証明図は以下のような形になる. .. .. (A1) ∃xψ [ψ[y/x]] .. .. (A2) ρ ρ (∃E) Γ1, Γ2 ⊂ ΓをそれぞれA1, A2 の解消されていない仮定の集合とする. A1に関する帰納法の仮定よ りΓ1|= ∃xψ. ΓのモデルM, σについてMσ(∃xψ) = T rueであり,このときある個体aが存在して

Mσ(x→a)(ψ) = T rueが成り立つ. 定理3.10よりMσ(y→a)(ψ[y/x]) = T rueが成り立つ. ここでyは Γ2の論理式に自由出現しないため定理3.7よりM, σ(y→ a)はΓ2∪ {ψ[y/x]}のモデルである. A2に

関する帰納法の仮定よりMσ(y→a)(ρ) = T rueとなり, yはρにも自由出現しないのでMσ(ψ) = T rue が成り立つ.

(∀I) 解消されていない仮定の集合をΓ′ とする. Γ′ ⊂ ΓであるからΓのモデルM, σはΓ′のモデルでもあ る. yはΓ′ の論理式に自由出現しないため, 任意の個体aについてM, σ(y→ a)はΓ′のモデルであ る. 帰納法の仮定よりMσ(y→a)_{(φ[y/x]) = T rueであり,定理3.10よりM}σ(x→a)_{(φ) = T rue. ∀の解}

釈に関する定義よりMσ_{(∀xφ) = T rueとなり成り立つ.} (∀E) Γ のモデルM, σ について, 帰納法の仮定より Mσ(∀xφ) = T rueであり, 任意の個体a に対し て Mσ(x→a)(φ) = T rue が 成 り 立 つ. a は 任 意 で あ る か ら Mσ(t) = a と す る と 定 理 3.8 よ り Mσ(φ[t/x]) = T rueが成り立つ. (束縛代入) ΓのモデルM, σについて,帰納法の仮定より1≤ i ≤ nとなる任意のiについてMσ_(∀x(t i =

si)) = T rue. このとき任意の個体aに対して Mσ(x→a)(ti) = Mσ(x→a)(si)となる. 定理3.10よ

り Mσ(x→a)_(s

i) = Mσ(y→a)(si[y/x]) であり, Mσ(x→a)(ti) = Mσ(y→a)(si[y/x])がいえる. a は

任意であったのでMσ

x(ti) はMyσ(si[y/x])と関数として等しい. このとき, 項の解釈の定義より,

Mσ_{(F (x(t}

1· · · ti· · · tn)t′1· · · t′m)) = Mσ(F (x(s1· · · si· · · sn)t′1· · · t′m))すなわち

Mσ(F (x(t1· · · tn)t′1· · · t′m) = F (y(s1[y/x]· · · sn[y/x])t′1· · · t′m)) = T rue

となる. 以上より健全性が示された.

4.2

完全性

定理 4.2 (完全性定理) Γを論理式の集合, φを論理式としたとき以下が成り立つ. Γ|= φ =⇒ Γ ⊢ φ 本節ではこの完全性定理を証明していく. 証明手法として文献[1]でなされている通常の一階述語論理に対 する完全性の証明に対し,束縛演算子記号に関する議論を加えることで行う. 束縛演算子記号以外については 同じ議論となるため,適宜証明は省略する. まず,論理式の集合に対して矛盾,無矛盾という概念を定義する.

定義 4.3 論理式の集合Γに対し, Γ⊢ ⊥が成り立っているとき, Γは矛盾するといい, そうでないときΓは無矛盾であ るという この矛盾の概念を用いて以下の定理を考える. 定理 4.4 (モデル存在定理) Γを論理式の集合としたとき以下が成り立つ. Γが無矛盾=⇒ Γはモデルを持つ モデル存在定理から完全性定理を導けることが知られている. したがって,モデル存在定理を示せばよい. 文献[1]に倣い,変数集合V arを自由出現する変数の集合_Fと束縛出現する変数の集合_Bを分けたものを 考える. すなわち_{F ∩ B}が空集合となっているものとする. ただし, F, Bはともに無限集合であるとする. 本 節では以降, 項,論理式の集合として以下で定義されるものを考える.

Term_F,B={t | F V ar(t) ⊂ F, BV ar(t) ⊂ B} Fomula_F,B={φ | F V ar(φ) ⊂ F, BV ar(φ) ⊂ B}

Γ⊂ Fomula_F,BかつΓに自由出現しない_Fの要素が無限個存在するようなΓに対してモデル存在定理が示 すことを目標とする. モデルを構成するため,極大無矛盾集合と呼ばれる集合を定義する. 定義 4.5 論理式の集合Γ⊂ Fomula_F,Bが極大無矛盾集合であるとは以下が成り立つことをいう. • Γは無矛盾 • 任意のφ∈ Fomula_F,Bに対して, φ∈ Γまたは_{¬φ ∈ Γ} • 任意の_{∃xφ ∈ Γ}に対してある項t∈ Term_F,Bが存在してφ[t/x]∈ Γ 極大無矛盾集合の性質として以下の性質が知られている. 定理 4.6 Γ が極大無矛盾集合ならば以下が成り立つ. Γ⊢ φ ⇐⇒ φ ∈ Γ 定理 4.7 Γ が極大無矛盾集合ならば以下が成り立つ. ¬ψ ∈ Γ ⇐⇒ Mσ(ψ)̸∈ Γ ψ1∧ ψ2∈ Γ ⇐⇒ ψ1∈ Γかつψ2∈ Γ ψ1∨ ψ2∈ Γ ⇐⇒ ψ1∈ Γまたはψ2∈ Γ ψ1→ ψ2∈ Γ ⇐⇒ ψ1̸∈ Γまたはψ2∈ Γ ∃xψ ∈ Γ ⇐⇒ ∃s ∈ TermF,B ψ[s/x]∈ Γ ∀xψ ∈ Γ ⇐⇒ ∀s ∈ TermF,B ψ[s/x]∈ Γ

無矛盾な論理式の集合 Γ ⊂ Fomula_F,B から Γ ⊂ Γ+ _{となるような極大無矛盾集合Γ}+ _{を構成する.} Fomula_F,Bは可算集合であるため, 要素を順に並べてφ1, φ2,· · · とする. Γ0= Γとし, Γnを以下のように定 義する. Γn+1=        Γn (Γn∪ {φn+1}が矛盾する) Γn∪ {∃xψ, ψ[y/x]} ( Γn∪ {φn+1}が無矛盾かつ φn+1が∃xψという形のとき ) Γn∪ {φn+1} (それ以外) (ただしyはΓnにも∃xψにも自由出現しないFの変数記号である) Γ+₌∪∞ n=1Γnとすることにより, 極大無矛盾集合が構成できる. Term_F,Bに対して関係_∼を t∼ s⇐⇒ t = s ∈ Γdef + と定義し,この関係に対して同値類をとったものを対象領域Dとする. tを代表元とする同値類を[[t]]と表す. 束縛演算子記号以外の解釈は通常通り以下のように定める. fM([[t1]], ..., [[tn]]) := [[f t1· · · tn]] pM([[t1]], ..., [[tn]]) = T rue⇐⇒ pt1· · · tn∈ Γ+ これらは代入規則により, well-definedであることがいえる. [1] このストラクチャーでの束縛演算子記号の解釈を考える. 束縛演算子記号の解釈はD上の関数を引数に持 つため,関数を項で表すことができるかが重要である. 以下で項表現可能,項表現という概念を導入する. 定義 4.8 x∈ Bとする. D上の関数gがxによって項表現可能であるとは, F V ar(T )⊂ F ∪ {x}, BV ar(T ) ⊂ Bとな る項Tが存在して,任意のs∈ T erm_F,Bに対して以下を満たすことをいう. g([[s]]) = [[T [s/x]]] xによって項表現可能なgに対して,上のような項TをTg,xと書き, gのxによる項表現と呼ぶ. 定義 4.9 このストラクチャーM での束縛演算子記号F の解釈FM を次のように定める FM((g1, ..., gn), ([[t′1]], ..., [[t′m]])) =    [[F (x(Tg1,x· · · Tgn,x)t′1· · · t′m)]] ( ある変数記号xによって すべてのgiが項表現可能のとき ) [[y]] (otherwise) (ただしyは_Fのある変数記号である) この定義がwell-definedになっていることを示す. 自由項に関しては関数記号と同様に言える. 束縛項に関 しては,以下の定理を示せば良い. 定理 4.10 Tgi,xがgiのxによる項表現であり, Tg′i,yがgiのyによる項表現であるとき, 以下が成り立つ. [[F (x(Tg1,x· · · Tgn,x)t ′ 1· · · t′m)]] = [[F (y(Tg′1,y· · · T ′ gn,y)t ′ 1· · · t′m)]]

Proof. Tg1,x, ..., Tgn,x, Tg′1,y, ..., T ′ gn,yに束縛出現する変数記号は有限であるから, これらに含まれていないBの変数 記号zが存在する. このときzはTg1,x, ..., Tgn,xのxに代入可能であり,さらにTg′1,y, ..., T ′ gn,yのyにも代入 可能である. 以下の3つを示せば十分である. [[F (x(Tg1,x· · · Tgn,x)t′1· · · t′m)]] = [[F (z(Tg1,x[z/x]· · · Tgn,x[z/x])t′1· · · t′m)]] (4.1) [[F (y(Tg′1,y· · · T ′ gn,y)t ′ 1· · · t′m)]] = [[F (z(Tg′1,y[z/y]· · · T ′ gn,y[z/y])t ′ 1· · · t′m)]] (4.2) [[F (z(Tg1,x[z/x]· · · Tgn,x[z/x])t1′ · · · t′m)]] = [[F (z(Tg′1,y[z/y]· · · T ′ gn,y[z/y])t ′ 1· · · t′m)]] (4.3) (4.1)まず_∀x(Tgi,x= Tgi,x)は仮定なしで導けるため, Γ+⊢ ∀x(Tgi,x= Tgi,x) となる. 定理4.6より, ∀x(Tgi,x = Tgi,x)∈ Γ + である. ここでzはTgi,xのxに代入可能であったから,束縛代入規則より, Γ+⊢ F (x(Tg1,x· · · Tgn,x)t ′ 1· · · t′m) = F (z(Tg1,x[z/x]· · · Tgn,x[z/x])t ′ 1· · · t′m) が成り立ち, 定理4.6より F (x(Tg1,x· · · Tgn,x)t ′ 1· · · t′m) = F (z(Tg1,x[z/x]· · · Tgn,x[z/x])t ′ 1· · · t′m)∈ Γ + となる. 同値類の定義より(4.1)が成り立つ. 同様にして(4.2)も示せる. (4.3) Tgi,x, Tg′i,yはそれぞれgiのx, yによる項表現であることから,任意のs∈ TermF,Bに対して, [[Tgi,x[s/x]]] = [[T ′ gi,y[s/y]]] となる. ここでzはTgi,xのx及びTg′i,yのyに代入可能であったから, [[Tgi,x[z/x][s/z]]] = [[T ′ gi,y[z/y][s/z]]] すなわち, Tgi,x[z/x][s/z] = T ′ gi,y[z/y][s/z]∈ Γ + となる. ここで, sは任意であったため,定理4.7(6)から, ∀z(Tgi,x[z/x] = Tg′i,y[z/y])∈ Γ + が言える. これを用いることで束縛代入規則から, Γ+⊢ F (z(Tg1,x[z/x]· · · Tgn,x[z/x])t ′ 1· · · t′m) = F (z(Tg′1,y[z/y]· · · T ′ gn,y[z/y])t ′ 1· · · t′m) が成り立つことがわかる. 定理4.6より F (z(Tg1,x[z/x]· · · Tgn,x[z/x])t ′ 1· · · t′m) = F (z(Tg′1,y[z/y]· · · T ′ gn,y[z/y])t ′ 1· · · t′m)∈ Γ+ よって同値類の定義より(4.3)が成り立つ. このストラクチャーM に対して, σを,「任意のx∈ Fに対してσ(x) = [[x]]」が成り立つ任意の個体割り 当てとする. このM, σの組がΓのモデルになっていることを示す. 以下σはこの条件をみたすものとする.

補題 4.11 x1, ..., xn∈ Bとする. FVar(s)⊂ F ∪ {x1, ..., xn}, BVar(s) ⊂ Bとなる項sについて以下が成り立つ Mσ(s) = [[s∗]] ただし∗はσ(xi) = [[ti]] (ti∈ Term_F,B)としたときの代入[t1/x1][t2/x2]· · · [tn/xn]を表す. Proof. sの構成に関する帰納法で示す. 束縛演算子記号以外の場合は省略する. 簡単のため1,1-引数束縛演算子記号 の場合を示す. まず,束縛演算子を含む項の解釈の定義と帰納法の仮定から以下が成り立つ. Mσ(F (x(t)t′)) = FM(M_xσ(t), Mσ(t′)) = FM(Mxσ(t), [[t′∗]]) ここでMσ x(t)について考える. ∗からxに関する代入を除いたものを∗−とすると,任意のa∈ TermF,Bに対 して,以下が成り立つ. Mxσ(t)([[a]]) = Mσ(x→[[a]])(t) = [[t∗−[a/x]]] (∵帰納法の仮定) よって, t∗−はMσ x(t)のxによる項表現となっている. したがって, Mσ(F (x(t)t′)) = FM(M_xσ(t), [[t′∗]]) = [[F (x(t∗−)t′∗)]] = [[(F (x(t)t′))∗]] となる. したがってMσ_{(s) = [[s}∗_{]]が成り立つ.} 補題 4.12 論理式φ∈ Formula_F,Bについて以下が成り立つ. φ∈ Γ+⇐⇒ Mσ(φ) = T rue Proof. φの構成に関する帰納法で示す. (i) φが_⊥のときは明らか. (ii) φがt = sのとき, t = s∈ Γ+⇐⇒ [[t]] = [[s]]. 補題4.11よりこれはMσ(t) = Mσ(s)と同値であり,す なわちMσ(t = s) = T rueと同値である (iii) φがpt1· · · ptnのとき, pt1· · · ptn ∈ Γ+⇐⇒ pM([[t1]], ..., [[tn]]) = T rue ⇐⇒ pM (M (t1), ..., M (tn)) = T rue (∵補題4.11) ⇐⇒ Mσ_(pt 1· · · ptn) = T rue (iv) φが¬ψ, ψ1∨ ψ2, ψ1∧ ψ2, ψ1→ ψ2のいずれかの形のとき,定理4.7と帰納法の仮定から簡単に示せる.

(v) φが_{∀xψ, ∃xψ}のいずれかの形のとき,まず,∀xψについて考えると, 定理4.7と帰納法の仮定より ∀xψ ∈ Γ+_{⇐⇒任意の項t∈ Term} F,Bに対してψ[t/x]∈ Γ+ (4.4) ⇐⇒任意の項t∈ Term_F,Bに対して, Mσ(ψ[t/x]) = T rue (4.5) となる. (4.5)のとき, 任意の個体 aはある項t ∈ Term_F,B を使って[[t]]と表わせ, 補題4.11より Mσ_{(t) = [[t]]であるから,定理3.8より} 任意の個体aに対してMσ(x→a)(ψ) = T rue (4.6) が成り立つ. 逆に(4.6)のとき, 任意の項tは解釈はある個体となるため,定理3.8より(4.5)が成り立 つ. よって(4.5)と(4.6)は同値である. (4.6)は_∀に関する定義より, Mσ_{(∀xψ) = T rueと同値であ} るため,題意を示せた. ∃xψのときも同様に示せる. Γ⊂ Γ+_{であるため補題4.12よりこのM, σはΓのモデルである. 以上よりモデル存在定理がいえ, 完全性} 定理が示せた.

5

考察

本稿では, 一階述語論理の拡張として, 項の内部で項を束縛するような体系を構成した. これの発展として 項の内部で論理式を束縛する体系も同様に構成し, 健全性と完全性が示せるだろう. これらの体系は,関数や 個体集合を受け取り個体を返す関数を含むため, ある種の二階述語論理だと解釈できる. 二階述語論理では

standard semanticsとHenkin semanticsの2つの意味論が知られている(文献[3]などを参照). 本稿の議論 では, 項表現可能という概念を用いて,定義4.9の様にストラクチャーを構成している. 項表現できない関数 については適当な解釈を与えているため, この体系はstandard semanticsに対しても完全であるといえるだ ろう.

参考文献

[1] 鹿島亮 ,「数理論理学」朝倉出版, 2009 [2] 森田茂行,「論理学: 意味とモデルの理論」 東京電機大学出版局, 1999

[3] V¨a¨an¨anen, Jouko. ”Second-order logic and foundations of mathematics.” Bulletin of Symbolic Logic 7.4 (2001): 504-520.