Дрозд Ю. Основи математичної логіки (на укр. языке)
Подождите немного. Документ загружается.
Q
z60
f(x, z) = 1
Q
z6y+1
f(x, z) = f(x, y + 1)
Q
z6y
f(x, z).
µ
z<0
f(x, z) = 0
µ
z<y+1
f(x, z) = sg(f (x, µ
z<y
f(x, z)))·
· µ
z<y
f(x, z)(y + 1) sg(f(x, µ
z<y
f(x, z)))
n N P :
N
n
→ B
1 0
0 1
∧, ∨ ¬ ¬P = 1−
.
P P ∧Q = min(P, Q)
P ∨Q = max(P, Q)
x = y sg(|x − y|)
x < y sg(y −
.
x)
x|y sg(res(y, x))
Pr(x) = x sg(x−
.
1) sg(|D(x) − 2|) D(x) =
P
y6x
sg(res(x, y))
x
p
(x) = x
p
(0) = 2,
p
(1) =
3,
p
(2) = 5, . . .
p
(0) = 2
p
(x+ 1) = µ
z<
p
(x)!+1
g(x, z)
g(x, y) = (
p
(x) < y ∧ Pr(y))
v(x, y) =
p
(y)
x v(0, y) =
0
v(x, y) = µ
z<x
g(x,
p
(y), z), g(x, y, z) = ¬y
z+1
|x.
len(x) = max {y | v(x, y) 6= 0 }
x∗y
x ∗y =
p
(0)
k
0
p
(1)
k
1
. . .
p
(r)
k
r
p
(r + 1)
l
0
p
(r + 2)
l
1
. . .
p
(r + s + 1)
l
s
,
x =
p
(0)
k
0
p
(1)
k
1
. . .
p
(r)
k
r
r = len(x) y =
p
(0)
l
0
p
(1)
l
1
. . .
p
(s)
l
s
s = len(y)
x ∗ y = x
Q
z6len(y)
p
(len(x) + z + 1)
v(y,z)
.
f(x, y)
f
]
(x, y) =
Q
z<y
p
(z)
f(x,z)
f
]
f(x, y) = v(f
]
(x, y + 1), y)
f
f(x, y) = h(x, y, f
]
(x, y)) h
f
]
f
]
(x, 0) = 1
f
]
(x, y + 1) = f
]
(x, y)
p
(y)
f(x,y)
= f
]
(x, y)
p
(y)
h(x,y,f
]
(x,y))
,
f f
]
(x, y)
f(x, z) z < y f(x, z) =
v(f
]
(x, y), z)
f(x, 0) = g
0
(x), f(x, 1) = g
1
(x), . . . , f(x, m) = g
m
(x),
f(x, y + m + 1) = h(x, y, f(x, y), x(y + 1), . . . , x(y + m)),
g
k
h m
m > 1
x m
a
0
+ a
1
m + a
2
m
2
+ ··· + a
r
m
r
0 6 a
k
< m k r = [log
m
x]
max
l | m
l
6 x
a
k
k
m x Z(x, k, m)
Z(x, k, m) = res([x/m
k
], m)
g
1
, g
2
, . . . , g
n
R
1
, R
2
, . . . , R
m
a
f(x) =
g
1
(x) R
1
(x),
g
2
(x) R
2
(x),
. . . . . . . . . . . . . . . . . . . . . . . . . . . .
g
m
(x) R
m
(x).
f(x) =
P
m
k=1
g
k
(x)(1 −
.
R(x))
N
n
N
n
n > 2
σ
n
k
(x) (k = 1, 2, . . . , n) τ
n
(x
1
, x
2
, . . . , x
n
)
τ
n
(σ
n
1
(x), σ
n
2
(x), . . . , σ
n
n
(x)) = x;
σ
n
k
(τ (x
1
, x
2
, . . . , x
n
)) = x
k
k.
n = 2
τ τ
2
σ
k
(k = 1, 2)
σ
2
k
(a, b)
(0, 0) (0, 1)
ww
p
p
p
p
p
p
(0, 2)
ww
p
p
p
p
p
p
(0, 3)
ww
p
p
p
p
p
p
(1, 0) (1, 1)
ww
p
p
p
p
p
p
(1, 2)
ww
p
p
p
p
p
p
(2, 0 (2, 1)
ww
p
p
p
p
p
p
(3, 0)
(a, b) (a
0
, b
0
)
a + b < a
0
+ b
0
a + b = a
0
+ b
0
a < a
0
m + 1
a + b = m m(m + 1)/2 a + b < m τ(a, b) (a, b)
τ(a, b) = a + (a + b)(a + b + 1)/2
τ(0, 0) = 0
c (σ
1
(c), σ
2
(c))
c d
d d(d +
1)/2 6 c d =
(
√
8c + 7 − 1)/2
σ
1
(c) =
c −d σ
2
(c) = d −σ
1
(c) d
τ, σ
1
, σ
2
n σ
n
k
τ
n
τ
n+1
(x
1
, x
2
, . . . , x
n+1
) = τ
n
(x
1
, x
2
, . . . , x
n−1
, τ
2
(x
n
, x
n+1
));
σ
n+1
k
(x) =
σ
n
k
(x), k < n,
σ
2
1
(σ
n
n
(x)), k = n,
σ
2
2
(σ
n
n
(x)), k = n + 1
τ
n
σ
n
k
N
n
N
n
→ N N N → N
f : N
n
→ N
m
σ
n
◦ f ◦ τ
m
σ
n
(x) = (σ
n
1
(x), . . . , σ
n
n
(x))
f(x) = (f
1
(x), . . . , f
m
(x)) f
i
R
1
R
2
. . . R
n
R
i
A
0 1 v | E S P ∨ ∧ ⇒ ¬ ∀ ∃ ( )
A
0 1 v | E S P ∨ ∧ ⇒ ¬ ∀ ∃ ( )
0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15
a γ(a)
w = a
n
a
n−1
. . . a
1
a
0
A
γ(w) = 16
n
γ(a
n
) +16
n−1
γ(a
n−1
) +···+ 16γ(a
1
) +γ(a
0
)
γ
A
A
l(n) = [log
16
n] + 1 n Z
k
(n) =
Z(n, k, 16) k n
Evv 4 · 16
2
+ 2 · 16 + 2 =
1072
n = SS . . . S
| {z }
n−1
11 . . . 1
| {z }
n
5 · 16
2n−2
+ 5 · 16
2n−3
··· + 5 · 16
n
+ 16
n−1
+ 16
n−2
+ ··· + 1.
w
0
w
1
w
2
. . . w
n
γ(w
n
) + γ(w
n−1
) · 16
l(w
n
)
+ γ(w
n−2
) · 16
l(w
n
)+l(w
n−1
)
+
+ ··· + γ(w
0
) · 16
P
n
k=1
l(w
k
)
γ(w) = n, γ(w
0
) = m
w (w ⇒ w
0
) w
0
m + 15 · 16
l(m)
+ 14 · 16
l(m)+1
+ m · 16
l(m)+2
+
+ 9 · 16
2l(m)+2
+ n · 16
2l(m)+3
+ 13 · 16
2l(m)+l(n)+3
+
+ 15 · 16
2l(m)+l(n)+4
+ n · 16
2l(m)+l(n)+5
.
Var(x) x
Term(x) x
Atom(x) x
Sent(x) x
MP(x, y, z) x
y z
Occ(x, y, z) y
x
z x
Oct(x, y) y
x
Dom(x, y, z) x
z
Qv v y
Free(x, y, z) y
x z
Sub(x, y, z) x
y z
Gen(x, y) x
y
Tfr(x, y, z) y
y z
Ded(x, y) x
y
2 · 16
n
+ 3 · 16
n−1
+ ··· + 3 · 16 + 3 2 n = 0 x
Var(x) = sg
Z
l(x)
(x) − 2
+
P
y<l(x)
Z
y
(x) − 3
.
0 1
S P
Term(x) = sg
(x −
.
1)·
·
Q
y<x
Q
z<x
x −
5 · 16
l(y)+l(z)
+ y · 16
l(z)
+ z
+
+ Term(y) + Term(z)
·
·
Q
y<x
Q
z<x
x −
6 · 16
l(y)+l(z)
+ y · 16
l(z)
+ z
+
+ Term(y) + Term(z)
.
0 x =
0 = γ(0) x = 1 = γ(1) 0
x 5ab a b
y = γ(v) z = γ(w) v w x =
γ(Svw) S P
Et
1
t
2
t
1
, t
2
Atom(x) = sg
Q
y<x
Q
z<x
x − (4 · 16
l(y)+l(z)
+ y · 16
l(z)
+ z)
+
+ Term(y) + Term(z)
.
Sent(x) = sg
Atom(x)·
·
Q
y<x
x − (10 · 16
l(y)
+ y)
+ Sent(y)
·
·
Q
y<x
Q
z<x
x − (13 · 16
l(y)+l(z)+2
+ y · 16
l(z)+2
+ 7 · 16
l(z)+1
+
+ z · 16 + 14)
+ Sent(y) + Sent(z)
·
·
Q
y<x
Q
z<x
x − (13 · 16
l(y)+l(z)+2
+ y · 16
l(z)+2
+ 8 · 16
l(z)+1
+
+ z · 16 + 14)
+ Sent(y) + Sent(z)
·
·
Q
y<x
Q
z<x
x − (13 · 16
l(y)+l(z)+2
+ y · 16
l(z)+2
+ 9 · 16
l(z)+1
+
+ z · 16 + 14)
+ Sent(y) + Sent(z)
·
·
Q
y<x
Q
z<x
x − (11 · 16
l(y)+l(z)
+ y · 16
l(z)
+ z)
+
+ Var(y) + Sent(z)
·
·
Q
y<x
Q
z<x
x − (12 · 16
l(y)+l(z)
+ y · 16
l(z)
+ z)
+
+ Var(y) + Sent(z)
.
2 3 v |
2
|
Occ(x, y, z) = sg
Sent(x) + Var(y) +
Z
l
(x) − 2
+
+
y −
res(x, 16
z+1
)/16
(z+1)−
.
l(y)
+ sg
Z
z−
.
l(y)
(x) − 3
.
Free(x, y, z) = sg
Occ(x, y, z) + (1 −
.
Dom(x, y, z))
Sub
1
(x, y, z)
x
y
z
Sub
1
(x, y, z) = sg
(l(x) −
.
u) + Term(y)
res(x, 16
(u+1)−
.
l(z)
)+
+ 16
(u+1)−
.
l(z)
y + 16
((u+1)−
.
l(z))+l(y)
[x/16
u+1
]
+
+ sg
(l(x) −
.
u) + Term(y)
x,
u = µ
t<l(x)
Free(x, z, t)
x y
u = l(x) Sub
1
(x, y, z) = x w
1
w
2
w
3
w
2
l(z) u
res(x, 16
(u+1)−
.
l(z)
) w
3
[x/16
u+1
] w
1
w
1
w
4
w
2
w
4
Sub(x, y, z, t)
Sub(x, y, z, 0) = x,
Sub(x, y, z, t + 1) = Sub
1
(Sub(x, y, z, t), y, z).
Sub(x, y, z) = Sub(x, y, z, l(x))
S T E
Ax
k
(x) x
k
Ax(x) =
Q
28
k=1
Ax
k
(x)
Ax(x)
Ax
1
(x) x
(A ⇒ (B ⇒ A))
Ax
1
(x) = sg
Q
y<x
Q
z<x
Sent(y) + Sent(z)+
+
x − (14 + 14 · 16 + y · 16
2
+ 9 · 16
l(y)+2
+
+ z · 16
l(y)+3
+ 13 · 16
l(y)+l(z)+3
+ 9 · 16
l(y)+l(z)+4
+
+ y · 16
l(y)+l(z)+5
+ 13 · 16
2l(y)+l(z)+5
)
.
Ax
12
(x) x (A
z
t
⇒
∃zA) t z A
Ax
12
(x) = sg
Q
y<x
Q
z<y
Q
t<x
Sent(y) + Var(z) + Term(t)+
+ Tfr(y, z, t) +
x − (14 + 16y + z · 16
l(y)+1
+
+ 12 · 16
l(y)+l(z)+1
+ 9 · 16
l(y)+l(z)+2
+
+ u · 16
l(y)+l(z)+3
+ 13 · 16
l(y)+l(z)+l(u)+3
)
,
u = Sub(y, t, z)
Ax
28
(x) x ((A
v
0
∧
∀v(A ⇒ A
v
Sv1
)) ⇒ ∀vA)
Ax
28
(x) = sg
Q
y<x
Sent(y) +
x − (14 + 16y + 2 · 16
l(y)+1
+
+ 11 · 16
l(y)+2
+ 9 · 16
l(y)+3
+ 14 · 17 · 16
l(y)+4
+
+ u · 16
l(y)+6
+ 9 · 16
l(y)+l(u)+6
+ y · 16
l(y)+l(u)+7
+
+ 13 · 16
2l(y)+l(u)+7
+ 2 · 16
2l(y)+l(u)+8
+ 11 · 16
2l(y)+l(u)+9
+
+ 8 · 16
2l(y)+l(u)+10
+ t · 16
2l(y)+l(u)+11
+
+ 13 · 17 · 16
2l(y)+l(u)+l(t)+11
)
,
t = Sub(y, 2, 0), u = Sub(y, 2, 1313) 1313 = 5 ·16
2
+ 2 ·
16 + 1 = γ(Sv1)
Seq(x, y) x
y
Seq(x, y) = sg
Sent(y) + |x − y| ·
Q
z<x
Q
t<x
Seq(z, y) + Sent(t)+
+
x − (z + 15 · 16
l(z)
+ t · 16
l(z)+1
)
·
·
x − (t + 15 · 16
l(t)
+ z · 16
l(t)+1
)
.
Ded(x, y)
Ded(x, y) = sg
Ax(y) + |x − y|
·
Q
z<x
Q
t6z
Ded(z, t)+
+
x − (y + 15 · 16
l(y)
+ z · 16
l(y)+1
)
+
+ Ax(y) ·
Q
u6z
Seq(z, u) + Gen(y, u)
·
·
Q
u<z
Q
v<z
Seq(z, u) + Seq(z, v) + MP(y, u, v)
N
f : N
n
→ N
g(x, y) f(x) = σ
1
(µ
y
g(x, y))
σ
1
= σ
2
1
n = 1 A(x, y) f(x)
f(a) = b A ` A(a, b)
n = γ(A), m = γ(x), l = γ(y)
h(x, y, z) = Ded(z, Sub(Sub(n, m, x), l, y)).
h(a, b, c) = 0 c
A(a, b) a b
A ` A(a, b) a b, c
h(a, b, c) = 0 b
g(x, y) = h(x, σ
1
(y), σ
2
(y)) a c g(a, c) = 0
f(a) = σ
1
(c) f(x) = σ
1
(µ
y
g(x, y))
M ⊆ N
n
M ⊆ N
n
M ⊆ N
M A(x) m
M a ∈ M A ` A(a)
h(x, y) = Ded(y, Sub(m, l, x)) l = γ(x) g(x) = h(σ
1
(x), σ
2
(x))
a ∈ M
b h(a, b) = 0 c ∈ M M 6= ∅
f(x)
f(x) =
(
σ
1
(x), g(x) = 0,
c, g(x) 6= 0.
M
f(x)
A(x, y) M
∃xA(x, y)
b ∈ M a f(a) = b
A ` A(a, b) A ` ∃xA(x, b) b /∈ M a
c = f(a) A ` A(a, y) ⇒ y = c A ` b 6= c
A ` ¬A(a, b)
ω
∃xA(x, b)
∃xA(x, y) M
Γ
N
Γ ¬Γ
G(x, y) x
A y A
v
x
G(x, y) = Ded(y, Sub(x, γ(x), 2))
γ(x) γ(x)
G(x, y)
G x y
x = v
n ¬∃yG(v, y) Γ = ¬∃yG(n, y)
γ(Γ) = Sub(n, γ(n), 2) A ` Γ m
G(n, m)
A ` G(n, m) A ` ∃yG(n, y) A ` ¬Γ
A
Γ
∃yG(n, y)
m
G(n, m) G(n, m) A ` ¬G(n, m)
m Γ
∃yG(n, y) Γ
Γ