Тервер.asmАлгоритмыКомбалгJSMarkupHackWeb

Аксиоматическая система

Содержание:

У нас есть язык формальной логики. Зафиксируем из него некоторое множество формул. Будем называть их теоремами.

Фиксируем некоторое множество функций, определенных на множестве всех формул, со значениями в это же множество. Будет называть их правилами вывода.

Если $\phi$ - правило вывода, а формула $q = \phi(F_1, F_2, .., F_k)$, то формулу $q$ называют непосредственным следствием формул $F_1, F_2, .., F_k$, полученным с помощью правила $\phi$.

Обычно правила вывода пишут так: $\Large \frac{F_1, F_2, .., F_k}{q}$

Аксиоматическая система

Это такая тройка:

Выводимая формула

Формула называется выводимой в данной аксиоматической системе, если:

Других выводимых формул нет.

Формальная теорема

Выводимая формула, несовпадающая с аксиомой, называется формальной теоремой.

Непротиворечивость

Невозможность получить ложное утверждение из истины называется непротиворечивостью аксиоматической системы.

Непротиворечивой системой называется система, в которой нельзя вывести формулу и её отрицание.

Полнота

Если всякая тавтология выводима, то система называется полной.

Исчисление логики высказываний

Аксиоматическая система или исчисление логики высказываний это систему с набором аксиом и правилами вывода, описанными ниже.

Аксиомы

  1. $x_1 \to (x_2 \to x_1)$

    $(x_1 \to (x_2 \to x_3)) \to ((x_1 \to x_2) \to (x_1 \to x_3))$

  2. $x_1 \and x_2 \to x_1$

    $x_1 \and x_2 \to x_2$

    $(x_1 \to x_2) \to ((x_1 \to x_3) \to (x_1 \to x_2 \and x^3))$

  3. $x_1 \to x_1 \or x_2$

    $x_2 \to x_1 \or x_2$

    $(x_1 \to x_3) \to ((x_2 \to x_3) \to (x_1 \or x_2 \to x_3))$

  4. $(x_1 \leftrightarrow x_2) \to (x_1 \to x_2)$

    $(x_1 \leftrightarrow x_2) \to (x_2 \to x_1)$

    $(x_1 \to x_2) \to ((x_2 \to x_1) \to (x_1 \leftrightarrow x_2))$

  5. $x_1 \to ¬(¬x_1)$

    $¬(¬x_1) \to x_1$

    $(x_1 \to x_2) \to (¬x_2 \to ¬x_1)$

Правила вывода

  1. Правило подстановки

    Пусть $F$ и $G$ - некоторые формулы. Если в записи $F$ имеется литерал $x_n$, то все вхождения этого символа в формулу $F$ можно заменить на формулу $G$.

    Результат замены записывают так: $\large S^{x_n}_G(F)$

    А само правило замены: $\Large \frac{p, q, x_n}{S^{x_n}_G(F)}$

  2. Правило заключения (Modus Ponens)

    $\Large \frac{F, F \to G}{G}$

Доказательство

Доказательство формальной теоремы - процесс последовательного применения правил вывода для построения логического следования из аксиом к данной формуле.

Пример: Доказать, что формула $x_1 \to x_1$:

Подставим в аксиому 1.2 $x_1$ вместо $x_3$:

$(x_1 \to (x_2 \to x_1)) \to ((x_1 \to x_2) \to (x_1 \to x_1))$

Modus Ponens с аксиомой 1.1:

$((x_1 \to x_2) \to (x_1 \to x_1))$

Подставим $(x_2 \to x_1)$ вместо $x_2$:

$(x_1 \to (x_2 \to x_1) \to (x_1 \to x_1))$

Modus Ponens с аксиомой 1.1:

$x_1 \to x_1$

Выводимость формулы

Пусть у нас есть множество формул $\Gamma$.

Формула $F$ выводима из $\Gamma$ (пишут $\Gamma \vdash F$), если существует конечная последовательность $F_1, F_2, .., F_n$, такая, что $F_n = F$ и в которой $\forall F_i \in \Gamma$.

Формула выводима, если: