Files

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

  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)