Теорема о полноте
Мы приведём два доказательства теоремы о полноте. Первое является «конструктивным», т. е. в нём описывается рецепт построения вывода для каждой тавтологии. Второе доказательство такого рецепта не даёт. Зато оно может применяться и для других формальных систем, когда идея первого доказательства не работает. В обоих доказательствах используется выводимость некоторых конкретных формул. Часть из них… Читать ещё >
Теорема о полноте (реферат, курсовая, диплом, контрольная)
Теорема 1.27 (полнота ИВ). Если формула является тавтологией, то она выводима в ИВ.
Мы приведём два доказательства теоремы о полноте. Первое является «конструктивным», т. е. в нём описывается рецепт построения вывода для каждой тавтологии. Второе доказательство такого рецепта не даёт. Зато оно может применяться и для других формальных систем, когда идея первого доказательства не работает.
В обоих доказательствах используется выводимость некоторых конкретных формул. Часть из них уже встречалась выше. Остальные приводятся в следующей лемме.
Лемма 1.28. В ИВ выполняются выводимости:
Доказательство. По теореме дедукции из леммы 1.16 следует утверждение (1.3), а из (1.3) следует (1.4).
Покажем, как построить вывод для (1.5). Поскольку Л, Л—"С IС (применение modus ponens к гипотезам), то В Ь (Л—>С)—>С (теорема дедукции). Из леммы 1.25 (б) следует, что (В—*С)—>С h 1C—>1(Л—>С). Значит, из транзитивности вывода (лемма 1.23) получаем Л Ь 1C—>~|(Л—>С). Теперь для получения искомого вывода формулы 1(Л—>С) из гипотез Л, 1C осталось применить правило modus ponens к гипотезе 1C и формуле 1C—Я (Л—>С).
Приведём вывод для (1.6).
Теперь докажем (1.7). Достаточно построить вывод 1Л—)А, Л—>А I- А
aside class="viderzhka__img" itemscope itemtype="http://schema.org/ImageObject">
и дважды применить теорему дедукции. ?