Это читается как: если ложь истинна, то любое предложение C истинно.
Отрицание похоже на импликацию.
A true u ⋮ p true A true I u , p A true A true C true E {\displaystyle {\cfrac {\begin{matrix}{\cfrac {}{A{\hbox{ true}}}}\ u\\\vdots \\p{\hbox{ true}}\end{matrix}}{\lnot A{\hbox{ true}}}}\ \lnot _{I^{u,p}}\qquad {\cfrac {\lnot A{\hbox{ true}}\quad A{\hbox{ true}}}{C{\hbox{ true}}}}\ \lnot _{E}}
Правило введения освобождает как от названия гипотезы u , так и от последующего p , т.е. предложение p не должно встречаться в заключении A . Поскольку эти правила схематичны, интерпретация правила введения такова: если из " A true " мы можем вывести для каждого предложения p , что " p true ", то A должно быть ложным, т. е. "не true ". Для исключения, если показано, что и A , и не A являются истинными, то возникает противоречие, и в этом случае каждое предложение C истинно. Поскольку правила для импликации и отрицания настолько схожи, должно быть довольно легко увидеть, что не A и A ⊃ ⊥ эквивалентны, то есть каждое из них выводимо из другого.
Последовательность, полнота и нормальные формы
Говорят, что теория непротиворечива, если ложность не доказуема (без каких-либо допущений) и полна, если каждая теорема или ее отрицание доказуемы с использованием правил логического вывода. Это утверждения, касающиеся всей логики, и обычно они привязаны к некоторому понятию модели . Однако существуют локальные понятия согласованности и полноты, которые являются чисто синтаксическими проверками правил вывода и не требуют обращения к моделям. Первым из них является локальная согласованность, также известная как локальная сводимость, которая гласит, что любое производное, содержащее введение связки, за которым немедленно следует ее исключение, может быть превращено в эквивалентное производное без этого обхода. Это проверка на прочность правил исключения: они не должны быть настолько сильными, чтобы включать знания, которые еще не содержатся в их предпосылках. В качестве примера рассмотрим союзы.
A true u B true w A ∧ B true ∧ I A true ∧ E 1 ⇒ A true u {\displaystyle {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\ {\text{true}}}}u\qquad {\cfrac {}{B\ {\text{true}}}}w}{A\wedge B\ {\text{true}}}}\wedge _{I}}{A\ {\text{true}}}}\wedge _{E1}\end{aligned}}\quad \Rightarrow \quad {\cfrac {}{A\ {\text{true}}}}u}
В двойственном смысле локальная полнота говорит о том, что правила исключения достаточно сильны, чтобы разложить связку на формы, подходящие для ее правила введения. Снова для союзов:
A ∧ B true u ⇒ A ∧ B true u A true ∧ E 1 A ∧ B true u B true ∧ E 2 A ∧ B true ∧ I {\displaystyle {\cfrac {}{A\wedge B\ {\text{true}}}}u\quad \Rightarrow \quad {\begin{aligned}{\cfrac {{\cfrac {{\cfrac {}{A\wedge B\ {\text{true}}}}u}{A\ {\text{true}}}}\wedge _{E1}\qquad {\cfrac {{\cfrac {}{A\wedge B\ {\text{true}}}}u}{B\ {\text{true}}}}\wedge _{E2}}{A\wedge B\ {\text{true}}}}\wedge _{I}\end{aligned}}}
Эти понятия в точности соответствуют β -редукции (бета-редукции) и –преобразованию ( eta -преобразованию) в лямбда-исчислении , использующем изоморфизм Карри-Ховарда ( Curry - Howard isomorphism ),,,. С помощью локальной полноты мы видим, что каждое производное может быть преобразовано в эквивалентное производное, где вводится основная соединительная. Фактически, если весь вывод подчиняется этому порядку исключений, за которыми следуют введения, то он называется нормальным. При нормальном выводе все исключения происходят выше введений. В большинстве логик каждый вывод имеет эквивалентный нормальный вывод, называемый нормальной формой . Существование нормальных форм, как правило, трудно доказать, используя только естественную дедукцию, хотя такие описания существуют в литературе, в первую очередь, написанные Дагом Правицем в 1961 году. [7] Гораздо проще показать это косвенно с помощью представления последовательного исчисления разрезов .