第 2 章述語論理

第 2 章述語論理
1 述語論理
A. 数学的理論の形式的展開
b. 数学的理論の展開
１．公理はつぎの 2 つ。
1.1) 論理的公理
これはすべての数学理論に共通に成り立つと仮定させられている論理式
① トートロジーに含まれる全ての命題変数にそれぞれ任意の論理式を代入して得られる論理式は全て論理
的公理である。
② A4:xF(x)⊃ F (t)A5 : F (t) ⊃ ∃xF (x)
は論理的公理。ただし、F(t) は F(x) のすべての x に項 t を代入したものを表す。
2.2) 数学的公理
これは取り扱う数学理論に固有な公理。数学的公理の集合を、その数学理論に対する公理系という。
2. 推論規則
すでに Hp で述べた推論規則のほか、∀ および ∃ についての推論規則がつけ加わる。すなわち、
R1:A”,A”⊃ B ⊢ B(M P )
R2:A”⊃ F (a) ⊢ A′′ ⊃ ∀xF (x)
R3:F(a)⊃ A′′ ⊢ ∃xF (x) ⊃ A′′
は推論規則であう。
定義 3
a および b で規定された体系を（第一階）述語論理の上の形式的体系という。またこの体系が数学的公理を
多く含まないとき、この体系を（第一階）述語計算といい、Hp で表す。
定理 1
定義 3 で規定された述語の上の形式的体系とは、次の１∼４で定められる形式的体系と同値である。
1. 記号
(1) 対象定数 ci (2) 自由変数 ai (3) 束縛変数 xni
(4) 関数記号 fni (5) 述語記号 pni [(1)∼(5) は上で述べたものと同一] (6) 論理記号 ⊃, ¬, ∀
2. 表現
論理式（定義２），項（定義１）
3．公理
1
① 論理的公理 A1:A”⊃ (B ⊃ A′′ )A2 : (A′′ ⊃ (B ⊃ C)) ⊃ ((A′′ ⊃ B) ⊃ (A′′ ⊃ C)A3 : (¬B ⊃ ¬A′′ ) ⊃
((¬B ⊃ A′′ ) ⊃ B)A4 : ∀xF (x) ⊃ F (t)
② 数学的公理
4．推論規則
R1:A”,A”⊃ B ⊢ B(M P )R2 : A′′ ⊃ F (a) ⊢ A′′ ⊃ ∀xF (x)
ただし、a は A” にも F(x) にも含まれない自由変数とする。
B. フレーム
a. フレーム
言語 L とは数学理論に現れる具体的な用語を一般的に形式化したものであった。したがって L に現れるの
は意味のない記号の列。L の論理式は、各記号が具体的に何を表すかという解釈が与えられたとき、始めて意
味をもってくる。そして正しいかどうか定義できる。このように L として解釈して与えられる対象とその解
釈ー対応ーをフレームという。
定義 4 1)M は空でない集合とし、フレームの領域という。2)ci (i = 0, 1, 2, ...) ただし、ci ∈ M とする。L の
対象定数 ci からci ∧ の写像をρ で表す。（ci は L の対象定数に対応する具体的な対象を表している）
3)fi n (n = 1, 2, ...; i = 0, 1, 2, ...) ただし fi n を n 変数の関数記号とするときfi n は M の n 個の直積 M n か
n
ら M への一意写像 (M の operation) である。L の関数記号 fi n からf i への写像を。
4)pni (n = 1, 2, ...; i = 0, 1, 2, ...) ただし pi n を n 変数の述語記号とするときpi n は M の n 個の直積 M n の部
分集合である。すなわち、＜ v1 , ..., vn ＞の形の元からなる集合を表し、vi ∈ M である。L の述語記号 pi n か
らpi n への写像をτ で表す。
以上 1）∼4）の集合 M’ = [M;ρ; σ; τ ] を L の１つのフレームという。
例
言語 L の論理式としてたとえば P20 (a1 , a2 ), ∀x1 P0 2 (a1 , x1 ) などが与えられたとし、P0 2 (∗1 , ∗2 ) は自然数論
における述語∗1 ≤ ∗2 に対応する記号として用いられたとする。L のフレームを 1 つ定めた時 M として自然数
の集合を選んだとする。
P20 (a1 , a2 ) に対して)p0 2 は集合｛＜ x, y ＞ |x ≤ y ｝で表しており Po 2 (a1 , a2 ) は)p0 2 の元 < x, y > によって
みたされる。また、∀x1 P0 2 (a1 , x1 ) は、すべての自然数 x1 に対して a1 ≤ x1 が成り立つという性質を表してお
り、a1 = 0 のときだけみたされる。さらに ∃x2 ∀x1 )p20 (x2 , x1 ) を考えれば、これはどんな自然数 x1 に対して
も、x2 ≤ x1 が成り立つような x2 が存在する。すなわち最小の自然数が存在することを表す命題であり、M が
自然数の集合のときは真な命題を表しているが、フレームを変えて M を整数の集合とすれば偽な命題となる
。このように、フレームの定め方によって真にも偽にもなる。
b.「みたされる」の定義
M’ の領域 M の元からつくられた可算列を M’ の点列といい m,n などで表す。M’ の 2 つの点列
m=(m’0 , m′1 , m′2 , ...), n = (n′0 , n′1 , n′2 , ...), m′i ∈ M, n′i ∈ M
に対し、i̸= j ならば m′j = n′j であるとき m′ = n′ と書くことにする。そこで L の項、論理式などをフレー
ム M ′ の元によって解釈するところから始める。
定義５ t を L の項とするとき、t[m’] を次のように定義する。1)t が自由変数 ai のとき、t[m′ ] = m′i 2)t が対
n
象定数 ci のとき、t[m′ ] = ci 3)t が f n (t1 , ..., tn ) のとき、t[m′ ] = f (t1 [m′ ], ..., tn [m′ ])
2
2
例 L の項 t が f22 (a3 , f1 2 (a1 , c4 )) とする。L のフレームを M ′ として、領域 M は整数の集合f1 (∗1 , ∗2 ) は ∗1
2
+∗2 , f2 (∗1 , ∗2 ) は ∗1 ∗ ∗2 で c4 は M の指定された元、整数 3 であるとする。
2
2
M’ の任意の点列 m’ に対し、t[m’]=f2 (m′3 , f1 (m′ , 3)) = m′3・(m′1 + 3)
m’1 , m′3 は M の元だから、t[m′ も M の元になっていることが分かる。
このように t[m’] は直観的にいうと、t に現れる自由変数を m’ の元でおきかえ、t に現れる関数記号は、M’
の対応する関数を置き換えられる M の元のことである。
定理２
t を L の項，m’ を M’ の点列とすれば、t[m’]∈ M ′ である。
証明方針:t に含まれる関数記号の個数についての帰納法を用いる。
t が自由変数のとき ai のとき t[m′ ] = m′i ∈ M ′ , t が対象定数 ci のとき t[m′ ] = ci ∈ M ′ は定義 5 より明らか
であるから t が f n (t1 , ..., tn ) のとき、各 ti [m′ ] ∈ M ′ とすると < t1 [m′ ], ..., tn [m′ ] >∈ M n であり、f n は M ′n
から M の中への一意写像であるから
t[m’]=fn (t1 , ..., tn )[m′ ] = f n (t1 [m′ ], ..., tn [m′ ]) ∈ M
である。
次に、L の任意の論理式 A” に、フレーム M’ の点列 m’ を代入したとき、A” が成り立つという概念を帰納
的に次のように定義する。
定義 6 L の論理式 A”,M’ の点列 m’ について、M’,m’|= A′′ を次のように定義する。
1)A” が素論理式のとき M’,m’|= pi n (t1 , ..., tn ) < t1 [m′ ], ..., tn [m′ ] >∈ Pi
n
2)A” の一番外側の記号が ¬, ∧, ∨,
M’,m’|= ¬BM ′ , m′ |= B が成り立たない。M ′ , m′ |= B ∧ CM ′ , m′ |= B かつ M ′ , m′ |= CM ′ , m′ |=
B ∨ CM ′ , m′ |= B または M ′ , m′ |= CM ′ , m′ |= B ⊃ CM ′ , m′ |= B ならば M ′ , m′ |= C
3)A” の一番外側の記号が、∀, ∃ のとき、
M’,m’|= ∀xj F (xi )m′ = n′ をみたす任意の n′ に対して M ′ , n′ |= F (ai )
M’,m’|= ∃xi F (xj )m′ = n′ をみたすある n′ に対して M ′ , n′ |= F (ai )
ただし、3) における ai は F (xj ) に現れない自由変数のうちで最小の番号を持ったものとする。M ′ , m′ |= A′′
のとき、A′′ は M ′ において m′ によってみたされるという。(satisf iable)
例 L の論理式 A” が P21 (f1 1 (a2 ), a3 ) であるとする。これは素論理式。
L のフレーム M’ の領域 M として実数の集合をとり、P21 (∗1 , ∗2 ) を∗1 = ∗2 , f1 1 (∗) を exp(∗) と解釈
すれば M ′ の任意の点列 m′ = (m′0 , m′1 , m′2 , ...) に対し、A′′ が M ′ において m′ によってみたされると
は expm′2 = m′3 が成り立つときをいう。定義６の 1）ではこのことを a = b をみたす順序対 < a, b > の集合
pi 2 を用いて < expm′2 , m′3 >∈ pi 2 と表してある。
注:L の論理式 A” が、∀x3 P 5 (a0 , a1 , x3 , a6 , a7 ) とし A′′ が M ′ の任意の点列 m′ = (m′0 , m′1 , m′2 , ...) によっ
てみたされるとは直観的に M ′ , n′ |= P 5 (a0 , a1 , a2 , a6 , a7 ) が成り立てばよいことで定義 6 の 3) の妥当である
ことがわかる。
定理 3
L の任意の論理式 A”,M’ の任意の点列 m’ について、M’,m’|= A′′ または M ′ , m′ |= ¬A′′ の一方だけが
成り立つ。
証明定義６の２）より明らか。
定理４１）1.1 節の B 項における (1.1)∼(1.6),(1.8) および (1.14)∼(1.18) に対し、これらの論理式に現れ
3
る命題変数を任意の論理式でおきかえれば、A”≡ B の形のトートロジーをえるが、このとき
M’,m’|= A′′ M ′ , m′ |= B
2)M’,m’|= ∃xF (x)m′ , n′ |= ¬∀x¬F (x)M ′ , m′ |= ∀xF (x)m′ , n′ |= ¬∃x¬F (x)
ただし、m’ は M’ の任意の点列とする。
注:以下形式的な計算を簡単化するため m2
4

Download Report