Теорема дедукции

Содержание:

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

Если $\Gamma \cup {F} \vdash G$, то $\Gamma \vdash (F \to G)$

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

Пусть для формулы $G$ есть вывод, т.е. существует последовательность из $\Gamma \cup {F} : G_1, G_2, .., G_n = G$

Докажем индукцией по $n$:

• База индукции

  $n = 1$, тогда $G$:

  • либо формальная теорема

  • либо формула из $\Gamma$

    В этих случаях вывод строится так:
    
     $G, G \to (F \to G), F \to G$
    

  • либо $G = F$, поскольку Modus Ponens применять не к чему

     $G \to G = F \to G$
    

• Шаг индукции

  Пусть для $k < n$ уже доказано. Рассмотрим $k = n$

  Тогда $G$:

  • формальная теорема

  • формула из $\Gamma$

  • $G = F$

    Эти случаи не отличаются от варианта $n = 1$.

  • $G = G_n$ получена по правилу Modus Ponens из каких-то формул $G_a$ и $G_b$, где $a, b < n$.

    В этом случае $G_b$ должна иметь вид $G_b \to G_n$, чтобы применить Modus Ponens. Поскольку формулы $G_a$ и $G_b$ расположены в выводе формулы $G_n$, то всё, что написано перед каждой из них, это её вывод из $\Gamma \cup {F}$.

    По Переходу индукции для формул $F \to G_b = F \to (G_a \to G_n)$ и $F \to G_a$ есть вывод из $\Gamma$.