Дрозд Ю. Основи математичної логіки (на укр. языке)
Подождите немного. Документ загружается.
E
Ev
0
v
0
,
Ev
0
v
1
⇒ E(F uv
0
v, F uv
1
v),
F,k,l
Ev
0
v
1
⇒ (P uv
0
v ⇒ P uv
1
v)),
P,k,l
F P
T u =
v
2
. . . v
k+1
v = v
k+2
. . . v
k+l+1
k, l
k + l + 1 = n F P
n
I T I(E)
I(E)(a, b)) = 1
a = b
t = t
0
Ett
0
T
x, y, z, t, . . . v
0
, v
1
, v
2
, v
3
, . . .
O
L(x, y) ⇒ ¬L(y, x),
L(x, y) ∧ L(y, z) ⇒ L(x, z),
L I
I(L)
O
G P
e
P (x, P (y, z)) = P (P (x, y), z),
P ex = x ∧ P xe = x,
∃yP xy = e ∧ P yx = e.
I(P ) : M ×M →
M
I(e)
G
F
S, P o, e
S(x, S(y, z)) = S(S(x, y), z),
Sxy = Syx,
Sxo = x,
∃ySxy = o,
P (x, P (y, z)) = P (P (x, y), z),
P xy = P yx,
P xe = x,
¬x = o ⇒ ∃yP xy = e,
P (x, Syz) = S(P xy , P xz).
I F I(S)
I(P ) I(o) I(e)
R o, e S, P
L
O F
¬x = y ⇒ Lxy ∨ Lyx,
Lxy ⇒ L(Sxz, Syz),
Loz ∨ Lxy ⇒ L(P xz, P yz),
(∃xA ∧ ∃y∀x(A ⇒ Lxy)) ⇒
⇒ (∃y((∀x(A ⇒ Lxy ∨ x = y))∧
∧ ∀z(Lzy ⇒ ∃x(Lzx ∧ ¬A))),
A R
x
A
R
R
R
a, b na < b
n R
T I
M
∼= I(E)
M
f
M = M/ ∼
∼
e
I(F )(A
1
, A
2
, . . . , A
n
) = I(F )(a
1
, a
2
, . . . , a
n
), a
i
∈ A
i
,
e
I(P )(A
1
, A
2
, . . . , A
n
) = I(P )(a
1
, a
2
, . . . , a
n
), a
i
∈ A
i
,
F P n
e
I
f
M
a
i
b
i
∈ A
i
e
I T
E,0,1 E,1,0
a ∼ b b ∼ a a ∼ b a ∼ c b ∼ c
∼
a ∈ A, b ∈ B A, B
e
I(E)(A, B) = I(E)(a, b) = 1 a ∼ b A = B
I A T
e
I φ
val(I, ψ, A) ψ ψ(x) ∈ φ(x)
x
e
I
T T
e
I I
e
I
T
T
T
T
A T T |= A
|=
I
A I T
T
¯
T
T
A T
T ∪ {A }
T A
T |= A T |= ¬A
T
T M
N
M
m
m
m m
A, B, C
A B
A ⇒ B, A
B
,
A, B
A
∀xA
,
A x
A
1
, A
2
, . . . , A
n
A T A
n
= A
i = 1, 2, . . . , n
A
i
A
i
∈ T
j < i k < i A
j
= A
k
⇒ A
i
A
i
A
j
A
k
j < i A
i
= ∀xA
j
x
A
i
A
j
x
A T
T T ` A T
A
T
T
A = R
E
1
,E
2
,...,E
n
A
1
,A
2
,...,A
n
R
R
1
, R
2
, . . . , R
m
R
A
1
, A
2
, . . . A
m
A
i
= R
i
E
1
,E
2
,...,E
n
A
1
,A
2
,...,A
n
A
` ¬∃xA ⇒ ∀x¬A
` ∃x¬A ⇒ ¬∀xA
y A
` ∀xA ⇒ ∀yA
x
y
A ⇒ ∃xA, (A ⇒ ∃xA) ⇒ (¬∃xA ⇒ ¬A),
¬∃xA ⇒ ¬A, ∀x(¬∃xA ⇒ ¬A),
∀x(¬∃xA ⇒ ¬A) ⇒ (¬∃xA ⇒ ∀x¬A), ¬∃xA ⇒ ∀x¬A.
(A ⇒ B) ⇒ (¬B ⇒ ¬A)
∀xA ⇒ A
x
y
, ∀y(∀xA ⇒ A
x
y
),
∀y(∀xA ⇒ A
x
y
) ⇒ (∀xA ⇒ ∀yA
x
y
), ∀xA ⇒ ∀yA
x
y
.
M ` A T ` B B ∈ M T ` A
T ` A T ` ∀xA x
T `
¯
A
¯
A A
F m
T A
1
, A
2
, . . . , A
n
T
y
A
0
1
, A
0
2
, . . . , A
0
n
A
0
i
A
i
F t
1
t
2
. . . t
m
t
1
, t
2
, . . . , t
m
y
T
P m
T A
1
, A
2
, . . . , A
n
T
Q r T y
1
, y
2
, . . . , y
r
A
0
1
, A
0
2
, . . . , A
0
n
A
0
i
A
i
P t
1
t
2
. . . t
m
t
1
, t
2
, . . . , t
m
Qy
1
y
2
. . . y
r
T
A T T ` A
A T
T
` A ` ¬A
P
0
, P
1
, . . . , P
n
, . . . A
A
∗
A
P
k
A
k
= A||. . . | k |
A A
∗
A
1
, A
2
, . . . , A
n
A M
A
∗
1
, A
∗
2
, . . . , A
∗
n
A
∗
M
∗
` A A
∗
A
` A ` ¬A
A ` ∀xA
A x
A ⇒ ∀xA
` A ⇒ ∀xA
T = T
1
∪ T
2
B
1
, B
2
, . . . , B
n
T B
i
T
2
B
i
1
, B
i
2
, . . . , B
i
k
(i
1
< i
2
<
··· < i
k
) T
1
B
i
B
1
, B
2
, . . . , B
n
T
2
T
2
T
2
B
i
T
2
• B
i
T
1
• B
i
B
j
B
k
j, k < i T
2
• B
i
B
j
j < i
T
2
B T ∪ {A } A
A ⇒ B T
B T ∪ {A }
A A T ∪ {A } ` B
T ` A ⇒ B
B
1
, B
2
, . . . , B
m
B T ∪{A } A ⇒ B
T B
i
A
B
i
⇒ (A ⇒ B
i
), A ⇒ B
i
B
i
= A A
B
i
A B
j
x B
i
= ∀xB
j
x
A B
i
∀x(A ⇒ B
j
), ∀x(A ⇒ B
j
) ⇒ (A ⇒ ∀xB
j
), A ⇒ ∀xB
j
.
A ⇒ B
j
A ⇒ B T
B
T ∪ {A
1
, A
2
, . . . , A
n
} {A
1
, A
2
, . . . , A
n
}
A
1
⇒ (A
2
⇒ (. . . ⇒ (A
m
⇒ B) . . . )) T
A
i
T∪{A
1
, A
2
, . . . , A
n
} ` B
T ` A
1
⇒ (A
2
⇒ (. . . ⇒ (A
m
⇒ B) . . . ))
A ⇒
T
B T ` A ⇒ B A ≡
T
B
A ⇒
T
B B ⇒
T
A T = ∅ A ≡ B
(A ⇒ B) ⇒ (¬B ⇒ ¬A) A ⇒
T
B
¬B ⇒
T
¬A A ≡
T
B ¬A ≡
T
¬B
(A ⇒ B) ⇒ ((B ⇒ C) ⇒ (A ⇒ C)
A ⇒
T
B B ⇒
T
C A ⇒
T
C
A ⇒ B A
0
⇒ B
0
A
0
≡
T
A B
0
≡
T
B
A B
x
A ⇒
T
B ∀xA ⇒
T
∀xB ∃xA ⇒
T
∃xB
A ≡
T
B ∀xA ≡
T
∀xB ∃xA ≡
T
∃xB
¬∃xA ≡ ∀x¬A ∃xA ≡ ¬∀x¬A
¬∀xA ≡ ∃x¬A ∀xA ≡ ¬∃x¬A
y x A
∀xA ≡ ∀yA
x
y
∃xA ≡ ∃yA
x
y
∃xA ⇒ B ≡ ∀x(A ⇒ B) x
B
A ⇒ B T
∀xA ⇒ A, A, B, ∀xB.
∀xB T ∪ {∀xA } T ` ∀xA ⇒
∀xB A ⇒ B T (A ⇒ B) ⇒ ((B ⇒
∃xB) ⇒ (A ⇒ ∃xB))
(B ⇒ ∃xB) ⇒ (A ⇒ ∃xB), B ⇒ ∃xB, A ⇒ ∃xB, ∀x(A ⇒ ∃xB),
∀x(A ⇒ ∃xB) ⇒ (∃xA ⇒ ∃xB), ∃xA ⇒ ∃xB.
∃xA ⇒ ∃xB
` ¬∀xA ⇒ ∃x¬A
` ∃x¬A ⇒ ¬∀xA. ` ¬∃x¬A ⇒ ∀x¬¬A
¬¬A A ` ¬∃¬A ⇒ ∀xA
` ¬∀xA ⇒ ¬¬∃¬A ` ¬∀xA ⇒ ∃x¬A
∀yA
x
y
∀xA
∀xA, ∀xA ⇒ A
x
y
, A
x
y
, ∀yA
x
y
.
x y A
x
y
(A
x
y
)
y
x
= A A A
x
y
∃xA ⇒ B (X ⇒ Y ) ⇒ (¬Y ⇒ ¬X)
¬B ⇒ ¬∃xA (X ⇒ Y ) ⇒ ((Y ⇒ Z) ⇒
(X ⇒ Z)) ¬B ⇒ ∀x¬A ∀xA ⇒ A
¬B ⇒ ¬A A ⇒ B
∀x(A ⇒ B) ∃xA ⇒ B ` ∀x(A ⇒ B)
` ∃xA ⇒ B ⇒ ∀x(A ⇒ B)
A ≡
T
A
0
B ≡
T
B
0
¬A ≡
T
¬A
0
;
A ∧ B ≡
T
A
0
∧ B
0
;
A ∨ B ≡
T
A
0
∨ B
0
;
A ⇒ B ≡
T
A
0
⇒ B
0
.
∀x(A ∧ B) ≡ ∀xA ∧ ∀xB;
∃x(A ∨ B) ≡ ∃xA ∨ ∃xB;
∃x(A ⇒ B) ≡ ∀xA ⇒ ∃xB,
∃x(A ⇒ B) ≡ A ⇒ ∃xB, x A,
∃x(A ⇒ B) ≡ ∀xA ⇒ B, x B;
∀x(A ∨ B) ≡ ∀xA ∨ B , x B;
∃x(A ∧ B) ≡ ∃xA ∧ B , x B.
A ⇒ ∀xB ≡ ∀x(A ⇒ B) x
A
` ∃y∀xA ⇒ ∀x∃yA
∀x∀yA ≡ ∀y∀xA ∃x∃yA ≡ ∃y∃xA
∀x(A ∨ B) ≡ ∀xA ∨ ∀xB
∃x(A ∧ B) ≡ ∃xA ∧ ∃xB
∀x(A ⇒ B) ≡ (∃xA ⇒ ∀xB)
A
A
0
= Q
1
x
1
Q
2
x
2
. . . Q
m
x
m
A
0
Q
1
, Q
2
, . . . , Q
m
x
1
, x
2
, . . . , x
m
A
0
A A
Π = Q
1
x
1
Q
2
x
2
. . . Q
m
x
m
A
0
A
0
A
A A
A
A = QxB Q A ≡ A
0
= QxB
0
B
0
B A
0
A = ¬B B
0
= Q
1
x
1
Q
2
x
2
. . . Q
m
x
m
C C
B
A ≡ A
0
= Q
0
1
x
1
Q
0
2
x
2
. . . Q
0
m
x
m
¬C,
Q
0
i
Q
i
A
0
A = B ∨ C B
0
= Π
B
B
0
C
0
= Π
C
C
0
B C Π
B
Π
C
B
0
C
0
Π
B
Π
C
A ≡ A
0
= Π
B
Π
C
(B
0
∨C
0
) A
0
A = B ∧ C A = B ⇒ C
∀xA∨∀xB, ∃xA∧
∃xB ∃xA ⇒ ∀xB
T A
T ` A T ` ¬A T ` B
B