Введение

В математической логике имплициальный высказывательный исчисление - это версия классического высказывательного исчисления, которая использует только один соединительный, называемый имплицией или условным. В формулах эта двоичная операция обозначается "implies", "if , then", "→", "", и т. д.

Полная информация

Имплициальный предложения исчисление семантически завершен в отношении обычных двух оцененных семантики классической логики предложения. То есть, если Γ представляет собой набор имплицитных формул, а A - имплицитная формула, связанная с Γ, то .

Добавление аксиомы

Что произойдет, если к вышеперечисленным будет добавлена другая схема аксиом? Есть два случая: (1) это тавтология; или (2) это не тавтология. Если это тавтология, то множество теорем остается множеством тавтологий, как и прежде. Однако в некоторых случаях можно найти значительно более короткие доказательства теорем. Тем не менее, минимальная длина доказательств теорем останется неограниченной, то есть для любого натурального числа n все еще будут теоремы, которые не могут быть доказаны в n или меньше шагов. Если новая схема аксиом не является тавтологией, то каждая формула становится теоремой (что делает понятие теоремы бесполезным в этом случае). Более того, существует верхняя граница минимальной длины доказательства каждой формулы, потому что существует общий метод доказательства каждой формулы. Например, предположим, что новая схема аксиом была ((B→C)→C)→B. Тогда ((A→(A→A))→(A→A))→A является экземпляром (одной из новых аксиом) и также не тавтологией. Но [((A→(A→A))→(A→A))→A]→A является тавтологией и, таким образом, теоремой из-за старых аксиомов (используя результат полноты выше). Применяя modus ponens, мы получаем, что A - теорема расширенной системы. Тогда все, что нужно сделать, чтобы доказать любую формулу, это заменить А на желаемую формулу на протяжении всего доказательства А. Это доказательство будет иметь такое же количество шагов, как доказательство А.