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 ( ) 1
. 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 )t 1 t m) t 1,..., t n x, t 1,..., t m., n k=1 (k + c) 1, 2- Σ Σ(k(k + c)1 n)., s, t. 2.2. φ ::= t = s pt 1 t n ( φ) (φ ψ) (φ ψ) (φ ψ) ( xφ) ( xφ), φ, ψ, ρ.... 2.3 t F (x(t 1 t n )t 1 t m) t 1,..., t n, t 1,..., t m, t 1,..., 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(t 1 = s 1 ) x(t 2 = s 2 ) x(t n = s n ) F (x(t 1 t n )t 1 t m) = F (y(s 1 [y/x] s n [y/x])t 1 t m) ( ) ( y x, s 1,..., s n x ) ( ) Σ. x f(x) = g(x) n n f(x) = g(y) x=1 y=1 2
, Γ φ Γ φ Γ φ. 3 3.1. 3.1. D (D ) f F p f M, F M, p M. n, m- F M F M., Σ.,,. n, m- F n,m F M n,m. F M n,m : (D D) n D m 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). { a (y = x) σ(x a)(y) = σ(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. 3
(1) t = x(x ), M σ (x) = σ(x) (2) t = ft 1 t n, M σ (ft 1 t n ) = f M (M σ (t 1 ),..., M σ (t n )) (3) t = F n,m (x(t 1 t n )t 1 t m), M σ (F n,m (x(t 1 t n )t 1 t m)) = Fn,m((M M x σ (t 1 ),..., Mx σ (t n )), (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 σ (p n t 1 t n ) = T rue p M n (M σ (t 1 ),..., M σ (t n )) 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. a, M σ (φ) = T rue M σ(x a) (φ) = T rue 4
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 s 1, s 2. M σ (s 1 ) = M σ (s 2 ) M σ (t[s 1 /x]) = M σ (t[s 2 /x]) (2) φ φ x s 1, s 2. M σ (s 1 ) = M σ (s 2 ), (M σ (φ[s 1 /x]) = T rue M σ (φ[s 2 /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 3.8 M σ(x a) (ψ) = T rue M σ ( xψ) = T rue. 5
( E).. (A 1) xψ ρ [ψ[y/x]]. (A 2) ρ ( E) Γ 1, Γ 2 Γ A 1, A 2. A 1 Γ 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]}. A 2 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 = s i )) = T rue. a M σ(x a) (t i ) = M σ(x a) (s i ). 3.10 M σ(x a) (s i ) = M σ(y a) (s i [y/x]), M σ(x a) (t i ) = M σ(y a) (s i [y/x]). a Mx σ (t i ) My σ (s i [y/x]).,, M σ (F (x(t 1 t i t n )t 1 t m)) = M σ (F (x(s 1 s i s n )t 1 t m)) M σ (F (x(t 1 t n )t 1 t m) = F (y(s 1 [y/x] s n [y/x])t 1 t m)) = T rue.. 4.2 4.2 ( ) Γ, φ. Γ = φ = Γ φ. [1],.,.,,. 6
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 Term F,B ψ[s/x] Γ xψ Γ s Term F,B ψ[s/x] Γ 7
Γ Fomula F,B Γ Γ + Γ +. Fomula F,B, φ 1, φ 2,. Γ 0 = Γ, Γ n. Γ n Γ n+1 = Γ n { xψ, ψ[y/x]} Γ n {φ n+1 } ((Γ n {φ n+1 } ) ) Γn {φ n+1 } φ n+1 xψ ( ) ( y Γ n xψ F ) Γ + = n=1 Γ n,. Term F,B t s def t = s Γ +, D. t [[t]].. f M ([[t 1 ]],..., [[t n ]]) := [[ft 1 t n ]] p M ([[t 1 ]],..., [[t n ]]) = T rue pt 1 t n Γ +, 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 T g,x, g x. 4.9 M F F M ( x F M ((g 1,..., g n ), ([[t 1]],..., [[t [[F (x(t m]])) = g1,x T gn,x)t 1 t m)]] g i [[y]] (otherwise) ) ( y F ) well-defined..,. 4.10 T gi,x g i x, T g g i,y i y,. [[F (x(t g1,x T gn,x)t 1 t m)]] = [[F (y(t g 1,y T g n,y)t 1 t m)]] 8
Proof. T g1,x,..., T gn,x, T g 1,y,..., T g n,y, B z. z T g1,x,..., T gn,x x, T g 1,y,..., T g n,y y. 3. [[F (x(t g1,x T gn,x)t 1 t m)]] = [[F (z(t g1,x[z/x] T gn,x[z/x])t 1 t m)]] (4.1) [[F (y(t g 1,y T g n,y)t 1 t m)]] = [[F (z(t g 1,y[z/y] T g n,y[z/y])t 1 t m)]] (4.2) [[F (z(t g1,x[z/x] T gn,x[z/x])t 1 t m)]] = [[F (z(t g 1,y[z/y] T g n,y[z/y])t 1 t m)]] (4.3) (4.1) x(t gi,x = T gi,x), Γ + x(t gi,x = T gi,x). 4.6, x(t gi,x = T gi,x) Γ +. z T gi,x x,, Γ + F (x(t g1,x T gn,x)t 1 t m) = F (z(t g1,x[z/x] T gn,x[z/x])t 1 t m), 4.6 F (x(t g1,x T gn,x)t 1 t m) = F (z(t g1,x[z/x] T gn,x[z/x])t 1 t m) Γ +. (4.1). (4.2). (4.3) T gi,x, T g i,y g i x, y, s Term F,B, [[T gi,x[s/x]]] = [[T g i,y[s/y]]]. z T gi,x x T g i,y y, [[T gi,x[z/x][s/z]]] = [[T g i,y[z/y][s/z]]], T gi,x[z/x][s/z] = T g i,y[z/y][s/z] Γ +., s, 4.7(6), z(t gi,x[z/x] = T g i,y[z/y]) Γ +., Γ + F (z(t g1,x[z/x] T gn,x[z/x])t 1 t m) = F (z(t g 1,y[z/y] T g n,y[z/y])t 1 t m). 4.6 F (z(t g1,x[z/x] T gn,x[z/x])t 1 t m) = F (z(t g 1,y[z/y] T g n,y[z/y])t 1 t m) Γ + (4.3). M, σ, x F σ(x) = [[x]]. M, σ Γ. σ. 9
4.11 x 1,..., x n B. FVar(s) F {x 1,..., x n }, BVar(s) B s M σ (s) = [[s ]] σ(x i ) = [[t i ]] (t i Term F,B ) [t 1 /x 1 ][t 2 /x 2 ] [t n /x n ]. Proof. s.. 1,1-.,. M σ (F (x(t)t )) = F M (Mx σ (t), M σ (t )) = F M (Mx σ (t), [[t ]]) Mx σ (t). x, a Term F,B,. Mx σ (t)([[a]]) = M σ(x [a ]) (t) = [[t [a/x]]] ( ), t Mx σ (t) x., M σ (F (x(t)t )) = F M (Mx σ (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) φ pt 1 pt n, pt 1 pt n Γ + p M ([[t 1 ]],..., [[t n ]]) = T rue p M (M(t 1 ),..., M(t n )) = T rue ( 4.11) M σ (pt 1 pt n ) = T rue (iv) φ ψ, ψ 1 ψ 2, ψ 1 ψ 2, ψ 1 ψ 2, 4.7. 10
(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äänänen, Jouko. Second-order logic and foundations of mathematics. Bulletin of Symbolic Logic 7.4 (2001): 504-520. 11