# Язык логики первого порядка
> [!Легенда]
> $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$

1. Нелогические символы
	1. Обозначения функций
	2. Обозначения предметов
	3. Обозначения констант
	4. Имена переменных

2. Логические символы
	1. Конъюнкция
	2. Отрицание
	3. Дизъюнкция
	4. Логическое следование
	5. Квантры ($\forall$, $\exists$)

3. Терм
	1. Переменные и константы
	2. $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$

4. Формулы (высказывания)
	1. $p(x_1 \dots x_k)$ - предикат, $t_1, \dots, t_k$ - термы, $p(t_1 \dots t_k)$ - формула (атом)
	2. $A, B$ - формулы тогда, $\bar A$, $A \& B$, $A \vee B$, $A \rightarrow B$ - формулы
	3. $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 любит y
> $C(x)$ - корова ли
> $h$ - сено
> $\forall x C(x) \rightarrow L(x, h)$ - все коровы любят сено


---
## Формулы
1. Задаём утверждение U
	$P(x_1, \dots, x_k)$ - к-местный предикант
	 $P^I(x_1, \dots, x_k)$ - конкретный предикант на U
	 $f(x_1, \dots, x_k) \rightarrow f^I(x_1, \dots, x_k)$
2. Инт. термов
	$(f(t_1, \dots, t_k))^I = f^I(t^I_1, \dots, t^I_k)$
3. Инт. связок
	$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)$