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

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

Функциональная (не)полнота [ править ]

Сама по себе импликация не является функционально полным как логический оператор нельзя сформировать все другие двузначные функции истинности , поскольку из нее .

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

Однако если добавить нулевую связку ⊥ для обозначения ложности, то можно определить все остальные функции истинности. Формулы над полученным набором связок {→, ⊥} называются f-импликативными . ^[1] Если P и Q — предложения, то:

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

Поскольку известно, что вышеуказанные операторы функционально полны, отсюда следует, что любая функция истинности может быть выражена через → и ⊥.

Система аксиом [ править ]

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

Схема аксиом 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 — формула, то $\Gamma \vdash A$ означает, что A выводится с использованием приведенных выше аксиом и правил, а также формул из Γ в качестве дополнительных гипотез.

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

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

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

Основные свойства вывода [ править ]

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

Если

\Gamma \vdash A,

затем

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

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

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

Если

\Gamma ,A\vdash B

, затем

\Gamma \vdash A\to B.

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

Полнота [ править ]

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

Доказательство [ править ]

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

Доказательство аналогично полноте полной логики высказываний, но оно также использует следующую идею для преодоления функциональной неполноты импликации. Если A и F — формулы, то $A \to F$ эквивалентно $(\neg A*) \lor F,$ где A* — результат замены в A всех, некоторых или ни одного из вхождений F ложностью. Аналогично, $(A \to F) \to F$ эквивалентно $A* \lor F .$ Таким образом, при некоторых условиях их можно использовать вместо утверждений, что A* ложно или A* истинно соответственно.

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

A\to B,B\to C\vdash A\to C

( 1 )

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

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

( 2 )

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

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

( 3 )

Если мы далее предположим, что C → B , мы можем вывести

A \to B

, используя ( 1 ), тогда мы выведем C по modus ponens. Это показывает

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

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

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

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

Пусть F — произвольная фиксированная формула. Для любой формулы A определим $A 0 = (А \to F)$ и $А 1 знак равно ((А \to F) \to F).$ Рассмотрим только формулы с пропозициональными переменными p ₁ , ..., p _n . Мы утверждаем, что для каждой формулы A в этих переменных и каждого истинного назначения e ,

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

( 4 )

Докажем ( 4 индукцией по A. ) Базовый случай A = p _i тривиален. Пусть $А = (В \to С).$ Мы различаем три случая:

e ( C ) = 1. Тогда также e ( A ) = 1. Имеем
$(C\to F)\to F\vdash ((B\to C)\to F)\to F$
дважды применив ( 2 ) к аксиоме $C \to (B \to C).$ Поскольку мы получили $(C \to F) \to F$ по предположению индукции, мы можем сделать вывод $((B \to C) \to F) \to F .$
e ( B ) = 0. Тогда снова e ( A ) = 1. Теорема дедукции, примененная к ( 3 ), дает
$B\to F\vdash ((B\to C)\to F)\to F.$
Поскольку мы получили $B \to F$ по предположению индукции, мы можем сделать вывод $((B \to C) \to F) \to F .$
e ( B ) = 1 и e ( C ) = 0. Тогда e ( A ) = 0. Имеем
${\begin{aligned}(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{aligned}}$
таким образом $(B\to F)\to F,C\to F\vdash (B\to C)\to F$ по теореме дедукции. Мы вывели $(B \to F) \to F$ и $C \to F$ по предположению индукции, следовательно, мы можем сделать вывод $(B \to C) \to F .$ Это завершает доказательство ( 4 ).

теперь F — тавтология от переменных , _p1 ..., pn _.Пусть ,...,0 докажем Обратной индукцией по k = n , что для любого e назначения

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

( 5 )

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

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

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

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

{\begin{aligned}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{aligned}}

сначала установив 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 )) топор 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
П →( П → Р ) мп 4,6
( P →( P → R ))→ ((( P → R )→ R ) → ( P → R )) топор 2'
(( П → Р )→ Р )→( П → Р ) mp 7,8
((( P → R )→ R )→( P → R ))→( P → R ) топор 3
P → R mp 9,10

и обоснованность Выполнимость

Выполнимость в импликативном исчислении высказываний тривиальна, потому что каждая формула выполнима: просто присвойте всем переменным значение true.

Фальсифицируемость в импликативном исчислении высказываний NP-полна . ^[2] это означает, что достоверность (тавтология) является ко-NP-полной .

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

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

Предположим, что [( 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 → B истинно. Итак, С верно. Таким образом, А должно быть истинным, что противоречит тому факту, что оно ложно.

Таким образом, не существует оценки, которая делала бы (( 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. Это доказательство будет состоять из того же количества шагов ,

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

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

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

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

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

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

аа 5: Φ ₋ →(Φ ₊ →ꞈΦ)

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

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

Примеры:

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

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

Вывод аксиомы о подошвах Лукасевича

[(( P → Q )→ P )→(( P → P )→( S → P ))]→([(( P → Q ) → ( P → P ) ) → ( ( ( P → P ) → P )→( S → P ))]→[(( P → Q )→ R )→(( R → P )→( S → P ))]) aa 5
[(( P → P )→ P )→(( P → P )→( S → P ))]→([(( P →( P → P ))→ P )→(( P → P )→( S → P ))]→[(( P → Q )→ P )→(( P → P )→( S → P ))]) aa 5
П →( S → P ) аа 4
( P →( S → P ))→( P →(( P → P )→( S → P ))) аа 2
П →(( П → П )→( S → П )) mp 3,4
П → Па 1
( P → P )→(( P →(( P → P )→( S → P )))→[(( P → P )→ P )→ (( P → P )→( S → P ))] ) аа 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 → П ))] м.п. 9,2
П →( П → П ) аа 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
(( П → П )→ П )→( S → П ) mp 3,18
((( P → P )→ P )→( S → P ))→[(( P → Q )→( P → P ))→ ((( P → P )→ P )→( S → P )) ] аа 4
(( P → Q )→( P → P ))→((( P → P )→ P )→( S → P )) mp 19,20
(( P → Q )→ R )→(( R → P )→( S → P )) mp 21,16

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

См. также [ править ]

Ссылки [ править ]

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

^ Франкола, Джон; Голдсмит, Джуди; Шлипф, Джон; Шпекенмейер, Эвальд; Сваминатан, Р.П. (1999). «Алгоритм для класса чистых импликационных формул» . Дискретная прикладная математика . 96–97: 89–106. дои : 10.1016/S0166-218X(99)00038-4 .
^ Хойш, Питер (1999). «Сложность проблемы фальсифицируемости чистых импликационных формул» . Дискретная прикладная математика . 96–97: 127–138. дои : 10.1016/S0166-218X(99)00036-0 .

[1] Франкола, Джон; Голдсмит, Джуди; Шлипф, Джон; Шпекенмейер, Эвальд; Сваминатан, Р.П. (1999). «Алгоритм для класса чистых импликационных формул» . Дискретная прикладная математика . 96–97: 89–106. дои : 10.1016/S0166-218X(99)00038-4 .

[2] Хойш, Питер (1999). «Сложность проблемы фальсифицируемости чистых импликационных формул» . Дискретная прикладная математика . 96–97: 127–138. дои : 10.1016/S0166-218X(99)00036-0 .

[1]

[2]