Полнота и корректность в пропозициональной логике
РЕЗЮМЕ
В этом уроке рассматривается взаимосвязь между полнотой и корректностью в пропозициональной логике. Несмотря на то, что методы вывода и семантика в пропозициональной логике обсуждались широко, мало внимания уделялось взаимосвязи между этими двумя аспектами. Корректность относится к свойству логической системы, когда выражение G может быть выведено из множества выражений Γ, и, следовательно, G является (семантическим) следствием Γ. С другой стороны, полнота относится к свойству логической системы, когда, если G является семантическим следствием множества выражений Γ, то существует формальное доказательство с посылками Γ, из которого можно вывести G. Показано, что пропозициональная логика является корректной и полной, и приводится подробное объяснение каждого свойства. В частности, показано, как корректность выводится из структуры выводной системы пропозициональной логики, и как полнота выводится простым способом. Этот анализ имеет большое значение для понимания работы пропозициональной логики и для ее эффективного применения в различных областях знаний.
ЦЕЛИ ОБУЧЕНИЯ:
К концу этого урока студенты будут способны:
- Различать корректность и полноту в логической системе.
- Применять таблицу истинности для аксиом Лукашевича, чтобы доказать корректность пропозициональной логики.
- Объяснять как можно переписать modus ponens, используя семантическую версию теоремы о выводе.
- Понимать что корректность и полнота взаимосвязаны и могут быть выведены друг из друга.
- Анализировать концепцию тавтологии и ее связь с теоремами в пропозициональной логике.
СОДЕРЖАНИЕ
ПОЛНОТА И КОРРЕКТНОСТЬ В ПРОПОЗИЦИОНАЛЬНОЙ ЛОГИКЕ
ПРОПОЗИЦИОНАЛЬНАЯ ЛОГИКА КОРРЕКТНА
ПРОПОЗИЦИОНАЛЬНАЯ ЛОГИКА ПОЛНА
Полнота и корректность в пропозициональной логике
На этом этапе пришло время поговорить о полноте и корректности в пропозициональной логике. Оказывается, до сих пор много говорилось о методах вывода и семантике в пропозициональной логике, но все это было представлено таким образом, как будто это две полностью независимые стороны, не связанные между собой. На самом деле все наоборот.
КОРРЕКТНОСТЬ: Логическая система считается корректной, когда выражение G может быть выведено из множества выражений \Gamma, и, следовательно, G является (семантическим) следствием \Gamma. |
ПОЛНОТА: Система считается полной, если G является семантическим следствием множества выражений \Gamma, то существует формальное доказательство с посылками \Gamma, из которого можно вывести G. |
Рассмотрев эти идеи, мы увидим, что пропозициональная логика удовлетворяет условиям полноты и корректности.
Пропозициональная логика корректна
Получить корректность пропозициональной логики легко, наблюдая за структурой ее выводной системы. Если мы составим таблицу истинности для аксиом Лукашевича, то увидим, что они имеют такую структуру, которая всегда дает истинное значение, то есть:
| \models (\alpha \rightarrow (\beta \rightarrow \alpha)) |
| \models ((\alpha \rightarrow (\beta \rightarrow \gamma))\rightarrow ((\alpha \rightarrow \beta) \rightarrow (\alpha \rightarrow \gamma))) |
| \models ((\neg\beta \rightarrow \neg\alpha)\rightarrow(\alpha \rightarrow \beta)) |
Аналогичным образом, modus ponens можно переписать как \{\alpha,(\alpha\rightarrow \beta)\}\models \beta., что можно получить с использованием семантической версии теоремы о выводе. На самом деле, таким образом, мы получаем \{(\alpha\rightarrow \beta)\}\models (\alpha\rightarrow \beta),, а затем \models ((\alpha\rightarrow \beta)\rightarrow (\alpha\rightarrow \beta)),, что, конечно же, является очевидной тавтологией.
Пропозициональная логика полна
Полнота пропозициональной логики говорит нам, что, если B является семантическим следствием A, то B выводится из A. Иными словами: все истинные выражения имеют доказательство. Это то, что мы называем полнотой. Это можно вывести простым способом.
Это можно вывести простым способом. Предположим, что B не может быть выведено из A, или точнее \neg(A\vdash B), по теореме о выводе это эквивалентно утверждению: \neg (\vdash A\rightarrow B); теперь, если мы обратимся к корректности, это приводит к \neg(\models A \rightarrow B), что по теореме о выводе (семантическая версия) эквивалентно \neg(A\models B). В итоге мы получаем:
\neg(A\vdash B) \Rightarrow \neg(A\models B)
Что эквивалентно утверждению
(A\models B) \Rightarrow (A\vdash B)
Это означает, что, если A моделирует B, то B выводится из A. И если мы используем соответствующие теоремы о выводе, мы можем получить
(\models A\rightarrow B) \Rightarrow (\vdash A \rightarrow B)
Другими словами: если выражение является тавтологией, то оно является теоремой; и как мы видели, теоремы являются результатом доказательства.