2.9 KiB
2.9 KiB
Язык логики первого порядка
[!Легенда]
U
- универс Предикат - высказывание, отношение
U^k = \set{(u_1 \dots u_k) | u_i \in U}
\rho \subset U^k
определяет k-ый предикат
\rho(u_1 \dots u_k) = 1 \Leftrightarrow (u_1 \dots u_k) \in rho
\phi \subset U^{k+1}
\phi(a_1 \dots a_k, f(a_1 \dots a_k)) = 1
y = x^2
\phi = \set{(x, x^2) | x \in \mathbb R}
\phi^{-1} = \set{(x^2, x) | x \in \mathbb R}
y = \sqrt x
-
Нелогические символы
- Обозначения функций
- Обозначения предметов
- Обозначения констант
- Имена переменных
-
Логические символы
- Конъюнкция
- Отрицание
- Дизъюнкция
- Логическое следование
- Квантры (
\forall
,\exists
)
-
Терм
- Переменные и константы
f(x_1 \dots x_k)
- функция иt_1 \dots t_k
- термы\rightarrow f(t_1 \dots t_k)
- терм Примеры:e^x
,\sin x
,+
,\times
,\pi
,\frac{\sin(x+y)\times e^z}e
-
Формулы (высказывания)
p(x_1 \dots x_k)
- предикат,t_1, \dots, t_k
- термы,p(t_1 \dots t_k)
- формула (атом)A, B
- формулы тогда,\bar A
,A \& B
,A \vee B
,A \rightarrow B
- формулыA(x)
- формула\exists x: A(x)
и\forall x: A(x)
- формулы Пример:\forall x: f(p(x)) \rightarrow \exists y: p(f(y))
U = N; 0 \in \mathbb N
x > y: \exists z, \overline{z = 0}: y + z = x
\forall x: A(x) = \bigwedge\limits_{u \in U} A(u)
\forall x: P(x) \vee \forall x: F(x) = \forall x: P(x) \vee \forall y: F(y)
\forall p: \left[ \left[ P(1) \& (\forall n: P(n) \rightarrow P(n+1)) \right] \rightarrow \forall n: P(n) \right]
P(x): \forall y \forall z: (x=y,z) \rightarrow (y=1 \vee \exists \nu: y = \nu+\nu)
Термы:
c \in Cn \Rightarrow c
- терм
x \in Var \Rightarrow x
- терм
f \in Fn; t_1, \dots, t_k
- термы
\Rightarrow f(t_1, \dots, t_k)
- терм
[!Пример]
L(x, y)
- x любит yC(x)
- корова лиh
- сено\forall x C(x) \rightarrow L(x, h)
- все коровы любят сено
Формулы
- Задаём утверждение U
P(x_1, \dots, x_k)
- к-местный предикантP^I(x_1, \dots, x_k)
- конкретный предикант на Uf(x_1, \dots, x_k) \rightarrow f^I(x_1, \dots, x_k)
- Инт. термов
(f(t_1, \dots, t_k))^I = f^I(t^I_1, \dots, t^I_k)
- Инт. связок
F=\bar A \rightarrow F^I=\overline{A^I}
F = A \vee B \rightarrow F^I = A^I \vee B^I
F = A\&B \rightarrow F^I=B^I\&B^I
(F = A \rightarrow B) \rightarrow (F^I = A^I \rightarrow B^I)