VI. Интерпретации

Пример вывода в ИВ

Докажем теорему ИВ

AÞА

- принцип тождества. В записи через Ù и Ú это закон исключительного третьего Ø A Ú A.

w 1.АÞ((АÞA)ÞA)

[A1 с А+А, В=АÞA]

2.(АÞ((AÞА)ÞA)Þ

((АÞ(AÞA))Þ(AÞA))

[A 2 с A=A, В=AÞА, С=А]

3 .(AÞ(AÞA))Þ(AÞA)

[МР из 1 и 2]

4.А Þ(AÞA)

[А1 с В=А]

5. АÞА

[МР из 3 и 4]4

1.Каноническая

2.Теоретико-множественная

3.Электротехническая

1.Каноническая. Пропозициональные переменные интерпретируются как переменные пробегающие двухэлементное множество истинностных значений: и–л, t–f, 1-0, 0-1.

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

2. Пусть формула А ИВ от переменных А_{1 ….,} Аn записана только через связки Ø,Ù,Ú, образующие полный набор зависимых связок. Обозначим через А^є(х) высказывание получающееся из А заменой пропозициональной переменной А_i на формулу хєХ_i Ø для всех i=1,…,n.

Через Х_А обозначим терм получающийся из формулы А ИВ заменой каждого из логических символов Ø,Ù,Ú на теоретико-множественные знаки С_Е,Ç,È соответственно, а каждой пропозициональной переменной А _i – на символ Х_i, обозначающий подмножество выбранного заранее универсального множества Е.

Тогда

( Ø A)^є(х)= Ø A^є (х)

(А Ù B)^є (х)= А^Є(х) Ù B^є(х)

(А Ú B)^є(х) = А^є (х) Ú В^є (х)

Х _{Ø A}=С_ЕХ_А

Х _{A Ù B}=Х_АÇ_В

Х _{А Ú B} =Х_АÈC _В

причем

А^Є(х) Û х Є Х_А.

wИндукция по числу шагов построения формулы А.

Для формулы А из одной пропозициональной переменной А, формула А^Є(х) есть х єХ, что совпадает с формулой х є Х_А, поскольку термин Х_А – это просто Х.

Пусть утверждение верно для формул получающихся в шагов (предположение индукции). Рассмотрим формулу полученную в n+1 шаг. Пусть она например имеет вид А Ù В, где А и В – формулы, которые строятся в шагов; конечно в сумме число шагов их построения равно именно n, чтобы А Ù В получалась в n+1 шаг. Для этих формул по предположению индукции

А^є(х) Û х є Х_А и В^Є(х) Û х є Х_В

По определению пересечения множеств имеем

Хє Х_А Ç C_В Û х є Х_А Ù х є Х_В Û А^є (х) Ù В^є(х) Û (А Ù В)^є (х)8

3. Пусть формула А ИВ от переменных А_1,¼,А_n записана только через связки Ø,Ù,Ú, образующие полный набор зависимых связок. Сопоставим такой формуле А электрическую цепь с двумя внешними подводящими (отводящими) контактами, составленную из пакетных двухпозиционных переключателей. В одном состоянии (положении) такого переключателя ток проходит через один набор пар его контактов, а в другом – через другой. Пакетному двухпозиционному переключателю сопоставим совокупность литералов формулы А, являющихся некоторой фиксированной пропозициональной переменной А или ее отрицанием Ø A. Формуле – литералу сопоставим цепь с одним размыкателем, возле которого напишем литерал, считая такую цепь замкнутой (проводящей) в основном “замкнутом” состоянии пакетного переключателя, если литерал есть пропозициональная буква и разомкнутой (непроводящей), если литерал есть отрицание соответствующей пропозициональной буквы; в “разомкнутом” состоянии пакетного переключателя все наоборот: цепь не проводит, если литерал есть буква и проводит, если он есть отрицание буквы

_____ А_____А_____ Ø А ____Ø А ____

Если формулам А и В уже сопоставлены электрические цепи рассматриваемого вида; то их конъюнкции А Ù B сопоставляется цепь полученная последовательным, а дизъюнкции А Ú В – параллельным соединением цепей сопоставленных формулам – составляющим:

если А ~ А

то

А Ù B ~ А В t ~

А Ú B ~ f ~

Cоответствие между формулами ИВ и электрическими цепями рассматриваемого вида биективно: цепи однозначно соответствует формула, формуле¾цепь.

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

а) упрощать цепи (уменьшить число размыкателей) упрощая соответствующие формулы с использованием алгебраических свойств связок;

б) строить цепи с заданной функцией проводимости от положений (состояний) пакетных переключателей, записывая эту функцию в терминах связок Ø,Ù,Ú. Это можно сделать как последовательными шагами, как в доказательстве выразимости всех связок через Ø,Ù,Ú, так и одним махом, воспользовавшись с.д.н.ф. или с.к.н.ф.

Теорема дедукции ( Эрбран Неrbrand J.; 1930)

В ИВ и равным образом в ИИВ справедлива теорема дедукции.

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

Иными словами это утверждение можно представить как правило вывода для секвенций (рецепт преобразования истинных секвенций в истинные)

3Будем доказывать более сильное утверждение: Всякий вывод какой-либо формулы В из гипотез Г, А можно преобразовать в вывод импликации А Þ В из гипотез Г.

Индукция по длине вывода, т.е. по числу формул в списке В₁,…, В_n который является выводом формулы В=В_n из списка гипотез Г, А.

Начальный шаг индукции. Рассмотрим n=1. По определению вывода тогда В₁ = В есть либо аксиома, либо одна из гипотез.

Вывод импликации А Þ B.

Если В = А – выделенная гипотеза, то используем вывод принципа тождества АÞA уже построенный ранее.

1. В [аксиома или гипотеза из Г ]

2. ВÞ(AÞ B) [А₁ с А ® B и В ® А]

3.АÞB [МР из 1 и 2].

Предположение индукции. Всякий вывод из гипотез Г, А какой-либо формулы В, который содержит не более чем n формул можно преобразовать в вывод импликации АÞB из гипотез Г.

Индукция. Рассмотрим какой-либо вывод В₁,…, В_n+1 какой-либо формулы В, из гипотез Г, А длины n+1.Преобразуем его в вывод импликации АÞВ из гипотез Г. Перебор случаев. Либо В аксиома, либо В одна из гипотез Г, либо В=А, либо В=В_n+1 есть следствие двух предыдущих формул В_i и В_j = (В_i Þ B_{n +1}) по МР. В первых трех случаях построения вывода импликации АÞB уже описано при осуществлении начального шага индукции. Впоследнем случае отрезки вывода, заканчивающиеся формулами В_i и В_j, - это по определению вывода – выводы этих формул имеющие длины Поэтому, по предположению индукции, они преобразуются в выводы импликаций А Þ B _i и (АÞB_j)=(АÞ(B_iÞB_n+1). Если к объединению этих выводов (когда, скажем все формулы второго из них записываются после всех формул первого), которое тоже является выводом из гипотез Г последней из формул т.е. АÞ В_j добавить

i. (AÞ(B_іÞB_n+1))Þ((AÞB_i)Þ(AÞB_n+1)) [А2 с В=В_i, C=B_n+1]

ii. (AÞB_i)Þ(AÞB_n+1) [МР из і. и АÞ(B_iÞВ_n+1)]

ііі. АÞB_n+1 [МР из іі. и АÞB_і]

получим вывод АÞB из гипотез Г 8.

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

В ИС это правило постулируется, а в ИВ в его справедливости можно убедиться воспользовавшись тавтологией (полнота ИВ означает, что это теорема ИВ).

((С Ù A)Þ(B Ú D))Þ(СÞ((AÞB) Ú D))

1 1 1 0 0 0 0 10 1 0 0 0 0

переводом секвенций и их правил вывода в формулы ИВ, МР, сечением. Конечно то же можно применить к теореме дедукции, опираясь на тавтологию:

((СÙA)ÞВ)Þ(СÞ(AÞB))

1 1 1 1 ж 0 0 1 0 1 0 0

Вывод теоремы дедукции не опирающийся на полноту ИВ позволяет использовать ее при доказательстве полноты ИВ.