数学ノート 2018-

Save this PDF as:
 WORD  PNG  TXT  JPG

Size: px
Start display at page:

Download "数学ノート 2018-"

Transcription

1 (Sakaé Fuchino) I 2 II I I II 2012 update : (02:14JST)

2 download fml-6 3 2

3 I II A Th( Q, < ) Th( N, S, 0 ) Presburger Th( R, +,, 0, 1 )

4

5 I parti 1 introduction (symbolic logic) (mathematical logic) (foundation of mathematics) 1) : A. ( (logical system)) Gottfried Wilhelm von Leibniz (1646( 23 ) ( 1 )) (Leibniz ) Ernst Schröder (1841( 12 ) ( 35 )) Friedrich Ludwig Gottlob Frege (1848( 1 ) ( 14 )) 1) 5

6 2) Hilbert Paul Bernays (1888( 21 ) ( 52 )) 1 2 B. Hilbert Ackermann 1928 [5] ([4] ) C. Yes: Kurt Gödel (1906( 39 ) 1978( 53 )) (Completeness Theorem, 1929) I 8 D. : 3.6 () E. David Hilbert ( , 2 18 ) ( Hilbert ) F () E. Kurt Gödel ( ) (Incompleteness Theorems, l931) 15 2) Boole, de Morgan, Dodgeson (Luis Carrol), Russel l9 20 Peano 6

7 G. E.... [9], [11] II [1] : (2011). [2] H.-.D. Ebbinghaus J. Flum, W. Thomas: Einfürung in die mathematische Logik, Wissenschaftsverlag (1992, ). [3] Herbert B. Enderton, A Mathematical Introduction to Logic, Second Edition, Academic Press (2001). [4] G. Gentzen, Untersuchungen über das logische Schließen, Mathematische Zeitschrift. 39 (1934), , [5] D. Hilbert and W. Ackermann, Grundzüge der theoretischen Logik, Springer- Verlag (1928/1972). [6] : (1996). [7] : (1977). [8] Joseph R. Shoenfield, Mathematical Logic, A K Peters/CRC Press; 2Rev Ed. (1967/2001). [9] G. Takeuti, Two applications of Logic, Iwanami Shoten & Princeton University Press (1978). [10] : (1956/1974). [11] : 2 (1997). [12] : (2012). 7

8 1.1 φ x y(( z(z z + x z + y > 0) z(0 > z z + x z + y)) z(z z + x z + y 0)) (formula) x : for all x holds y : there exists x such that : and : implies 3) φ R, 0, + R, R, < R 4) R, 0, + R, R, < R = φ Q, 0, + Q, Q, < Q Q, 0, + Q, Q, < Q = φ 2 1 pred-logic x y(( z(z z + x z + y < 0) z(0 < z z + x z + y)) z(z z + x z + y 0)) : 0 : +, 3) objects = 4) + R, R, < R R + Q, Q, < Q Q 8

9 : < : : x, y, z :, :, : (, ),...,, ( ), : : x, y, z, x 0, x 1,..., etc. :,,, :, : (, ),, x, y, z x, y, z etc. L (language) L (constant symbol) (function symbol) 9

10 (relation symbol) L (arity) L L + L z z + x z + y L- (L-term) : (2.1) L ( 1 ) L-; term-0 (2.2) f L n-t 1,..., t n L-f(t 1,..., t n ) L- term-1 (2.3) L- (2.1) (2.2) term-2 (2.3) f 2 + +(t 1, t 2 ) (t 1 + t 2 ) t 1 + t 2 z z + x z + y ((z z) + (x z)) + y, z (((z + x) z) + y) + ((z z) + (x z)) + y L- t t (closed term) L- (closed L-term) L (( (( 1 + 1) + 1) + ) + 1 ) }{{} n 1 L 1 + n L- t x 1,..., x n t = t(x 1,..., x n ) 10

11 5) x 1,..., x n t L- L- L L- (L-structure) : L = {c i : i I} {f j : j J} {r k : k K} c i, f j, r k L f j m j - r k n k - A L- A A = A, c A i, fj A, rk A i I,j J,k K A c A i, i I A j J f j A : A m j A k K r k A A n k- (r k A Am k ) c A i, fj A, rk A A c i, f j, r k t = t(x 1,..., x n ) L- t(x 1,..., x n ) A t A (x 1,..., x n ) : A n A L- 6) (2.4a) t c i term-3 t A (x 1,..., x n ) : A n A ; a 1,..., a n c i A ; (2.4b) t x i (1 i n) t A (x 1,..., x n ) : A n A ; a 1,..., a n a i ; (2.5) t f j (t 1,..., t mj ) term-5 5) x 1,..., x n V ar V ar x 1,..., x n 6) (2.4a) (2.4b), (2.5) L- (2.1) (2.2) (2.3) (2.4a) (2.4b), (2.5) L- t = t(x 1,..., x n ) t A (x 1,..., x n ) 11

12 t A (x 1,..., x n ) : A n A ; a 1,..., a n f j A (t A 1 (x 1,..., x n )(a 1,..., a n ),..., t A m j (x 1,..., x n )(a 1,..., a n )) 2.1 L 2 +, 1 R = R, + R, R, 1 R,... + R R 1 R 1 L- t(x, y) x x + y + 1 t R (x, y) 2 t R (x) : R 2 R ; r, s r 2 + s + 1 t A (x 1,..., x n ) x 1,..., x n L- (2.1) (2.3) : 2.1 t L-x 1,..., x n l 1,..., l k (k n) 1, 2,..., n t = t(x l1, x l2,..., x lk ) t = t(x 1,..., x n ) L- A = A,... a 1,..., a n A term-a-i t A (x 1,..., x n )(a 1,..., a n ) = t A (x l1,..., x lk )(a l1,..., a lk ) L- t L-a 1,..., a n A t c i (2.4a) t A (x 1,..., x n )(a 1,..., a n ) = c A i = t A (x l1,..., x lk )(a l1,..., a lk ) t x i t = t(x l1, x l2,..., x lk ) i l 1,..., l k (2.4b) t A (x 1,..., x n )(a 1,..., a n ) = a i = t A (x l1,..., x lk )(a l1,..., a lk ) 12

13 t f j (t 1,..., t mj ) t 1,..., t mj (2.5) t A (x 1,..., x n )(a 1,..., a n ) = f A j (t A 1 (x 1,..., x n )(a 1,..., a n ),..., t A m j (x 1,..., x n )(a 1,..., a n )) = 7) f A j (t A 1 (x l1,..., x lk )(a l1,..., a lk ),..., t A m j (x l1,..., x lk )(a l1,..., a li )) = t A (x l1,..., x lk )(a l1,..., a lk ) L- (L-formula) : (2.6) t 1, t 2 L- t 1 t 2 L- ; fml-0 (2.7) t 1,..., t n L- r L n-r(t 1,..., t n ) L- fml-1 ; (2.8) φ, ψ L- φ, (φ ψ), (φ ψ), (φ ψ) L- fml-2 ; (2.9) φ L-x 1 xφ, xφ L- fml-3 ; (2.10) fml-4 (2.6) (2.7) (atomic formula) φ (2.8) φ (literal) xφ xφ x φ, x x φ x b f(x)dx x a (bounded variable) (free variable) 8) x V ar φ φ i x 7) 8)

14 φ i x φ : φ xψ xψ φ i x x φ : i x φ i x φ L- φ x 1,..., x n φ = φ(x 1,..., x n ) x 1,..., x n φ () Fml L L- Fml L = {φ : φ L- } L- L- (L-sentence) Sent L L- Sent L = {φ : φ L- } L- L- V ar V ar L L- φ L- A = A,... φ A L-A L- A V ar A I I (V ar A ) (interprepation) L- A = A,... φ I (A, I) = φ 14

15 : I : V ar A x V ar a A I x,a : V ar A v V ar I(v) v x I x,a (v) = a v x 9) (2.11) L- t 1 = t 1 (x 1,..., x n ), t 2 = t 2 (x 1,..., x n ) φ t 1 t 2 fml-5 (A, I) = φ t A 1 (I(x 1 ),..., I(x n )) = t A 2 (I(x 1 ),..., I(x n )); (2.12) k- r L- t 1 = t 1 (x 1,..., x n ),..., t k = t k (x 1,..., x n ) fml-6 φ r(t 1,..., t k ) (A, I) = φ r A (t A 1 (I(x 1 ),..., I(x n )),..., t A k (I(x 1 ),..., I(x n ))); (2.13) L- θ, η fml-7 (a) φ θ η (A, I) = φ (A, I) = θ (A, I) = η; (b) φ θ η (A, I) = φ (A, I) = θ (A, I) = η; (c) φ θ (A, I) = φ (A, I) = θ ; (d) φ θ η (A, I) = φ (A, I) = θ (A, I) = η; (2.14) L- θ fml-8 (a) φ xθ (A, I) = φ a A (A, I x,a ) = θ ; (b) φ xθ (A, I) = φ a A (A, I x,a ) = θ. 2.1 : 2.2 φ = φ(x 1,..., x n ) L- A = A,... L- I : V ar A, I : V ar A I(x 1 ) = I (x 1 ),..., I(x n ) = I (x n ) (A, I) = φ (A, I ) = φ 9) I x,a I x a formula-a-i 15

16 2.2 φ = φ(x 1,..., x n ) (A, I) = φ I(x 1 ),..., I(x n ) a 1,..., a n A A = φ(a 1,..., a n ) (2.15) I(x 1 ) = a 1,..., I(x n ) = a n I : V ar A fml-8-0 (A, I) = φ φ L- L- (A, I) = φ I I A = φ A L- Th(A) = {φ Sent L : A = φ} Th(A) A 1 ((first order) theory) Th(A) A A = A, A 10) Th(A) A Q, < R, < 11) Th( Q, < ) = Th( R, < ) A Th(A) A L = {+,, 0, 1} L- x(x x = 1 + 1) φ R = R, + R, R, 0, 1, Q Q, + Q, Q, 0, 1 R = φ Q = φ Th(R) Th(Q) 3 L- L- T L- A L- A = T T L- φ A = φ A = T A T theorys-and-models 10) A A = A, A A 11) p.18 16

17 φ = φ(x 1,..., x n ) L- x 1 x n φ(x 1,..., x n ) L- L- φ - forall-closure T - T φ = φ(x 1,..., x n ) L- L- A A = T T A A = x 1 x n φ T = φ φ T L- T (consequences) Cn L (T ) Cn L (T ) = {φ Sent L : T = φ} L- A Th(A) = {φ Sent L : A = φ} L- T Th(A) Cn L (T ) = Th(A) T Th(A) (axiomatization) L n N \ {0} L- φ n x 1 x n ( 1 i<j n x i x j ) finite-str-inf-str-isom x i x j x i x j L- φ i,j, 1 i < j n ) ( φ 1 i<j n i,j 1 i < j n φ i,j L- A = A,... A = φ n A n L- T T = {φ n : n N \ {0}} 12) L- A = A,... A = T A 12) N = {0, 1, 2, 3,...} N \ {0} {0} N \ {0} = {1, 2, 3,...} 17

18 A A = A,... A L L- A T L L- L- n A A n : 3.2 L n N \ {0} L- φ n! (( ) ( )) x 1 x n x 1 i<j n i x j x x x 1 i n i ) L- φ i, 1 < i < n ( φ 1 i n i n-factorial A = φ n! A n φ = φ(x, y 1,..., y k ) x 1,..., x n φ n xφ (( ) ( )) x 1 x n x 1 i<j n i x j φ(x 1 i n i, y 1,..., y k ) L- A = A,... a 1,..., a k A A = n xφ(a 1,..., a k ) A = φ(a, a 1,..., a k ) a A n φ(a, a 1,..., a k ) a A n n! xφ n, m N\{0} φ n!, φ m! T = {φ n!, φ m! } 1 T T T T L = {c i : i I} {f j : j J} {r k : k K} A = A, c A i, f A j, r A k i I,j J,k K, B = B, c B i, f B j, r B k i I,j J,k K L- isomorphic A B g : A B : 18

19 (3.1) g A B 1 1 ; (3.2) i I g(c A i ) = c B i ; (3.3) j J a, a 1,..., a mj A f A j (a 1,..., a mj ) = a f B j (g(a 1 ),..., g(a mj )) = g(a); (3.4) k K a 1,..., a nk r A k (a 1,..., a nk ) r B k (g(a 1 ),..., g(a nk )). g A B A B L- id A : A A A A A A A B A = B : 3.1 L A = A,... B = B,... L- g : A B A B L- φ = φ(x 0,..., x n 1 ) a 0,..., a n 1 A isomorphic-str A = φ(a 0,..., a n 1 ) B = φ(g(a 0 ),..., g(a n 1 )) φ φ 3.2 L, A, B, g : A B 3.1 L- t = t(x 0,..., x n 1 ) g(t A (a 0,..., a n 1 )) = t B (g(a 0 ),..., g(a n 1 )) t 3.3 L L- A L- φ A L- B finite-structures 19

20 B = A B = φ A A : L- A φ A 3.3 L 2 r A = A, r A L- A = {a 0,..., a n 1 } a 0,..., a n 1 L- φ : ( ( ) ( ) x 1 x n x i<j<n i x j x x x i<n i ( ) ( ) ) r(x i,j<n, i,j r A i, x j ) r(x i,j<n, ij r A i, x j ) φ x 1 x n φ 0 φ x 1 x n φ 0 φ φ!n B = B,... L- B = φ b 1,..., b n B B = φ 0 (b 1,..., b n ) φ 0 B = {b 1,..., b n } g : A B g(a i ) = b i, 1 i n φ 0 g 1 1 φ 0 A B α 1, α 2 - ex-of-theories 3.3 L = {<} < 2 (dense linear order without end-points) T DLO α 1,..., α 6 T DLO = {α 1,..., α 6 } α 1 : x < y y < z x < z α 4 : x < y z (x < z z < y) α 2 : (x < x) α 5 : y (y < x) α 3 : x < y y < x x y α 6 : y (x < y). 20

21 R, < R Q, < Q T DLO Cn L (T DLO ) = Th( R, < R ) = T h( Q, < Q ) (Tarski ) L = {β, δ} β 3 δ 4 β(x, y, z) δ(x, y, x, y ) y x z xy x y A1 A13 : A1: β(x, y, x) x y A2: (β(x, y, u) β(y, z, u)) β(x, y, z) A3: (β(x, y, z) β(x, y, u) x y) (β(x, z, u) β(x, u, z)) A4: δ(x, y, y, x) A5: δ(x, y, z, z) x y A6: (δ(x, y, z, u) δ(x, y, v, w)) (z, u, v, w) A7: (Pasch ) v((β(x, t, u) β(y, u, z)) (β(x, v, y) β(z, t, v))) A8: (Euclid ) v w((β(x, u, t) δ(y, u, z) x u) (β(x, z, v) β(x, y, w) β(v, t, w))) A9: (δ(x, y, x, y ) δ(y, z, y, z ) δ(x, u, x, u ) δ(y, u, y, u ) β(x, y, z) β(x, y, z) x y) δ(z, u, z, u ) A10: z(β(x, y, z) δ(y, z, u, v)) A11: x y ( β(x, y, z) β(y, z, x) β(z, x, y)) A12: (δ(x, u, x, v) δ(y, u, y, v) δ(z, u, z, v) u u) (β(x, y, z) β(y, z, x) β(z, x, y)) A13: L- φ = φ(x, v, w,...), ψ = ψ(y, v, w,...) ( y, z, u φ x, z, u ψ ): z x y((φ ψ) β(z, x, y)) u x y((φ ψ) β(x, u, y))) 3.5 Peano L PA = {0, S, +, } 0 S

22 S(x) x x + 1 p 1, p 2, p 3,, T PA = {p 1, p 2, p 3, a 1, a 2, m 1, m 2 } {p φ : φ(x, x) Fml L } T PA Peano (Peano arithmetic) T PA p 1 : x y S(x) S(y) p 3 : x 0 y (S(y) x) p 2 : 0 S(x) a 1 : x + 0 x m 1 : x 0 0 a 2 : x + S(y) S(x + y) m 2 : x S(y) (x y) + x T PA p φ φ p φ : φ(0, x) x (φ(x, x) φ(s(x), x)). x φ(x, x) N = N, 0 N, +1, +, T PA 0 S k- S k (0) S k (0) = S( (S( 0 )) ) }{{}}{{} k k T PA f : N k N L PA - φ f = φ f (x 0,..., x k ) a 0,..., a k 1 N k f(a 0,..., a k 1 ) = b T = φ f (S a 0 (0),..., S a k 1 (0), b) PA Th(N) Cn LPA (PA) Th(N) T T Th(N) T Th(N) ( 12, 15 ) 3.6 (Zermelo-Fraenkel ) E. Zermelo A. Fraenkel ZF ZF 22

23 13) : L = {ε} ε 2 ZF ZF = {,,,,,, } { φ, φ : φ Fml L } 14) () () L- : : z (zεx zεy) x y z t (t εz) : z t (tεz t x t y) : s t [tεs y (yεx tεy)] φ, ψ φ ψ ((φ ψ) (ψ φ)) t εz tεz z x y (yεz yεx) x u (uεx) {x}, x y L- : p t [tεp t x] : : x [ y (yεx y ) t (tεx t {t}εx)] x [x y (yεx z (zεy z εx))] φ(y, x 1,..., x n ) = φ(y, x) L- φ : s t [tεs tεx φ(t, x)] φ(x, y, x) Fml L 13) Zermelo Fraenkel Skolem 14) (informal ) xεy ( ) x ( ) y 23

24 φ : x [xεa y φ(x, y, x)] x y y [φ(x, y, x) φ(x, y, x) y y ] b y [yεb x (xεa φ(x, y, x))]. ZF ZF [1] A. Tarski, What is elementary geometry?, Proceedings of an International Symposium held at the Univ. of Calif., Berkeley, Dec. 26, 1957 Jan. 4, 1958, Studies in Logic and the Foundations of Mathematics, Amsterdam, North- Holland (1959), [2] K. Kunen, Set-theory, North-Holland (1983) (2.8) (φ ψ) 4.1 L φ L- (1) φ L- φ 0, φ 1, φ 0, φ 1 φ = (φ 0 φ 1 ), φ = (φ 0 φ 1) φ 0 = φ 0, φ 1 = φ 1 addendum unambiguity unambiguous (2) φ L- φ 0, φ 1, φ 0, φ 1 φ = (φ 0 φ 1 ), φ = (φ 0 φ 1) φ 0 = φ 0, φ 1 = φ 1 24

25 (3) φ L- φ 0, φ 1, φ 0, φ 1 φ = (φ 0 φ 1 ), φ = (φ 0 φ 1) φ 0 = φ 0, φ 1 = φ L φ ψ L-φ == ψ L A V ar A I (A, I) = φ (A, I) = ψ φ == ψ φ ψ φ ψ L A V ar A I (A, I) = φ ψ φ == ψ φ ψ () == Fml L : minimal-setting 4.1 L φ, ψ, η L- (1) φ == φ; (2) φ == ψ ψ == φ ; (3) φ == ψ ψ == η φ == η L (2.11) (2.14) : 4.2 L φ ψ L- abbrev-0 (1) (φ ψ) == ( φ ψ); (2) (φ ψ) == (φ ψ); (3) xφ == x φ. L Φ : Fml L Fml L : (4.1) φ Φ(φ) = φ; fml-9 (4.2a) φ ψ Φ(φ) = Φ(ψ); fml-10 (4.2b) φ φ 0 φ 1 Φ(φ) = ( Φ(φ 0 ) Φ(φ 1 )); (4.2c) φ φ 0 φ 1 Φ(φ) = (Φ(φ 0 ) Φ(φ 1 )); 25

26 (4.3a) φ xψ Φ(φ) = xφ(ψ); fml-11 (4.3b) φ xψ Φ(φ) = x Φ(ψ). φ Φ(φ),, 4.3 L Φ : Fml L Fml L L- φ φ == Φ(φ) abbrev-1,,,,,,, φ,, Ψ(φ),,,,,,,, 4.4 L φ, ψ, η L-: (1) ((φ ψ) η) == (φ (ψ η)); (2) ((φ ψ) η) == (φ (ψ η)). 4.4 ((φ ψ) η) (φ (ψ η)) (φ ψ η) φ 0,..., φ n 1 φ 0 φ n 1 i<n φ i, {φi : i < n} : 4.5 φ, ψ, η ((φ ψ) η) == (φ (ψ η)) and-and 4.3 subformula 26

27 L L- φ SubF ml(φ) φ φ (4.4) L- t 1, t 2 φ t 1 t 2 SubF ml(φ) = subfml-1 {φ} ; (4.5) L- t 1,..., t n L n- r φ r(t 1,..., t n ) subfml-2 SubF ml(φ) = {φ} ; (4.6) L- φ 1, φ 2 SubF ml(φ 1 ), SubF ml(φ 2 ) subfml-3 (a) φ φ 1 SubF ml(φ) = SubF ml(φ 1 ) {φ} ; (b) φ φ 1 φ 2, φ 1 φ 2, φ φ 2 SubF ml(φ) = SubF ml(φ 1 ) SubF ml(φ 2 ) {φ} ; (4.7) L- ψ SubF ml(ψ), φ xψ subfml-4 xψ SubF ml(φ) = SubF ml(ψ) {φ} L- φ, ψ ψ φ (subformula) ψ SubF ml(φ) L- t L- φ freev ar(t), freev ar(φ) L- t freev ar(t) : (4.8a) t freev ar(t) = ; freevar-0 (4.8b) t x V ar freev ar(t) = {x} ; (4.9) L- t 1,..., t n L n- f t = f(t 1,..., t n ) freevar-1 freev ar(t 1 ),..., freev ar(t n ) freev ar(t) = freev ar(t 1 ) freev ar(t n ) L- t freev ar(t) {x 1,..., x n } t = t(x 1,..., x n ) L- φ freev ar(φ) : 27

28 (4.10) L- t 1, t 2 φ t 1 t 2 freev ar(φ) = freevar-1 freev ar(t 1 ) freev ar(t 2 ) ; (4.11) L- t 1,..., t n L n- r φ r(t 1,..., t n ) freevar-2 freev ar(φ) = freev ar(t 1 ) freev ar(t n ) ; (4.12) L- φ 1, φ 2 freev ar(φ 1 ), freev ar(φ 2 ) freevar-3 (a) φ φ 1 freev ar(φ) = freev ar(φ 1 ) ; (b) φ (φ 1 φ 2 ), (φ 1 φ 2 ), (φ φ 2 ) freev ar(φ) = freev ar(φ 1 ) freev ar(φ 2 ) ; (4.13) L- ψ freev ar(ψ), φ xψ freevar-4 xψ freev ar(φ) = freev ar(ψ) \ {x} L- φ freev ar(φ) {x 1,..., x n } φ = φ(x 1,..., x n ) L- φ L- freev ar(φ) = (propositional logic) : normal-form sentential-logic (5.1) : A 1, A 2,..., B 1, B 2,..., etc. (5.2) :,,, (5.3) : (, ) (5.4) ; 28

29 (5.5) φ, ψ (φ ψ), (φ ψ), φ, (φ ψ) ; (5.6) φ A 1,..., A n φ = φ(a 1,..., A n ) A 1,..., A n 2 = {0, 1} 1 0 (true) (false) on off f n f : 2 n 2 f 2 2 n 2 n = { i 1,..., i n : i 1,..., i n 2} φ = φ(a 1,..., A n ) f φ(a1,..., A n) : 2 n 2 : (5.7) φ A i (1 i n) p 1,..., p n 2 f φ(a1,..., A n)(p 1,..., p n ) = p i ; (5.8) a-0 (a) φ (ψ 0 ψ 1 ) p 1,..., p n 2 1, f ψ0 (A 1,..., A n)(p 1,..., p n ) = 1 f φ(a1,..., A n)(p i,..., p n ) = f ψ1 (A 1,..., A n)(p 1,..., p n ) = 1 ; 0, ; (b) φ (ψ 0 ψ 1 ) p 1,..., p n 2 1, f ψ0 (A 1,..., A n)(p 1,..., p n ) = 1 f φ(a1,..., A n)(p 1,..., p n ) = f ψ1 (A 1,..., A n)(p 1,..., p n ) = 1 ; 0, ; (c) φ ψ 0 p 1,..., p n 2 1, f ψ0 (A 1,..., A n)(p 1,..., p n ) = 0 f φ(a1,..., A n)(p 1,..., p n ) = 0, ; 29

30 ; (d) φ (ψ 0 ψ 1 ) p 1,..., p n 2 1, f ψ0 (A 1,..., A n)(p 1,..., p n ) = 0 f φ(a1,..., A n)(p 1,..., p n ) = f ψ1 (A 1,..., A n)(p 1,..., p n ) = 1 ; 0, A 1,..., A n φ = φ(a 3, A 1 ) φ φ = φ(a 1, A 2, A 3 ) p 1, p 2, p 3 2 f φ(a1,a 2,A 3 )(p 1, p 2, p 3 ) = f φ(a3,a 1 )(p 3, p 1 ) 5.1 k n 1 i 1,..., i k n prop-l-0 φ = φ(a i1,..., A ik ) φ φ = φ(a 1,..., A n ) p 1,..., p n 2 f φ(a1,..., A n)(p 1,..., p n ) = f φ(ai1,..., A ik )(p i1,..., p ik ) φ,, (6.1 ) I PropVar I : PropVar 2 I A I(A) I φ = φ(a 1,..., A n ) I = φ f φ(a1,..., A n)(i(a 1 ),..., I(A n )) = 1 30

31 I = φ I φ I φ 5.1 A 1,..., A n = φ I I = φ = φ φ (universally valid) φ (tautology) 5.2 φ = φ(x 1,..., x n ) L φ 1 = φ 1 (x 1...x m ),..., φ n = φ n (x 1,..., x m ) L- A = A,... L- a 1,..., a m A 0 < k < n 1, A = φ k (a 1,..., a m ) i k = 0, prop-l-1 A = φ(φ 1,..., φ n )(a 1,..., a m ) f φ(x1,..., x n)(i 1,..., i n ) = φ = φ(x 1,..., x n ) L φ 1 = φ 1 (x 1...x m ),..., φ n = φ n (x 1,..., x m ) L- L- A prop-l-2 A = x 1 x m φ(φ 1,..., φ n ) φ = φ(a 1,..., A n ) ψ = ψ(a 1,..., A n ) φ == ψ (φ φ functionally equivalent) f φ(a1,..., A n) = f ψ(a1,..., A n) L- φ, ψ φ == ψ L- A A = φ A = ψ (4.2 ) 5.4 φ = φ(a 1,..., A n ) ψ = ψ(a 1,..., A n ) φ == ψ L η 1,..., η n Fml L φ(η 1,..., η n ) == ψ(η 1,..., η n ) 5.2 φ 31

32 5.3 φ(φ 1,..., φ n ) Fml L φ φ φ = φ(a 1,..., A n ) 2 n p 2 n f φ(a1,..., A n)(p) = 1 ψ Fml L φ φ 1,..., φ n Fml L ψ = φ(φ 1,..., φ n ) φ φ ((A 1 A 2 ) A 3 ) f φ(a1,a 2,A 3 ) : sentential-logic-a functional-completeness A 1 A 2 A 3 (A 1 A 2 ) ((A 1 A 2 ) A 3 ) ((A 1 A 2 ) A 3 ) (A 1 A 2 ) ((A 1 A 2 ) A 3 ) φ 1, φ 2, φ 3 (φ 1 φ 2 ) == (φ 1 φ 2 ) ((φ 1 φ 2 ) φ 3 ) == (φ 1 (φ 2 φ 3 )) functionally equivalence ( ) (6.1) ((φ 1 φ 2 ) φ 3 ) (φ 1 φ 2 φ 3 ) i {1,2,3} φ i, {φ i : i b-a {1, 2, 3}} 32

33 t 2 n φ t(a 1,..., A n ) 0<i n φ t,i φ t,i = A i t i entry 1 A i f φ t(a 1,..., A n) f φ t(a 1,..., A n)( s) = 1 s = t f : 2 n 2 φ f = φ f (A 1,..., A n ) {φ t : t 2 n, f( t) = 1} f 0 φ f A 1 A 1 f = f φf (A 1,..., A n) ( ) : 6.1 f : 2 n 2,, φ = φ(a 1,..., A n ) f = f φ(a1,..., A n) func-comp-1 {,, } (functionally complete) φ, ψ (φ ψ) == ( φ ψ) (φ ψ) == ( φ ψ) ( ) {, } {, } (φ ψ) == ( φ ϕ) ( ) 6.3 {, } {,, },, φ = φ(a 1,..., A n ) f φ(a1,..., A n)(1, 1,..., 1) = 1 ( 1, 1,..., 1 1 n ),, 33

34 6.2 T T (satisfiable) sentential-compactness I : PropVar 2 φ T I = φ T (finitely satisfiable) T T T T ( ) 6.4 T φ T comp-1 T {φ} T { φ} T T {φ} T { φ} T T, T T T {φ} T { φ} T T T I : PropVar 2 I = T T I = φ I T {φ} T {φ} I = φ (5.8), (c) I = φ I = T { φ} T { φ} comp ( ) T T T PropVar 15) PropVar A 1, A 2, A 3,... (PropVar ) T n, n N (6.2) T 0 = T ; a-1 15) (Prime Ideal Theorem) (ZF) T ( PropVar ) PropVar (ZF ) 2 ( PropVar ) ( ) 34

35 (6.3) T n {A n+1 } T n+1 = T n {A n+1 } a-2 T n+1 = T n { A n+1 } 6.4 T n T = n N T n Claim T T T n N T T n T n T Claim n N A n+1 T A n+1 T A n+1 T A n+1 T n+1 (6.3) A n+1 T n+1 T A n+1, A n+1 T m A n+1, A n+1 T m {A n+1, A n+1 } T m I : PropVar 2 1, A n+1 T I (A n+1 ) = 0, I T Claim φ T I = φ n φ A 1, A 2,..., A n φ i, i = 1, 2,..., n A i, A i T φ i = A i, Weak König s Lemma 35

36 {φ, φ 1, φ 2,..., φ n } T I = {φ, φ 1, φ 2,..., φ n } I φ 1,..., φ n i = 1,..., n I(A i ) = 1 A i T I (A i ) = 1 I {A 1,..., A n } = I {A 1,..., A n } I = φ 5.1 I = φ 6.3 G, E G E G E appl-comp-thm ( ) x, y G x E y y E x () x G x E x G x E y x, y E 1 G, E ( G ) E G, E G G, E χ : G {1, 2,..., n} G n x, y G x E y χ(x) χ(y) n 2 G, E n χ Appel Haken 6.6 () (K. Appel and W. Haken, 1976) 4 36

37 ( ) 16) 4 G, E G, E G G x, y G x E y x E y 6.7 () G, E G, E 4 PropVar = {c x,i : x G, i {1, 2, 3, 4}} c x,i, x G, i {1, 2, 3, 4} c x,i x i T (6.4) T = {(c x,1 c x,2 c x,3 c x,4 ) : x G} a-3 {c x,i c x,j : x G, i, j {1, 2, 3, 4}, i j} {c x,i c y,i : x, y G, x E y, i {1, 2, 3, 4}}. T 1 1, 2, 3, T T I f : G {1, 2, 3, 4} f(x) = i I(c x,i ) = 1 f G, E 4 16) ( )

38 7 3 L T L-φ = φ(x 1,..., x n ) L- L- A A = T T A A = x 1 x n φ T = φ φ T φ T L- K 17) T φ T K T K φ : formal-system-of-proof (7.1) K (correct) 18) T K φ T = φ K-0 (7.2) K (complete) T = φ T K φ K-1 (7.3) T K φ φ T P K-2 P T P K φ T P P T φ T P K φ K T = φ T P K φ P P φ T K : K L K L A, R = A L, R L (L L ) A L- R p, φ p L- φ L- φ A φ K p R p K ρ = p, φ p = {φ 1,..., φ n } 17) K Kalkül logisches Kalkül 18) K (sound) 38

39 (ρ) φ 1,..., φ n φ K A, R L K L- Γ, L- P L- φ Γ P K φ P φ Γ K Γ K φ φ K Γ : L- P = φ 1,..., φ n φ Γ K (7.4) (7.5) : (7.4) φ n = φ; K-3 (7.5) 1 i n : K-4 (a) φ i A Γ (b) (p, ψ) R p {φ 1,..., φ i 1 } φ i = ψ. P φ Γ K Γ P K φ Γ K φ φ Γ K Γ P K φ P Γ P K φ n P Γ n K φ K n K n P K Γ P K φ, Γ K φ,... Γ P K φ, K φ,... Γ P K φ, Γ K φ,... L Γ P,L K φ, Γ L K φ,... (7.3) L L- L L- A R K K (7.1), (7.2), L L- Γ L- φ Γ K φ Γ = φ Γ K φ K K (7.1), (7.2), (7.3) K 39

40 K (7.1), (7.2), (7.3) φ 1,..., φ k, φ φ 1 φ k φ (φ 1 (φ 2 ( (φ k 1 (φ k φ)) ))) (φ ψ) φ ψ (2.9) 2 A = xφ A = x φ 4.2, 4.3 (2.9) φ xφ xφ x φ L 1 K 3 : 1. Fml L K 2. x, y, z, x 1, x 2,..., y 1, y 2,... K : (7.6) x x ; eq-a (7.7) x y y x ; eq-b (7.8) x y y z x z ; eq-b-0 (7.9) x 1 y 1 x n y n f(x 1,..., x n ) f(y 1,..., y n ), eq-c f L n ; (7.10) x 1 y 1 x n y n r(x 1,..., x n ) r(y 1,..., y n ), eq-d r L n. 3. () φ Fml L, x V ar, t L-φ x t y yψ φ t φ x φ(t/x) xφ K 19) 19) φ(t/x) φ x L- t 40

41 K : 1. () φ, ψ Fml L φ, φ ψ K ψ ; 2. () φ, ψ Fml L x V ar φ ψ K xφ ψ x ψ K (7.1), (7.2), (7.3) K P, n P K, n K L 1 L L-T L- φ, φ 0, φ 1,..., ψ, ψ 0,... L- 7.1 () T φ T = φ. soundness n n N \ {0} (7.11) T n φ T = φ soundness-0 n = 1 φ T φ T T = φ φ 5.3 T = φ φ T = φ φ = φ : φ α(t/x) α x t A = φ I : V ar A (A, I) = α(t/x) (A, I) = xα I : V ar A (A, I) = α(t/x) t = t(x 1,..., x k ) x α(t/x) φ = φ(x) φ x 41

42 a = t A (I(x 1 ),..., I(x k )) (A, I x,a ) = α (A, I) = xα A = φ n > 1 1 m < n (7.11) n m φ T n = 1 A = φ φ 1,..., φ n φ φ = φ n φ 1,..., φ n 1 φ i, j < n φ j = φ i φ φ i, φ i φ φ φ 1,..., φ i φ 1,..., φ j φ i φ j T i φ i, T j φ j A = T (7.12) A = φ i s-0 (7.13) A = φ i φ s-1 I : V ar A (7.13) (A, I) = φ i (A, I) = φ (7.12) (A, I) = φ i (A, I) = φ I : V ar A A = φ φ i < n φ i φ φ i η ν x x ν φ xη ν A T (A L- A = T ) I : A V ar (A, I ) = η ν (A, I x,a ) = η a A (A, I x,a ) = ν x ν (A, I) = ν (A, I) = x η ν a A (A, I x,a ) = η (A, I) = η (A, I) = x η ν 42

43 I A = x η ν A = φ K K (meta-theorem) 7.2 ( 7.3) 8.4, ( 8.5) implication 7.2 T φ 1 φ k φ T φ 1,..., T φ k T φ φ 1 φ k φ φ 1,..., φ k T φ T P 1 φ 1 φ k φ T P 2 T φ 1 T φ 1 φ k φ φ 1 (φ 2 φ k φ) φ 2 φ k φ φ 1 φ 1 φ k φ P 1 P 2 φ 2 φ k φ T φ 2 φ k φ 20) T φ P 1, P 2,..., T φ T {φ 1,..., φ k } φ T, φ 1,..., φ k φ 7.3 ( Deduction Theorem) (1) L- T L- Deduction-Thm φ, ψ T φ ψ T, φ ψ (2) φ L-T, φ ψ T φ ψ. 20) 2 S = s 1,..., s n, T = t 1,..., t m S T s 1,..., s n, t 1,..., t m 43

44 7.2 (1) φ ψ T ψ T {φ} ()(2) φ L- ψ T {φ} φ ψ T (1): φ 1,..., φ n φ ψ T φ n = φ ψ φ 1,..., φ n φ ψ T {φ} φ, φ 1,..., φ n, φ, ψ φ, φ ψ ψ ψ T {φ} (2): (1) n N \ {n} (7.14) φ L- T, φ n ψ T φ ψ reduction-0 n n = 1 ψ = φ ψ T ψ 1 φ = ψ φ ψ T φ ψ ψ T T ψ ψ (φ ψ) 21) T ψ (φ ψ) 7.2 T φ ψ 22) n > 1 1 m < n (7.14) P = φ 1,..., φ n ψ T {φ} P φ n = ψ 1 ψ n = 1 φ n 1 i, j < n φ j = φ i φ n φ 1,..., φ i T, φ φ i T φ φ i T φ φ i φ n 21) ψ (φ ψ) (A (B A)) A, B ψ φ (A (B A)) (A (B A)) 22) 7.2 k =

45 (φ φ i ) (φ φ i φ n ) (φ φ n ) 7.2 φ φ n (= φ ψ) T ψ = φ n 1 i < n φ i η ν φ n xη ν φ i φ n x ν T φ η ν (φ η ν) (η φ ν) T η φ ν 23) T xη φ ν ( xη φ ν) (φ xη ν) T φ ( xη ν), T φ ψ K (7.3) : 7.4 T L- φ L-T φ T T T φ endlichkeitssatz T P φ P P T T T T T P φ 8 K (7.2) : vollst-satz 8.1 () T = φ T φ T L- φ L- completeness 8.1 L- T L- φ T φ T T model-consis 23) φ L- 45

46 8.2 T T : T T T L- T x(x x) 7.1 T = x(x x) T A A = x(x x) = 8.3 L- T : inconsistent (a) T (b) L- φ T (φ φ) (c) T x x. (a) (b) T (b) (c): L- φ T (φ φ) (φ φ) x x 7.2 T x x (c) (a): T x x x x (7.6) x x x x (x x x x) T (x x x x) (b) (c) φ T φ 8.4 T φ T x 1 x n φ. n = 1 xφ x φ ( ): T φ y φ T, y y y φ T y y y φ ( y y y φ) ( φ y y y) T φ y y y vdash-forall (8.1) T x φ y y y all-0 ( x φ y y y) ( y y y x φ) (8.1) (8.2) T y y y x φ all-1 46

47 y y y (7.6) (8.2) x φ T x φ, T xφ ( ): T xφ y T, y y y x φ T y y y x φ ( y y y x φ) ( x φ y y y) T x φ y y y φ x φ ( φ x φ) ( x φ y y y) ( φ y y y) T φ y y y. ( φ y y y) ( y y y φ) T y y y φ ( ) T φ 8.5 ( Substitution Theorem) T φ L- t φ x T φ(t/x) subst-thm t φ φ(t/x) x φ ( φ(t/x) φ) ( x φ φ(t/x)) 7.2 (8.3) x φ φ(t/x) subst-0 T φ 8.4 (8.4) T x φ subst (8.3) (8.4) T φ(t/x) 8.6 ( 8.1) L- T T T completeness : φ = φ(x 1,..., x n ) = 8.4 T = φ T = x 1 x n φ T φ T x 1 x n φ 47

48 φ L- T φ T { φ} T { φ} T, φ φ T φ φ ( φ φ) φ 7.2 T φ 8.6 T { φ} T = φ T φ T = φ T L- 8.6 T : C L L C L 8.7 φ L- L-L T φ L ( T L φ ) T φ L ( T L φ ) : P = φ 1,..., φ n φ T L φ n = φ c 1,..., c m P C x 1,..., x m P m φ 1,..., φ n c 1,..., c m x 1,..., x m φ 1,..., φ n φ n = φ L- φ n = φ φ i T φ i = φ i P = φ 1,..., φ n L φ T V L = {Γ : Γ L- Γ } V L 8.7 V L V L 8.8 Γ, Γ i, i I L - (a) Γ V L L - φ Γ φ Γ {φ} V L (b) Γ V L Γ Γ Γ V L. (c) Γ V L Γ Γ Γ V L. V-L 48

49 (d) Γ i V L, i I i, j I Γ i Γ j Γ j Γ i i I Γ i V L. (e) Γ {(φ ψ)} V L Γ {φ} V L Γ {ψ} V L. (f) Γ V L L - φ Γ {φ} V L Γ { φ} V L (g) Γ V L Γ { xφ(x)} V L Γ {φ(c/x)} V L c Γ {φ(x)} ( C) Γ { xφ(x), φ(c/x)} V L (a): Γ V L Γ φ Γ {φ} V L Γ {φ} x x Γ {φ} P x x, Γ Q φ Q P x x Γ 8.3 Γ V L (b): Γ V L Γ x x Γ Γ Γ x x 8.3 Γ V L (c): (b) Γ Γ Γ V L Γ V L Γ x x 7.4 Γ Γ Γ x x 8.3 Γ V L (d): i I Γ i V L x x i I Γ i P P i 0 I P i I Γ i Γ i0 Γ i0 P x x Γ i0 V L (e): Γ {φ} V L Γ {ψ} V L Γ {φ} x x Γ {ψ} x x (8.5) Γ φ x x Γ ψ x x bbdv-0 (8.6) (φ x x) (ψ x x) (φ ψ x x) bbdv-1 (8.5), (8.6) 7.2 Γ φ ψ x x Γ {φ ψ} x x Γ {φ π} V L 49

50 (f): Γ {φ} V L Γ { φ} V L Γ {φ} x x Γ { φ} x x (8.7) Γ φ x x Γ φ x x bbdv-2 (8.8) (φ x x) ( φ x x) x x bbdv-3 (8.7), (8.8) 7.2 Γ x x Γ V L (g): Γ {φ(c/x)} V L Γ {φ(c/x)} x x Γ φ(c/x) x x P φ(c/x) x x Γ z P P c z P P φ(z/x) x x Γ P xφ(x) x x Γ Γ { xφ(x) x x} x x 8.3 Γ { xφ(x) x x} V L : Γ φ(c/x) xφ(x) Γ {φ(c/x)} xφ(x) Γ {φ(c/x)} V L (a) Γ { xφ(x), φ(c/x)} V L 8.9 T V L, T T (8.9) (8.11) : Henkin-extension (8.9) L - φ φ T φ T ; Henkin-0 (8.10) L - φ T φ φ T ; Henkin-1 (8.11) xφ T c C φ(c/x) T Henkin-2 50

51 (8.9) (8.11) T Henkin (Henkin theory) T T T Henkin T T Henkin (Henkin extension) 8.9 L - L - φ 0, φ 1, φ 2,... (8.12) L - φ Henkin-2-0 V L ( ) T 0 T 1 T 2 T 3 (8.13) (8.16) : (8.13) T 0 = T ; Henkin-3 (8.14) i N T i ( C) Henkin-4 ; (8.15) T i {φ i } V L Henkin-5 (a) φ i xψ(x) c T i {φ i } C T i+1 = T i {φ i, ψ(c)}; (b) φ i xψ(x) T i+1 = T i {φ i } (8.16) T i {φ i } V L T i+1 = T i { φ i }. Henkin-6 T i, i N (8.14) V L : 8.7 T V L (8.13) (8.14) T 0 (8.13) (8.15) (8.16) T i+1 T i T i+1 C n N (8.14) (8.15), (a) T i+1 V L 8.8, (g) (8.16) T i+1 V L 8.8, (f) T = i N T i 8.8, (d) T V L T (8.9) (8.11) 51

52 (8.9): φ L -φ T φ = φ i0 i 0 N φ i0 T i0 +1 T i0 +1 (8.16) φ = φ i0 T i0 +1 T (8.10): φ L - T φ 7.4 i 0 N T i0 φ (8.12) i 1 i 0 φ = φ i1 T i1 φ i1 T i1 {φ i1 } V L T i1 +1 (8.15) φ = φ i1 T i1 +1 T (8.11): xφ(x) T i 0 N xφ(x) T i0 i 1 i 0 xφ(x) = φ i1 (8.15), (a) φ(c) T i1 +1 T c C 8.13 Henkin T K : 8.10 L t, t, t, t 1,..., t n, t 1,..., t n L- (a) t t; (b) x(x t) x t ; (c) t t t t; (d) t t t t t t. (e) L n- f t 1 t 1 t n t n f(t 1,..., t n ) f(t 1,..., t n) ; terms (f) L n- r t 1 t 1 t n t n r(t 1,..., t n ) r(t 1,..., t n). (a): (7.6) ( 8.5) (b): φ = x t t t x(x t) (a) t t 7.2 x(x t) (c),(d), (e), (f): (7.7), (7.8), (7.9), (7.10), ( 8.5) 8.11 T Henkin Henkin-theory 52

53 (a) (b) c C c c T t, t, t L - t t, t t T t t T (c) t L - c C c t T c, c C c t, c t T c c T (d) c, c C t, t L - c t, c t T c c T t t T (e) t 1,..., t n, t 1,..., t n L-f n- t 1 t 1 T,..., t n t n T f(t 1,..., t n ) f(t 1,..., t n) T. (f) t 1,..., t n, t 1,..., t n L-r n- t 1 t 1 T,,..., t n t n T r(t 1,..., t n ) r(t 1,..., t n) T. (g) φ L - φ T φ T (h) φ, ψ L - φ ψ T (φ T ψ T ) (i) φ, ψ L - φ ψ T (φ T ψ T ) (j) φ, ψ L - φ ψ T (φ T ψ T ) (a): 8.10,(a) c c (8.10) c c T (b): (7.8) t t t t t t t t, t t T, T t t, T t t 7.2 T t t (8.10) t t T (c): 8.10,(b) (8.10) x(x t) T (8.11) c C c t T 8.10,(c),(d) c t c t c c c t, c t T 7.2 T c c (8.10) c c T (d): (c) (e): 8.10,(e), 7.2 (8.10) (f): 8.10,(f), 7.2 (8.10) (g) φ T (8.9) φ T φ T φ T T (φ φ) 8.3 T V L 53

54 (h): φ T ψ T φ T φ φ ψ 7.2 T φ ψ (8.10) φ ψ T φ T ψ T φ T ψ T (8.9) φ T ψ T φ ψ (φ ψ) 7.2 T (φ ψ) (g) φ ψ T (i), (j): (h) c, c C c c c c T 8.11,(a),(b) C c C [c] A = {[c] : c C} A L - A L D F, R c C c A = [c] d D 8.11,(c),(d) c d T c C c d A = [c] f F n- c 1,..., c n C n 8.11,(c) c f(c 1,..., c n ) T 8.11,(d), (e) c f A ([c 1 ],..., [c n ]) = [c] f A : A n A r R n- r A = { [c 1 ],..., [c n ] : r(c 1,..., c n ) T } (8.17) A = A, c A, f A, r A c D C, f F, r R A L - A T Henkin (Henkin model) 54

55 8.12 T T Henkin A Henkin Henkin-terms (a) t = t(x 1,..., x n ) L- c, c 1,..., c n C (8.18) c t(c 1,..., c n ) T [c] = t A ([c 1 ],..., [c n ]) Henkin-7 (b) t 1 = t 1 (x 1,..., x m ),..., t n = t n (x 1,..., x m ) L- c 1,..., c m C, r R n- (8.19) r(t 1 (c 1,..., c m ),..., t n (c 1,..., c m )) T Henkin-8 t A 1 ([c 1 ],..., [c m ]),..., t A n([c 1 ],..., [c m ]) r A (a): t t D (8.18) A m- f F t t = f(t 1 (x 1,..., x n ),..., t m (x 1,..., x n )) t 1 (x 1,..., x n ),..., t m (x 1,..., x n ) (8.18) 8.11, (c) c 1,..., c m C (8.20) c i t i (c 1,..., c n ) T, i = 1,..., m Henkin-9 (8.20) 8.10,(e), 7.2, (8.10) (8.21) t(c 1,..., c n ) f(c 1,..., c m) T Henkin-10 (8.20) (8.22) t A i ([c 1 ],..., [c n ]) = [c i ], i = 1,..., m Henkin-11 (8.23) t A ([c 1 ],..., [c n ]) = f A (t A 1 ([c 1 ],..., [c n ]),..., t A m([c 1 ],..., [c n ])) = f A ([c 1],..., [c m])henkin-12 c t(c 1,..., c n ) T c f(c 1,..., c m) T ; (8.21) 8.11,(b) [c] = f A ([c 1],..., [c m]) ; f A [c] = t A ([c 1 ],..., [c n ]) ; (8.23) 55

56 (b): 8.11, (c) c i C, i = 1,..., n (8.24) c i t i (c 1,..., c m ) T, i = 1,..., n Henkin-13 (a) (8.25) [c i ] = t A i ([c 1 ],..., [c m ]), i = 1,..., n Henkin-14 r(t 1 (c 1,..., c m ),..., t n (c 1,..., c m )) T r(c 1,..., c n) T ; (8.24) 8.11, (f) [c 1],..., [c n] r A ; r A t A 1 ([c 1 ],..., [c m ]),..., t A n([c 1 ],..., [c m ]) r A ; (8.25) 8.6 : 8.13 T T Henkin A Henkin L - φ A = φ φ T A C L- A L T Henkin-model L- φ = φ(x 1,..., x n ) (8.26) c 1,..., c n C Henkin-15 A = φ([c 1 ],..., [c n ]) φ(c 1,..., c n ) T φ t(x 1,..., x n ) t (x 1,..., x n ) c, c C (8.27) c t(c 1,..., c n ), c t (c 1,..., c n ) T Henkin-16 56

57 A = φ([c 1 ],..., [c n ]) t A (c 1,..., c n ) = t A (c 1,..., c n ) ; = [c] [c ] ; (8.27) 8.12, (a) c c T ; t(c 1,..., c n ) t (c 1,..., c n ) T ; 8.11, (d) φ(c 1,..., c n ) T φ m- r R r(t 1 (x 1,..., x n ),..., )t m (x 1,..., x n ) A = φ([c 1 ],..., [c n ]) t A 1 ([c 1 ],..., [c n ]),..., t A m([c 1 ],..., [c n ]) r A ; = r(t 1 (c 1,..., c n ),..., t m (c 1,..., c n )) T ; 8.12, (b) φ(c 1,..., c n ) T φ = ψ ψ (8.26) A = φ([c 1 ],..., [c n ]) A = ψ([c 1 ],..., [c n ]) ; = ψ(c 1,..., c n ) T ; ψ(c 1,..., c n ) T ; 8.11, (g) φ(c 1,..., c n ) T φ (ψ η), (ψ η), (ψ η) ψ, η (8.26) 8.11, (h), (i), (j) φ xψ(x, x 1,..., x n ) ψ (8.26) A = φ([c 1 ],..., [c n ]) c C A = ψ([c], [c 1 ],..., [c n ]) ; = c C ψ(c, c 1,..., c n ) T ; xψ(x, c 1,..., c n ) T 57

58 7.2 (8.11) 9 ( ) anwendunegen-des-vollst satzes 9.1 ( ) T L T T T L- 8.2 T ( ) T 8.6 T T T (finitely satisfiable) : 9.2 L L- A = A,... (9.1) A = φ A compact-0 L- φ φ (9.1) T = {φ} {c i c j : i, j N, i j} 58

59 c i, i N L T Ã Ã c i, i N A φ L- A c i, i N A A (9.1) φ 59

60 II partii 10 S S S A S t S t A L 24) S = S(L) := {,,,...} V ar L, Sent L Fml L S decidability 10.1 Fml L Sent L Fml L φ Fml L A canonical L A Th(A) = {φ Sent L : A = φ} (10.1) Th(A) decidable-0 canonical A A (10.1) S N successor function S : N N; n n + 1 (10.2) Th( Q, < ) 11.2 dec-0 (10.3) Th( N, 0, +, S, < ) 11.4 dec-1 (10.4) Th( R, 0, 1, +, ) 11.5 dec-2 60

61 (10.5) Th( N, 0, +,, S, < ) dec-3 1 : (10.6) Th( Q, 0, +,, S, < ) N Q, 0, +,, S, < dec-4 (Julia Robinson ) 1 (10.4), (10.5), (10.6) N Q R, 0, 1, +, N Q R, 0, 1, +, Th( R, 0, 1, +, ) Th( N, 0, +,, S, < ) Th( Q, 0, +,, S, < ) A L S = S(L) A L- T Th(A) A decidable-theories axioms Cn(T ) = Th(A) Cn(T ) = Cn L (T ) = {φ Sent L : T = φ} Cn(T ) = {φ Sent L : T φ} Th(A) A 11.1 A Th(A) T A T S L- φ T S B 0, B 1, B 2,... B i, i = 0, 1, 2,... n B n φ φ T B n φ T φ Th(A) φ Th(A) 24) 61

62 φ Th(A) Cn(T ) = Th(A) φ 25) 11.2 Th( Q, < ) Th( N, 0, S ) Presburger 11.5 Th( R, 0, 1, +, ) rationals quantifier-elimination presburger reals 12 N = N, 0, +,, E, S, < +, E (E(x, y) = x y ) S successor function (n n+1) < ; 2 ; 1 ; 2 0; +,, E; S; < L A 26) x < y z(z 0 y x + z) φ(x, y) N = x y (x < y φ(x, y)) < N x < y N N L A N E N reduction N M = N, 0, +,, S, < 27) N M 25) feasible 26) A arithmetic 27) N M M multiplicative overview 62

63 E N M E 28) E 29) successor + n (numeral) L A - S(S( (S(0 ) )) }{{}}{{} n n 1 S L A - S n (0) N ( ) 14 (?) N ( N M ) 12.1 (a) L A φ = φ(z) (z 0 x y(x y z (x S(0) y S(0)))) N = φ(n) n (b) L A ψ = ψ(z) u v w ((u 0 v 0) E(u, z) + E(v, z) E(w, z)) n 3 N = ψ(n) n- Fermat z (z > S(S(0)) ψ(z)) Fermat L A - ( N Fermat ) 30) 28) 14 N M 29) N + E ( ) 30) z > S(S(0)) u(u 0 z S(S(0)) + u) 63

64 14 L A Var {,,,...} s # s effective ( # s s Gödel number ) 14 n () Gödel number # s = n ( ) s Th(N) = {φ : φ L A - N = φ} A N N (definable) L A - φ = φ(x) n N (12.1) n A N = φ(s n (0)) b A Th(N) {#α : α A} N L A - σ N = σ A σ Goedel-1 ternary relation R (12.2) R = { a, b, c N 3 : a L A α = α(x) Gödel number c α(s b (0)) A Gödel number }. goedel-0 A coding 14 ( 14 ) R L A - ρ = ρ(v 1, v 2, v 3 ) a, b, c N R(a, b, c) N = ρ(s a (0), S b (0), S c (0)) (12.3) v 3 ρ(x, x, v 3 ) goedel-1 q Gödel number σ (12.4) v 3 ρ(s q (0), S q (0), v 3 ) goedel-2 64

65 σ A σ A σ σ A P k = #P (12.4) σ q (12.3) x S q (0) R ρ (12.5) N = ρ(s q (0), S q (0), S k (0)) goedel-3 A σ A ρ(s q (0), S q (0), S k (0)) A Th(N) N = ρ(s q (0), S q (0), S k (0)) (12.5) A σ A σ k N k σ Gödel number N = ρ(s q (0), S q (0), S k (0)) N = v 3 ρ(s q (0), s q (0), v 3 ) N = σ Tarski 12.2 ( ) #Th(N) = {#τ : τ L A - N = τ} N Th(N) ( L A - φ φ Th(N) φ Th(N) ) 12.1 σ #Th(N) N : 12.1 R (12.2) Goedel-2 (12.6) P = { a, b N 2 : a L A α = α(x) Gödel number N = α(s b (0)) }. goedel-4 P a N (12.7) P a = {b N : a, b P } goedel-5 65

66 a L A - φ a = φ a (x) Gödel number (12.8) P a = {b N : N = φ a (S b (0))} goedel-6 P a φ a N (12.9) H = {b N : b, b P } goedel-7 31) H P a N P H P T h(n), N Th(N) Th(N) weak-arith coding incompleteness 31) H 66