Дрозд Ю. Основи математичної логіки (на укр. языке)
Подождите немного. Документ загружается.
∀x∃yA ⇒ ∃y∀xA
A = P xy P
I I(F )
A
1
, A
2
, . . . , A
n
A
T A T T = T
1
∪ T
2
T
2
A
1
, A
2
, . . . , A
n
A T B = {A
i
1
, A
i
2
, . . . , A
i
m
}
B
x
c
A
1
, A
2
, . . . , A
n
A T ∪ B B
B
x
c
⇒ A T ∪ B
0
B
0
=
{A
i
1
, A
i
2
, . . . , A
i
m−1
} B
0
y
c
y B
x
y
⇒ A
∀y(B
x
y
⇒ A), ∀x(B ⇒ A), ∃xB ⇒ A, ∃xB, A.
A T ∪ B
0
B
0
∃xB T ∪ B
0
B
0
y
T
2
B
0
A T
`∃x(A ∧ B) ⇒ ∃xA ∧ ∃xB,
`(∀xA ∨ ∀xB) ⇒ ∀x(A ∨ B).
A
∃x
1
. . . ∃x
m
∀y
1
. . . ∀y
k
m = 0 k = 0
P
T P
P
P A
0
A P
P T T ` A
T ` A
0
T |= A T |= A
0
A
A
0
P
P
A A
P
A = ∃x
1
∃x
2
. . . ∃x
m
∀yB
P (m + 1) P
A A
0
= ∃x
1
∃x
2
. . . ∃x
m
∀y(B ⇒ P x
1
x
2
. . . x
m
y) ⇒
∀yP x
1
x
2
. . . x
m
y
T ` A P T T ` A
0
T ` A A
0
c
1
, c
2
, . . . , c
m
∀yB
x
1
x
2
...x
m
c
1
c
2
...c
m
X ⇒ ((X ⇒ Y ) ⇒ Y ))
` ∀yB
x
1
x
2
...x
m
c
1
c
2
...c
m
⇒
∀y
B
x
1
x
2
...x
m
c
1
c
2
...c
m
⇒ P c
1
c
2
. . . c
m
y
⇒ ∀yP c
1
c
2
. . . c
m
y
.
A
0
A
0
T
B
P u
1
u
2
. . . u
m
v
u
1
, u
2
, . . . , u
m
, v B
x
1
x
2
...x
m
y
u
1
u
2
...u
m
v
e
A = ∃x
1
∃x
2
. . . ∃x
m
∀y(B ⇒ B) ⇒ ∀yB
.
` B ⇒ B ` ∀y(B ⇒ B) ∀yB ≡
∀y(B ⇒ B) ⇒ ∀yB
e
A ≡ A A
T
A
∀ = ∃x
1
∃x
2
. . . ∃x
m
∀yΠB Π = Q
1
u
1
. . . Q
r
u
r
B
A
0
= ∃x
1
∃x
2
. . . ∃x
m
∀y(ΠB ⇒ P x
1
x
2
. . . x
m
y) ⇒ ∀yP x
1
x
2
. . . x
m
y
,
P (m + 1) P
B P T T ` A
T ` A
0
A
0
≡ ∃x
1
∃x
2
. . . ∃x
m
∀y
Π
0
(B ⇒ P x
1
x
2
. . . x
m
y) ⇒ ∀vP x
1
x
2
. . . x
m
v)
≡ ∃x
1
∃x
2
. . . ∃x
m
∃yΠ
(B ⇒ P x
1
x
2
. . . x
m
y) ⇒ ∀vP x
1
x
2
. . . x
m
v
≡ ∃x
1
∃x
2
. . . ∃x
m
∃yΠ∀v
(B ⇒ P x
1
x
2
. . . x
m
y) ⇒ P x
1
x
2
. . . x
m
v
,
v A Π
0
= Q
0
1
u
1
. . . Q
0
r
u
r
Q
0
j
Q
j
A
00
T ` A T ` A
00
A
00
A
∀x∃yA
A T
I φ I
val(I, φ, A) = 1 P
P
A
A
0
∀x
1
. . . ∀x
m
∃y
1
. . . ∃y
m
B B
P T A T
A
0
A
0
∃x∀yA
P
A
E c
0
c
1
S P
v + 1 6= 0
v + 1 = v
1
+ 1 ⇒ v = v
1
v + 0 = v
v + (v
1
+ 1) = (v + v
1
) + 1
v · 0 = 0
v · (v
1
+ 1) = v · v
1
+ v
A
v
0
∧ ∀v(A ⇒ A
v
v+1
) ⇒ ∀vA
A v
0 c
0
1 c
1
a + b Sab a ·b
ab P ab a = b
Eab a 6= b ¬a = b
· +
a 6 b ∃v a + v = b
a < b a 6 b ∧ a 6= b
n = (. . . ((1 + 1) + 1) + ··· + 1)
| {z }
n
A N
N
N(E) N(S)(a, b) = a+b N(P )(a, b) =
ab
A
A
x
0
∧ ∀x(A ⇒ A
x
x+1
) ⇒ ∀xA x
A
A A(x) x
A
A(t) A
x
t
A(x, y), A(x
1
, x
2
, x
3
)
A(a, b), A(c
1
, c
2
, c
3
) A ⇔ B
(A ⇒ B) ∧ (B ⇒ A) ⇔
∃!xA(x)
∃x
A(x) ∧ (A(y) ⇒ y = x)
N
A
ω
(Ω) A(v) A A ` ¬A(n)
n A ` ∃vA
ω
A A
A ` A A ` ¬A
1 S P
N t
0
Nt
+1
0
n NN . . . N
| {z }
n
0
x 6= 0 ⇒ ∃y x = y + 1
x + y = y + x
(x + y) + z = x + (y + z)
x(y + z) = xy + xz (x + y)z = xz + yz
xy = yx
x(yz) = (xy)z
x + z = y + z ⇒ x = y
x 6 y ∨ y 6 x x < y ∨ y < x ∨ x = y
x < y + 1 ⇔ x 6 y x < y ⇒ x + 1 6 y ¬x < 0
x + y = 0 ⇒ x = 0 ∧ y = 0
xy = 0 ⇒ x = 0 ∨ y = 0
xz = yz ∧ z 6= 0 ⇒ x = y
x < y ⇒ x + z < y + z
x < y ∧ z 6= 0 ⇒ xz < yz
A(x) A ` A(0)
¬X ⇒ (X ⇒ Y ) x + 1 = x + 1 ⇒ ∃y x + 1 = y + 1
A ` ∃y x + 1 = y + 1 A ` A(x) ⇒ A(x + 1)
A ` ∀xA
A ` 0 + x = x 0 + 0 = 0
0 + (x + 1) = (0 + x) + 1 0 + x = x
0+(x+1) = x+1 0+x = 0 ⇒ 0+(x+1) =
0 0 + 0 = 0 ∧∀x(0 + x = 0 ⇒ 0 + (x + 1) = x + 1) ⇒
∀x 0 + x = x A ` 0 + x = x
(x+1)+y = (x+y)+1 y = 0
(x + 1) + 0 = x + 1 = (x + 0) + 1 (x + 1) + y = (x + y) + 1
(x+1)+(y+1) = ((x+1)+y)+1 = ((x+y)+1)+1 =
(x + (y + 1)) + 1 A ` (x + 1) + y = (x + y) + 1
x + y = y + x (x + 1) + y = (x + y) + 1 =
(y + x) + 1 = y + (x + 1) A ` x + y = y + x
(x + y) + 0 = x + y = x + (y + 0) (x + y) + z = x + (y + z)
(x + y) + (z + 1) = ((x + y) + z) + 1 = (x + (y + z)) + 1 = x + ((y + z) + 1) =
x + (y + (z + 1)) A ` (x + y) + z = x + (y + z)
x(y + 0) = xy = xy + 0 = xy + x0 x(y + z) = xy + xz
x(y + (z + 1)) = x((y + z) + 1) = x(y + z ) + x = (xy + xz) + x =
xy + (xz + x) = xy + x(z + 1) A ` x(y + z) = xy +xz
0 · 0 = 0 0x = 0 0(x + 1) = 0x + 0 = 0 + 0 = 0
A ` 0x = 0 = x0 A ` (x + 1)y = yx + y = y(x + 1)
y = 0 (x + 1) ·0 = 0 = x ·0 + 0 (x + 1)y = xy + y
(x + 1)(y + 1) = (x + 1)y + (x + 1) = (xy + y) + (x + 1) = (xy + x) + (y + 1) =
x(y + 1) + (y + 1) A ` (x + 1)y = xy + y
A ` xy = yx
(xy)(zt) x +
((y + z) + t) xyzt x + y + z + t
z = 0 x+z = y+z ⇒ x = y
x+(z+1) = y+(z+1) (x+z)+1 = (y+z)+1 x+z = y+z
x = y A ` x + z = y + z ⇒ x = y
0 6 y y = y + 0 = 0 + y y 6 x x = y + z
x + 1 = y + z + 1 y 6 x + 1 x 6 y y = x + z
z 6= 0 A ` ∃z z = z + 1 c z = c + 1
y = x + (c + 1) = (x + 1) + c y 6 x + 1 z = 0 y = x 6 x + 1
x + 1 6 y y 6 x + 1
A ` x 6 y ∨ y 6 x
y 6= 0 c
y = c + 1 xy = xc + x xy = 0 x = 0
A(x) = (xz = yz ∧z 6= 0 ⇒ x = y) x = 0 xz =
0 xz = yz y = 0 A ` A(0)
A(x) x+1 6= 0 z 6= 0 ⇒ (x+1)z 6= 0
(x+1)z = yz∧z 6= 0 y 6= 0
c y = c + 1 xz + z = cz + z xz = cz
x = c x + 1 = c + 1 = y A(x + 1)
A ` A(x)
x + y = 1 ⇒ (x = 1 ∧ y = 0) ∨ (x = 0 ∧ y = 1)
xy = 1 ⇒ x = 1 ∧ y = 1
x < y ⇒ ¬y < x
x 6 y ∧ y 6 z ⇒ x 6 z
x 6 y ∧ y < z ⇒ x < z x < y ∧ y 6 z ⇒ x < z
x < y ⇔ x + z < y + z
x < y ∧ z 6= 0 ⇔ xz < yz
x|y ∃z y = xz
x|y ∧ y 6= 0 ⇒ x 6 y
x|y ∧ y|z ⇒ x|z
A
A
∀x
∀y
y < x ⇒ A(y)
⇒ A(x)
⇒ ∀xA(x)
A(x) A
∃xA(x) ⇒ ∃x
A(x) ∧ ∀y
A(y) ⇒ x 6 y
A(x) A
x 6 n ⇒ (x = 0 ∨ x = 1 ∨ x = 2 ∨ ··· ∨ x = n)
n
x 6= 0 ⇒ ∃! z ∃! t (y = xz + t ∧ t < x).
B(x) = ∀y
y 6 x ⇒ A(y)
∀x
∀y
y < x ⇒ A(y)
⇒ A(x)
∀xB(x)
B(x) ⇒ A(x) B(x) ≡ ∀y
y <
x + 1 ⇒ ∀(y)
B(x) ⇒ A(x + 1) B(0)
∀y
y 6 0 ⇒ A(0)
y 6 0 ⇔ y = 0 B(0) ≡ A(0)
¬y < 0 ∀y
y < 0 ⇒ A(y)) A(0)
B(0) B(x) A(x + 1)
y 6 x + 1 ≡ y = x + 1 ∨ y 6 x A(y)
B(x + 1) ∀xB(x)
¬∃x
A(x) ∧ ∀y
A(y) ⇒ x 6 y
∀x
¬A(x) ∨
¬∀y
A(y) ⇒ x 6 y
∀x
∀y
A(y) ⇒ x 6 y
⇒ ¬A(x)
X ∨Y ≡ (¬Y ⇒ X) ∀x
∀y
y < x ⇒ ¬A(y)
⇒ ¬A(x)
(X ⇒ Y ) ≡ (¬Y ⇒ ¬X)
∀x¬A(x) ¬∃xA(x) ¬∃x
A(x) ∧
∀y
A(y) ⇒ x 6 y
⇒ ¬∃xA(x) ∃xA(x) ⇒ ∃x
A(x)∧
∀y
A(y) ⇒ x 6 y
A
n
x 6 n ⇒ (x = 0∨x = 1 ∨x = 2 ∨···∨x = n)
n + 1 = n + 1 A
n+1
≡ A ∨ x = n + 1
A
n
n n = 0 n = 0 x 6 0 ⇒ x = 0
A
n
x 6 n + 1 ⇒ x = n + 1 ∨ x 6 n
(X ∨Y ) ∧ (Y ⇒ Z) ⇒ (Z ∨X) A
n+1
y = xz + t = xz
0
+ t
0
∧ t < x ∧ t
0
< x ⇒
z = z
0
∧ t = t
0
t 6 t
0
t
0
6 t
t 6 t
0
t
0
= u+t xz+t = xz
0
+u+t xz = xz
0
+u
xz
0
6 xz z
0
6 z
z = z
0
+ v xz
0
+ xv = xz
0
+ u xv = u t
0
= u + t u 6 t
0
t
0
< x u < x
u = 0 t = t
0
z = z
0
t
0
6 t
A(y) = ∃z ∃t (y = xz + t ∧t < x)
0 = x · 0 + 0 x 6= 0 ⇒ 0 < x A ` A(0) A(y)
c, d y = cx + d ∧ d < x y + 1 = cx + (d + 1)
d+1 6 x d+1 < x∨d+1 = x d+1 = x
y + 1 = cx + (d + 1) = cx + x = (c + 1)x + 0
A(y + 1) ∀yA(y)
A
[x/y] res(x, y) N
2
N
• b 6= 0 res(a, b) < b a = b[a/b] + res(a, b)
• [a/0] = 0 res(a, 0) = a
[a/b]
res(a, b) a b
a, b, . . .
a, b, . . .
A
a < b A ` a < b a = b
a b
A ` a + b = a + b A ` ab = ab
F (x
1
, x
2
, . . . , x
m
)
a
1
, a
2
, . . . , a
m
b = F (a
1
, a
2
, . . . , a
m
)
F (x
1
, x
2
, . . . , x
n
)
F c c
A ` F (a
1
, a
2
, . . . , a
m
) = b
A(0) ∧ A(1) ∧ . . . ∧ A(n) ≡
A
∀x
x 6 n ⇒ A(x)
A(0) ∨ A(1) ∨ ··· ∨ A(n) ≡
A
∃x
x 6 n ∧ A(x)
A ` ∀x
A(x) ⇒ ∃y
A(y) ∧ y < x
⇒ ∀x¬A(x).