Импликационное исчисление высказываний

редактировать

В математической логике импликационное исчисление высказываний является версией классическое исчисление высказываний, в котором используется только одна связка, называемая импликацией или условным. В формулах эта двоичная операция обозначается как «подразумевает», «если..., то...», «→», « $→ {\ displaystyle \ rightarrow}$ $\ rightarrow$ "и т. д.

Содержание

1 Виртуальная полнота как оператор
2 Система аксиом
3 Основные свойства вывода
4 Полнота
- 4.1 Доказательство
5 Система аксиом Бернейса – Тарского
6 Проверка того, является ли формула импликативного исчисления высказываний тавтологией
7 Добавление схемы аксиом
8 Альтернативная аксиоматизация
9 См. Также
10 Ссылки

Виртуальная полнота как оператор

Одно только следствие не функционально завершенное как логический оператор, потому что нельзя сформировать все другие двузначные истина функционирует от него. Однако, если у кого-то есть пропозициональная формула , которая известна как ложь и использует ее, как если бы она была нулевой связкой для ложности, тогда можно определить все другие функции истинности. Так что импликация в качестве оператора практически завершена. Если P, Q и F - предложения и F заведомо ложно, то:

¬P эквивалентно P → F
P ∧ Q эквивалентно (P → (Q → F)) → F
P ∨ Q эквивалентно (P → Q) → Q
P ↔ Q эквивалентно ((P → Q) → ((Q → P) → F)) → F

В более общем смысле, поскольку известно, что указанные выше операторы являются функционально полными, отсюда следует, что любую функцию истинности можно выразить в терминах «→» и «F», если у нас есть предложение F, которое заведомо ложно.

Стоит отметить, что F нельзя определить из → и произвольных переменных предложения: любая формула, построенная из → и пропозициональных переменных, должна получить значение true, если все ее переменные оценены как истинные. Как следствие, {→} не является функционально полным. Например, его нельзя использовать для определения двухзначной функции истинности, которая всегда возвращает false.

Система аксиом

Следующие утверждения считаются тавтологиями (несводимыми и интуитивно истинными по определению).

Схема аксиом 1 - это P → (Q → P).
Схема аксиом 2 - это (P → (Q → R)) → ((P → Q) → (P → R)
Схема аксиомы 3 (закон Пирса ): ((P → Q) → P) → P.
Одно ненулевое правило вывод (modus ponens ): из P и P → Q вывести Q.

Где в каждом случае P, Q и R могут быть заменены любыми формулами, которые содержат только "→ "как связующее. Если Γ - это набор формул, а A - формула, то $Γ ⊢ A {\ displaystyle \ Gamma \ vdash A}$ $\ Gamma \ vdash A$ означает, что A выводится с использованием аксиом и правил выше и формул из Γ как дополнительные гипотезы.

Лукасевич (1948) нашел систему аксиом для импликационного исчисления, которая заменяет схемы 1–3, приведенные выше, единственной схемой

((P → Q) → R) → ((R → P) → (S → P)).

Он также утверждал, что не существует более короткой системы аксиом.

Основные свойства вывода

Поскольку все аксиомы и правила исчисления являются схемами, вывод закрывается при подстановке :

Если

Γ ⊢ A, {\ displaystyle \ Гамма \ vdash A,}

\ Gamma \ vdash A,

, затем

σ (Γ) ⊢ σ (A), {\ displaystyle \ sigma (\ Gamma) \ vdash \ sigma (A),}

\ sigma (\ Gamma) \ vdash \ sigma (A),

где σ - любая подстановка (формул, использующих только импликацию).

Импликационное исчисление высказываний также удовлетворяет теореме дедукции :

Если

Γ, A ⊢ B {\ displaystyle \ Gamma, A \ vdash B}

\ Gamma, A \ vdash B

, то

Γ ⊢ A → B. {\ displaystyle \ Gamma \ vdash A \ to B.}

\ Gamma \ vdash A \ to B.

Как объясняется в статье теорема дедукции, это справедливо для любого аксиоматического расширения системы, содержащего схемы аксиом 1 и 2 выше и modus ponens.

Полнота

Импликативное исчисление высказываний семантически полное по отношению к обычной двузначной семантике классической логики высказываний. То есть, если Γ - это набор импликативных формул, а A - импликационная формула , вытекающая из из Γ, то $Γ ⊢ A {\ displaystyle \ Gamma \ vdash A}$ $\ Gamma \ vdash A$ .

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

Доказательство теоремы о полноте приводится ниже. Во-первых, используя теорему компактности и теорему дедукции, мы можем свести теорему о полноте к ее частному случаю с пустым Γ, т.е. нам нужно только показать, что каждая тавтология выводима в системе.

Доказательство похоже на полноту полной логики высказываний, но оно также использует следующую идею для преодоления функциональной неполноты импликации. Если A и F - формулы, то A → F эквивалентно (¬A *) ∨ F, где A * - результат замены в A всех, некоторых или ни одного из вхождений F на ложь. Точно так же (A → F) → F эквивалентно A * ∨ F. Таким образом, при некоторых условиях их можно использовать в качестве замены для утверждения, что A * ложно или A * истинно соответственно.

Сначала рассмотрим некоторые основные факты о выводимости:

A → B, B → C ⊢ A → C {\ displaystyle A \ to B, B \ to C \ vdash A \ to C}

A \ к B, B \ к C \ vdash A \ к C

(1)

Действительно, мы можем вывести A → (B → C), используя аксиому 1, а затем вывести A → C по modus ponens (дважды) из Ax. 2.

A → B ⊢ (B → C) → (A → C) {\ displaystyle A \ to B \ vdash (B \ to C) \ to (A \ to C)}

A \ to B \ vdash (B \ к C) \ к (A \ to C)

(2)

Это следует из (1) по теореме дедукции.

A → C, (A → B) → C ⊢ C {\ displaystyle A \ to C, (A \ to B) \ to C \ vdash C}

A \ to C, (A \ to B) \ to C \ vdash C

(3)

Если мы далее предположим, что C → B, мы можем вывести A → B с помощью (1), тогда мы получим C по modus ponens. Это показывает

A → C, (A → B) → C, C → B ⊢ C {\ displaystyle A \ to C, (A \ to B) \ to C, C \ to B \ vdash C}

A \ to C, (A \ to B) \ to C, C \ to B \ vdash C

, и теорема дедукции дает

A → C, (A → B) → C ⊢ (C → B) → C {\ displaystyle A \ to C, (A \ to B) \ to C \ vdash (C \ to B) \ to C}

от A \ к C, (от A \ к B) \ к C \ vdash (C \ to B) \ к C

. Применяем Axe. 3, чтобы получить (3).

Пусть F - произвольная фиксированная формула. Для любой формулы A определим A = (A → F) и A = ((A → F) → F). Рассмотрим только формулы в пропозициональных переменных p 1,..., p n. Мы утверждаем, что для каждой формулы A в этих переменных и каждого присвоения истинности e,

p 1 e (p 1),…, pne (pn) ⊢ A e (A). {\ Displaystyle p_ {1} ^ {e (p_ {1})}, \ dots, p_ {n} ^ {e (p_ {n}) } \ vdash A ^ {e (A)}.}

p_ {1} ^ {e (p_ {1})}, \ dots, p_ {n} ^ {e (p_ {n})} \ vdash A ^ {e (A)}.

(4)

Докажем (4) индукцией по A. Базовый случай A = p i тривиален. Пусть A = (B → C). Различаем три случая:

e (C) = 1. Тогда также e (A) = 1. Имеем
$(C → F) → F ⊢ ((B → C) → F) → F {\ displaystyle (C \ to F) \ to F \ vdash ((B \ to C) \ to F) \ to F}$ $(C \ to F) \ to F \ vdash ((B \ to C) \ to F) \ to F$
, применяя (2) дважды к аксиоме C → (B → C). Поскольку мы вывели (C → F) → F по предположению индукции, мы можем вывести ((B → C) → F) → F.
e (B) = 0. Тогда снова e (A) = 1. Теорема дедукции, примененная к (3), дает
$B → F ⊢ ((B → C) → F) → F. {\ displaystyle B \ to F \ vdash ((B \ в C) \ к F) \ к F.}$ $B \ to F \ vdash ((B \ to C) \ to F) \ to F.$
Поскольку мы вывели B → F по предположению индукции, мы можем вывести ((B → C) → F) → F.
e (B) = 1 и e (C) = 0. Тогда e (A) = 0. Имеем
$(B → F) → F, C → F, B → C ⊢ B → F по (1) ⊢ F по modus ponens, { \ Displaystyle {\ begin {align} (B \ to F) \ to F, C \ to F, B \ to C \ vdash B \ to F {\ text {by (1)}} \\ \ vdash F { \ text {by modus ponens,}} \ end {align}}}$ ${\ begin {align} (B \ to F) \ to F, C \ to F, B \ to C \ vdash B \ to F {\ text {by (1)}} \\ \ vdash F {\ text {by modus ponens,}} \ end {выровнено}}$
таким образом $(B → F) → F, C → F ⊢ (B → C) → F {\ displaystyle (B \ to F) \ to F, C \ to F \ vdash (B \ to C) \ to F}$ $(B \ to F) \ к F, C \ к F \ vdash (B \ к C) \ к F$ по теореме дедукции. Мы вывели (B → F) → F и C → F по предположению индукции, следовательно, мы можем вывести (B → C) → F. Это завершает доказательство (4).

Теперь пусть F - тавтология от переменных p 1,..., p n. Докажем обратной индукцией по k = n,..., 0, что для любого присваивания e,

p 1 e (p 1),…, pke (pk) ⊢ F. {\ Displaystyle p_ {1} ^ {e (p_ {1})}, \ dots, p_ {k} ^ {e (p_ {k})} \ vdash F.}

{\ displaystyle p_ {1} ^ {e (p_ {1})}, \ dots, p_ {k} ^ {e (p_ {k})} \ vdash F.}

(5)

Базовый случай k = n следует из частного случая (4) с использованием

F e (F) = F 1 = ((F → F) → F) {\ displaystyle F ^ {e (F)} = F ^ {1} = ((F \ to F) \ to F)}

{\ displaystyle F ^ {e (F)} = F ^ {1} = ((F \ to F) \ to F)}

и тот факт, что F → F является теоремой по теореме дедукции.

Предположим, что (5) выполняется для k + 1, мы покажем это для k. Применяя теорему дедукции к предположению индукции, получаем

p 1 e (p 1),…, pke ( pk) ⊢ (pk + 1 → F) → F, p 1 e (p 1),…, pke (pk) ⊢ ((pk + 1 → F) → F) → F, {\ displaystyle {\ begin {выровнено } p_ {1} ^ {e (p_ {1})}, \ dots, p_ {k} ^ {e (p_ {k})} \ vdash (p_ {k + 1} \ to F) \ to F, \\ p_ {1} ^ {e (p _ {1})}, \ dots, p_ {k} ^ {e (p_ {k})} \ vdash ((p_ {k + 1} \ to F) \ to F) \ to F, \ end { выровненный}}}

{\ displaystyle {\ begin {align} p_ {1} ^ {e (p_ {1 })}, \ dots, p_ {k} ^ {e (p_ {k})} \ vdash (p_ {k + 1} \ to F) \ to F, \\ p_ {1} ^ {e (p_ {1})}, \ dots, p_ {k} ^ {e (p_ {k})} \ vdash ((p_ {k + 1} \ to F) \ to F) \ to F, \ end {выровнено }}}

, сначала установив e (p k + 1) = 0, а второй установив e (p k + 1) = 1. Из этого мы получаем (5), используя modus ponens.

При k = 0 получаем, что тавтология F доказуема без предположений. Вот что нужно было доказать.

Это доказательство конструктивно. То есть, учитывая тавтологию, можно было бы действительно следовать инструкциям и создать доказательство этого из аксиом. Однако длина такого доказательства экспоненциально возрастает с увеличением числа пропозициональных переменных в тавтологии, следовательно, это не практический метод для каких-либо тавтологий, кроме самых коротких.

Система аксиом Бернейса – Тарского

Часто используется система аксиом Бернейса – Тарского. В частности, в статье Лукасевича аксиомы Бернейса – Тарского выводятся из единственной аксиомы Лукасевича как средства демонстрации ее полноты.. Она отличается от схем аксиом, приведенных выше, заменой схемы аксиом 2, (P → (Q → R)) → ( (P → Q) → (P → R)), с

схемой аксиом 2 ': (P → Q) → ((Q → R) → (P → R))

, которая называется гипотетический силлогизм. Это несколько затрудняет вывод мета-теоремы о дедукции, но это все же возможно.

Покажем, что из P → (Q → R) и P → Q можно вывести P → R. Этот факт можно использовать вместо схемы аксиом 2 для получения мета-теоремы.

P → (Q → R) для данного
P → Q для данного
(P → Q) → ((Q → R) → (P → R)) ax 2 '
(Q → R) → (P → R) mp 2,3
(P → (Q → R)) → (((Q → R) → (P → R)) → (P → (P → R))) ax 2 '
((Q → R) → (P → R)) → (P → (P → R)) mp 1,5
P → (P → R) mp 4,6
(P → (P → R)) → (((P → R) → R) → (P → R)) ax 2 '
((P → R) → R) → (P → R) mp 7,8
(((P → R) → R) → (P → R)) → ( P → R) ax 3
P → R mp 9,10 qed

Проверка того, является ли формула импликативного исчисления высказываний тавтологией

В этом случае полезной техникой является предполагаем, что формула не является тавтологией, и пытаемся найти оценку, которая делает ее ложной. Если удастся, то это действительно не тавтология. Если не получается, то это тавтология.

Пример нетавтологии :

Предположим, [(A → B) → ((C → A) → E)] → ([F → ((C → D) → E)] → [(A → F) → (D → E)]) ложно.

Тогда (A → B) → ((C → A) → E) верно; F → ((C → D) → E) верно; A → F верно; D верно; и E ложно.

Поскольку D истинно, C → D истинно. Таким образом, истинность F → ((C → D) → E) эквивалентна истинности F → E.

Тогда, поскольку E ложно и F → E истинно, мы получаем, что F ложно.

Поскольку A → F истинно, A ложно. Таким образом, A → B истинно и (C → A) → E верно.

C → A ложно, поэтому C истинно.

Значение B не имеет значения, поэтому мы можем произвольно выбрать его как истинное.

Подводя итог, оценка, которая устанавливает B, C и D как истинные, а A, E и F, как ложные, сделает [(A → B) → ((C → A) → E)] → ([F → ((C → D) → E)] → [(A → F) → (D → E)]) ложно. Так что это не тавтология.

Пример тавтологии :

Предположим, что ((A → B) → C) → ((C → A) → (D → A)) ложно.

Тогда (A → B) → C верно; C → A верно; D верно; и A ложно.

Поскольку A ложно, A → B истинно. Итак, C верно. Таким образом, A должно быть истинным, что противоречит тому факту, что оно ложно.

Таким образом, не существует оценки, которая делает ((A → B) → C) → ((C → A) → (D → 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 - теорема расширенной системы. Тогда все, что нужно сделать, чтобы доказать любую формулу, - это заменить A на нужную формулу на протяжении всего доказательства A. Это доказательство будет иметь такое же количество шагов, что и доказательство A.

Альтернативная аксиоматизация

Перечисленные выше аксиомы в основном работают через метатеорему дедукции, чтобы прийти к полноте. Вот еще одна система аксиом, которая прямо нацелена на полноту, минуя дедуктивную метатеорему.

Во-первых, у нас есть схемы аксиом, которые предназначены для эффективного доказательства подмножества тавтологий, содержащих только одну пропозициональную переменную.

aa 1: ꞈA → A
aa 2: (A → B) → ꞈ (A → (C → B))
aa 3: A → ((B → C) → ꞈ ((A → B) → C))
aa 4: A → ꞈ (B → A)

Доказательство каждой такой тавтологии начнется с двух частей (гипотезы и заключения), которые одинаковы. Затем вставьте между ними дополнительные гипотезы. Затем вставьте дополнительные тавтологические гипотезы (которые верны, даже если единственная переменная ложна) в исходную гипотезу. Затем добавьте еще гипотез снаружи (слева). Эта процедура быстро даст каждую тавтологию, содержащую только одну переменную. (Символ «ꞈ» в каждой схеме аксиом указывает, где начинается вывод, используемый в доказательстве полноты. Это просто комментарий, а не часть формулы.)

Рассмотрим любую формулу Φ, которая может содержать A, B, C 1,..., C nи заканчивается A в качестве окончательного заключения. Затем мы берем

aa 5: Φ - → (Φ + → ꞈΦ)

в качестве схемы аксиомы, где Φ - является результатом замена B на A во всем Φ и Φ + является результатом замены B на (A → A) во всем Φ. Это схема схем аксиом, поскольку существует два уровня подстановки: в первом подставляется Φ (с вариациями); во втором любая из переменных (включая как A, так и B) может быть заменена произвольными формулами импликативного исчисления высказываний. Эта схема позволяет доказать тавтологии с более чем одной переменной, рассматривая случай, когда B ложно Φ -, и случай, когда B истинно Φ +.

Если переменная, которая является окончательным выводом формулы принимает значение true, тогда вся формула принимает значение true независимо от значений других переменных. Следовательно, если A истинно, то Φ, Φ -, Φ + и Φ - → (Φ + → Φ) - все правда. Итак, без ограничения общности, мы можем считать, что A ложно. Обратите внимание, что Φ является тавтологией тогда и только тогда, когда и Φ -, и Φ + являются тавтологиями. Но в то время как Φ имеет n + 2 различных переменных, Φ - и Φ + имеют n + 1. Таким образом, вопрос о том, является ли формула тавтологией, свелся к вопросу о том, являются ли все определенные формулы с одной переменной каждой тавтологией. Также обратите внимание, что Φ - → (Φ + → Φ) является тавтологией независимо от того, является ли Φ, потому что если Φ ложно, то либо Φ -, либо Φ + будет ложным в зависимости от того, является ли B ложным или истинным.

Примеры:

Вывод закона Пирса

[((P → P) → P) → P] → ([((P → (P → P)) → P) → P] → [((P → Q) → P) → P]) aa 5
P → P aa 1
(P → P) → ((P → P) → ( ((P → P) → P) → P)) aa 3
(P → P) → (((P → P) → P) → P) mp 2,3
((P → P) → P) → P mp 2,4
[((P → (P → P)) → P) → P] → [((P → Q) → P) → P] mp 5,1
P → (P → P) aa 4
(P → (P → P)) → ((P → P) → (((P → ( P → P)) → P) → P)) aa 3
(P → P) → (((P → (P → P)) → P) → P) mp 7,8
((P → (P → P)) → P) → P mp 2,9
((P → Q) → P) → P mp 10,6 qed

Получение Лукасевича единственная аксиома

[((P → Q) → P) → ((P → P) → (S → P))] → ([((P → Q) → (P → P)) → ((( P → P) → P) → (S → P))] → [((P → Q) → R) → ((R → P) → (S → P))]) аа 5
[((P → P) → P) → ((P → P) → (S → P))] → ([((P → (P → P)) → P) → ((P → P) → ( S → P))] → [((P → Q) → P) → ((P → P) → (S → P))]) аа 5
P → (S → P) аа 4
(P → (S → P)) → (P → ((P → P) → (S → P))) aa 2
P → ((P → P) → (S → P)) mp 3,4
P → P aa 1
(P → P) → ((P → ((P → P) → (S → P))) → [((P → P) → P) → ((P → P) → (S → P))]) aa 3
(P → ((P → P) → (S → P))) → [((P → P) → P) → ((P → P) → (S → P))] mp 6,7
((P → P) → P) → ( (P → P) → (S → P)) mp 5,8
[((P → (P → P)) → P) → ((P → P) → (S → P)) ] → [((P → Q) → P) → ((P → P) → (S → P))] mp 9,2
P → (P → P) aa 4
(P → (P → P)) → ((P → ((P → P) → (S → P))) → [((P → (P → P)) → P) → ((P → P) → (S → P))]) аа 3
(P → ((P → P) → (S → P))) → [((P → (P → P)) → P) → ((P → P) → (S → P))] mp 11,12
((P → (P → P)) → P) → ((P → P) → (S → P)) mp 5,13
((P → Q) → P) → ((P → P) → (S → P)) mp 14,10
[((P → Q) → (P → P)) → ( ((P → P) → P) → (S → P))] → [((P → Q) → R) → ((R → P) → (S → P))] mp 15,1
(P → P) → ((P → (S → P)) → [((P → P) → P) → (S → P)]) aa 3
(P → ( S → P)) → [((P → P) → P) → (S → P)] mp 6,17
((P → P) → P) → (S → P) mp 3, 18
(((P → P) → P) → (S → P)) → [((P → Q) → (P → P)) → (((P → P) → P) → (S → P))] aa 4
((P → Q) → (P → P)) → (((P → P) → P) → (S → P)) mp 19, 20
((P → Q) → R) → ((R → P) → (S → P)) mp 21,16 qed

Использование таблицы истинности для проверки единственной аксиомы Лукасевича будет требует рассмотрения 16 = 2 случаев, так как содержит 4 различных переменных. В этом выводе мы смогли ограничить рассмотрение только тремя случаями: R - ложь, Q - ложь, R - ложь, Q - истина, а R - истина. Однако, поскольку мы работаем в рамках формальной системы логики (а не вне ее, неформально), каждый случай требовал гораздо больше усилий.

См. Также

Ссылки

Мендельсон, Эллиот (1997) Введение в математическую логику, 4-е изд. Лондон: Chapman Hall.
Лукасевич, Ян (1948) Кратчайшая аксиома импликационного исчисления предложений, Proc. Королевская ирландская академия, т. 52, сек. А, нет. 3, стр. 25–33.