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^IF = A\&B \rightarrow F^I=B^I\&B^I(F = A \rightarrow B) \rightarrow (F^I = A^I \rightarrow B^I)