И удаления пропози-

циональных связок

ПІ Sem ML

Логическое исчисление в виде натурального вывода обладает следующими особенностями:

а) название данного исчисления как натурального объясняется тем, что в нем процесс вывода в наибольшей степени приближен к обычным человеческим рассуждениям. То есть «натуральное» употребляется не в смысле неформального, не регламентированного сстрогими правилами, а в смысле получения следствия из произвольных допущений (гипотез) в отсутствие аксиом.

б) преимуществом S³ перед S² считается то, что в натуральных выводах процесс введения пропозициональных сязок получения следствия заметно короче. Как известно, в S² одна и та же формула может встречаться в структуре доказательства несколько раз, что значительно реже происходит в S³;

в) в S³ осуществляется определенная систематизация правил вывода. Каждой пропозициональной связке ставится в соответствие одно правило ее введения и одно правило ее удаления как главного знака формулы [наличие двух правил УК (удаления конъюнкции), ВД (введения дизъюнкции), УЕ (удаления эквиваленции) не яется существенным и не противоречит только что сказанному].

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

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

Например, формула А É В может быть введена, если наличествует заключение В из допущения А, то есть если верно, что А |- В.

Пименяя к формуле А É В правило УИ (удаления импликации), мы действуем так, как если бы В было выводимым из доказанного А, а это оказывается возможным в силу того, что формула А É В в посылке применения правила УИ регистрирует существование заключения В из А.

Систематизация правил введения и удаления пропозициональных связок принадлежит известному немецкому математику и логику Герхарду Генцену (1909-1946 гг.). Поэтомуиногданатуральные исчисления называют «генценовские исчисления».

Запишем правила (фигуры) заключения для S³:

1. G, А |- В _ (ВИ) 2. А, А É В (УИ)

G |- А É В В

3. А, В (ВК) 4. А & В; А & В (УК)

А & В А В

5. А__; В___ (ВД) 6. G, А |- С G, В |- С (УД)

А Ú В А Ú В G, А Ú В |- С

7. G, А |- В G, А |- Ø В (ВО)

G |- Ø А

8. Ø Ø А __ (УДО) А, Ø А (Сл. УО) - слабое удаление

А В отрицания

9. А É В, В É А (ВЭ) 10. А º В; А º В (УЭ)

А º В А É В В É А

 

Над чертой в каждом правиле записаны посылки, а под чертой – результат примененияправил. Каждое правило содержит одно заключение, в то время как посылок может быть несколько (что приводит к существованию однопосылочных, двухпосылочных и т.д. правил).

Все «правила введения» вводят соответствующую связку в заключение применения правила, а каждое «правило удаления» удаляет соответствующую связку из посылок. Исключение составляет лишь правило УД: дизъюнкция А Ú В скорее в нем «вводится», чем удаляется. Однако данное правило можно записать в непарадоксальном виде:

А Ú В G, А |- С G, В |- С

G |- С

 

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

[ A] [ A ] [ B ]

B __ (ВИ), А Ú В Ú С (УД)

А É В С

[ A ] [ A ]

В Ø В __ (ВО)

Ø А

 

Квадратные скобки укзывают на то, что в них находятся допущения (гипотезы).

В нашей системе S³ будем знак |- считать исходным.

При использовании этого знака в доказательствах и выводимотсях имеют в виду следующие его войства:

а) А |- А - рефлексивность виводимости;

б) если G Í D и G |- А, то D |- А (где G и D - произвольные списки формул, А - формула).

Данное свойство фиксирует тот факт, что если формула А выводима из множества посылок, то она остается выводимой, если к G добавить дополнительные посылки. Другими словами, если А |- В, то С, А |- В;

в) G |- А тогда и только тогда, когда в G существует конечное подмножество формул D такое, что D |- А ;

г) если D |- А и G |- В для любой формулы В из D, то G |- А. Другими словами, если А |- В и В |- С, то А |- С (транзитивность |- ).

Собственно говоря, все перечисленные свойства знака |- справедливы и для S².

Рассмотрим теперь определение доказательства в S³.. В отличие от правил вывода в S², которые используютя только для выведения одних доказанных выражений из других, в натуральном исчислении правила вывода могут применяться к любым ПП- выражениям.

Выражение, которое вытекает согласно некоторому правилу из доказанного выражения, само является доказанным. Однако выражение, вытекающее из недоказанного выражения, еще не является доказанным. В последнем случае необходимо каким-то образом избавиться от использованных допущений. В приведенных правилах заключения для S³ только два првила позволяют избавиться от допущений: (ВИ) и (ВО), только они удаляют гипотезу А из списка гипотез.

Поскольку в S³ отсутствуют аксиомы, то доказательство в S³ осноывается либо на правиле введения импликации, либо на правиле введения отрицания.

⇐ Предыдущая102103104105106107108109110111Следующая ⇒