III. Правила вывода ИВ

II. Правила построения формул ИВ.

Формулы ИВ определяются индуктивно, т.е. указываются неделимые атомные формулы, правила, по которым из заданных формул составляются новые, и постулируется, что никаких формул, кроме тех, которые являются таковыми согласно указанным правилам, нет.

Условимся обозначить в метаязыке произвольные формулы ИВ рукописными заглавными буквами из начала латинского алфавита: А,В,С,D ,…

1.Каждая отдельно взятая пропозициональная буква является формулой ИВ.

2.а) Если слово А является формулой ИВ, то слово ØА – тоже формула ИВ.

б) Если слова А и В являются формулами ИВ, то слово (АðВ), где знак ð обозначает в метаязыке произвольную двухместную связку из принятого списка основных связок ИВ, - тоже формула ИВ.

3. Слово из символов ИВ является формулой ИВ тогда, и только тогда, когда оно является таковой согласно ранее сформулированным правилам. При введении новых двухместных связок в сокращениях в метаязыке для соответствующих формул языка-объекта, сокращения записывают в виде, согласующемся с указанными правилами построения формул.

В метаязыке допускают сокращение числа скобок, используемых при записи формул; так, обычно опускают внешние скобки и некоторые другие, на основании соглашения о приоритете логических связок, определяя его местом связок в последовательности

Ø,Ú,Þ,Û:

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

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

 

Содержательно правило вывода – это алгоритм переработки заданных истин в другие. В метаязыке обозначают дробью вида.

где “числитель” Г - список известных истин – формул ИВ, определенной правилом вывода структуры. Формулы из списка Г называется посылками этого правила, а ”знаменатель”-формула А - их непосредственным следствием по рассматриваемому правилу.

Содержательно истины ИВ - это тавтологии. Поэтому правила вывода ИВ должны преобразовывать тавтологии в тавтологии. Можно указать много таких рецептов. Не все они независимы. Есть основные и производные или допустимые. Из бесчисленного множества возможных правил вывода в ИВ можно ограничиться двумя основными: МР и S, или даже одним - МР.

 

1.Modus ponens (лат.-способ вычеркивания или вычерчивания; название связано с проведением рассуждений с помощью знаков, вычерчиваемых прутиком на влажном песке пляжа). Коротко МР.

.

Если импликация и ее посылка истины, то истинно и заключение импликации. Содержательно это можно обосновать рассматривая таблицу истинности для импликации.

2. Подстановка. Коротко S (substitution)

Подстановка вместо всех вхождений пропозициональной переменной А в истинную формулу А(A) произвольной формулы В даст истинную формулу А(A/B).Содержательно это оправдано тем, что постоянная функция (тавтология) при cуперпонировании с любыми функциями остается постоянной (тавтологией).

Как правило, правилом подстановки избегают пользоваться явно, поскольку в выводе из гипотез его нельзя применять к гипотезам, в которых могут фигурировать фиксированные высказывания. Отказ от явного использования правила подстановки позволяет не различать вывод из гипотез и вывод.

Подстановка фактически означает, что пропозициональные переменные могут принимать в качестве значений формулы ИВ. Чтобы разделить объекты и средства исследования вводят метаязыковые переменные А, В, С ¼,отличные от пропозициональных и принимающие в качестве значений формулы ИВ. Возникает исчисление идентичное ИВ, но отличающееся интерпретацией: это ИВ применяемое к ИВ; формального различия нет. Однако, содержательно в метаязыковом ИВ каждая формула соответствует бесконечному числу формул ИВ-объекта, т.к. в них буквы А, В, С,…обозначают произвольные формулы ИВ-объекта (или, что то же самое, переменные А, В, С,…пробегают множество формул ИВ-объекта, или, что то же самое, принимают значения из указанного множества). Соответственно аксиомы в метаязыковом ИВ называют схемами аксиом ИВ-объекта т.к. при подстановке в каждую из них вместо метаязыковых пропозициональных букв произвольных формул ИВ–объекта т.к. при подстановке в каждую из них вместо метаязыковых пропозициональных букв произвольных формул ИВ-объекта (придания переменным А, В, С,¼ конкретных значений) получаем бесконечно много формул–аксиом ИВ–объекта. Можно было бы говорить и о схемах теорем языка-объекта, чего не принято делать.

3. Правило вывода в формулировке ИВ с единственной связкой – антиконъюнкцией ê и единственной схемой аксиом (см.ниже).

Легко проверить, воспользовавшись арифметическими выражениями для представляющих функций, что это действительно так: Аê(ВêC) = 1-А+АВС. Конечно в качестве заключения можно было бы написать и В. При С=В это правило есть МР, записанный через антиконъюнкцию.

Обычно постулируют несколько, не меньше одного, правил вывода, а многие другие используемые правила вывода получают с помощью постулированных основных как следствия развития теорем – их называют производными или допустимыми правилами.

 

IV. Аксиомы ИВ.

Содержательно аксиомы – это утверждения, рассматриваемые как истинные без доказательства. Выбор аксиом определяется компромиссом между желанием иметь поменьше постулируемых истин и удобством их использования. В отсутствие подстановки, как одного из основных правил вывода, речь должна идти о схемах аксиом, определяющих структуру формул, объявляемых аксиомами; число аксиом в этом случае бесконечно, но схем аксиом можно взять конечное число. Уменьшению числа аксиом или схем аксиом способствует их независимость, когда ни одна из схем аксиом не выводится из остальных.. Для ИВ вследствие полноты (выводимость всех истин–тавтологий) и существования разрешающей процедуры (т.е. алгоритма, позволяющего по любой формуле выяснить, является ли она истинной, тавтологией или теоремой, или нет) вопрос о числе и независимости аксиом скорее эстетический. В исследованиях (схем) аксиом на независимость находят применение многозначные логики. В приводимых ниже списках аксиом они подразумеваются (и так оно и есть) независимыми.

Если в качестве основных связок взять Ø,Ù,Ú.Þ, то удобный в смысле легкости содержательной интерпретации и легкости преобразования в систему (схем) аксиом ИИВ, список схем аксиом ИВ, включает 10 формул–тавтологий: (Kleene S.C. Introduction to Metamathematics—Princeton, 1952)

1.АÞ(BÞA),

2.(AÞВ)Þ((AÞ(BÞС))Þ(AÞС)); здесь можно поменять местами формулы (AÞВ) и(AÞ(BÞС)) без негативных последствий,

3.(АÞB)Þ((АÞС)Þ(АÞBÙС)).

4.(АÞВ)Þ((СÞB)Þ(AÚСÞВ)),

5.АÙBÞА,

6.АÙBÞB,

7.АÞAÚB,

8.ВÞAÚB,

9.(АÞB)Þ((AÞØB)ÞØA);

эту схему можно заменить в рамках ИВ на

9¢.(АÞØB)Þ(BÞØA)

без нарушения свойства полноты,

10.ØØАÞА.

Скажем, знак Û вводится как сокращение (АÛB):Û(АÞB)Ù(ВÞА)

Если в качестве основных связок взять Ø,Þ,то список (схем) аксиом сокращается до трех: 1, 2 и

3.(ØAÞØB)Þ((ØAÞB)ÞА).

Более того, можно было бы обойтись единственной схемой аксиом

(Meredith L.A. J. Comput. Syst. 3 , 155-164, 1953)

((((АÞB)Þ(ØСÞØD))ÞС)ÞE)Þ((EÞA)Þ(DÞА)).

Здесь связки Ù, Ú вводятся как сокращения ( в предыдущей формулировке это теоремы)

(AÙB):ÛØ(АÞØB)

(АÚB):ÛØAÞB

Если в качестве основных связок взять Ø, Ú, то можно взять аксиомы

(Hilbert D., Ackermann W. Grundzuge der theoretischen Logik. - Berlin,1938)

1.АÚAÞА,

2.АÞAÚB,

3.АÚBÞBÚA,

4.(ВÞС)Þ(АÚBÞАÚС)

(АÞB):ÛØАÚB

Для связок Ø,Ù схемы аксиом ИВ

(Rosser J.B. Logic for Mathematicians-New York, 1953)

1.АÞ(AÙA),

2.(АÙB)ÞA,

3.(АÞB)Þ(Ø(BÙС)ÞØ(СÙA))

с сокращением (АÞB):ÛØ(AÙØB)

Для единственной основной связки ½и единственного правила вывода

можно воспользоваться единственной схемой аксиом.

(Nicod J.C. Proc. Cambridge Phil. Soc, 19, 32-41, 1917)

(А ½(B½С)) ½{[ Dï(D ïD)]½[( E½B)½((A½E)½(AôE))]}

с сокращениями

ØA:ÛA½A,

(АÙB)Û(АïB)½(AôB),

(АÚB):Û(A½A)½(B½B),

(АÞB):ÛА½(B½B).

Это теоремы в основной формулировке для сокращения (А½B):ÛØ(AÙB).