Протологика: новый взгляд на природу логического (09.03.2010)

Автор: Шалак Владимир Иванович

ЧЕТВЕРТАЯ ГЛАВА - «Логика дефинициальной дедукции». В ней исследуем свойства дефиницальной вводимости, определенной в шестом параграфе третьей главы.

Параграф первый - «Основные свойства». Доказан ряд общих лемм о свойствах дефиницальной выводимости.

Лемма 1. Вывод ?; ? ? X имеет место, е. и т. е. для некоторого терма Y ? ? имеет место вывод ?; {Y} ? X.

Благодаря этой лемме при доказательстве свойств дефинициальной логики достаточно рассматривать выводы лишь из одноэлементного множества термов ?. В дальнейшем вместо ?; {Y} ? X мы будем использовать запись ?; Y ? X.

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

Теорема 1. (о консервативности определений) Если для множества определений ? и термов X, Y?L(?) не верно, что имеет место вывод ?; X > Y, то для любого нового определения Dx1…xn =def T вывод ??{Dx1…xn =def T}; X ? Y также не будет иметь места.

Параграф второй - «Функциональность». Дефинициальная логика обладает очень важным свойством, которое позволяет использовать ее для представления разннобразных функций. В специальной литературе оно получило название свойства ромба.

Теорема 2. Дефинициальная логика обладает свойством ромба. Если имеют место выводы ?; X ? Y и ?; X ? Z, то существует такой терм U, что имеют место выводы ?; Y ? U и ?; Z ? U.

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

Дефинициальное равенство термов. Два терма U, V?L(?) дефинициально равны (U =? V), если и только если существует такая последовательность термов <X0,…,Xn>, что n>0, X0 ? U, Xn ? V, и для всякого i<n либо Xi ? Xi+1, либо терм Xi+1 получен по правилу DE из терма Xi, либо терм Xi получен по правилу DE из терма Xi+1.

Теорема 3. U =? V, если и только если существует такой терм W, что ?; U ? W и ?; V ? W.

Редексы и свертки. Если Dx1…xn =def T – определение, то терм вида DY1…Yn будем называть редексом, а терм вида T[Y1/x1,…,Yn/xn] - сверткой данного редекса.

Нормальные формы.

Терм X находится в ?-нормальной форме, если и только если в него не имеет вхождения ни один редекс для определений ?.

Терм Y является ?-нормальной формой терма X, если Y находится в ?-нормальной форме, и ?; X ? Y.

Лемма 2.

Если ?; X ? Y, ?; X ? Z, и термы Y и Z находятся в ?-нормальной форме, то Y ? Z.

Если терм X имеет ?-нормальную форму, то она единственна.

Параграф третий - «Комбинаторная логика». Дефинициальная логика теснейшим образом связана с комбинаторной логикой Шейнфинкеля-Карри,, и ?-исчислением Чёрча.

Исходные символы языка:

x, y, z, … - переменные;

K, S – константы;

), ( - скобки.

Всякая переменная есть терм;

K и S - термы;

Если X и Y - термы, то (XY) – терм;

Ничто другое термом не является.

Термы-переменные и термы-константы будем называть атомарными термами. Терм, составленный лишь из констант K и S, будем называть комбинатором и выделять в тексте жирным шрифтом. При опускании в термах скобок предполагается их ассоциация влево. В комбинаторной логике изучают не термы сами по себе, а отношение редукции между ними, которое мы будем представлять посредством «?».

Редукции:

Если X и Y – термы, то X ?Y – редукция;

Ничто другое редукцией не является.

Аксиомы:

CA.1  X ? X

CA.2  KXY ? X

CA.3  SXYZ ? XZ(YZ)

Правила вывода:

CR.1   X ? Y  (  XZ ? YZ

CR.2   X ? Y  (  ZX ? ZY

CR.3   X ? Y,  Y ? Z  (  X ? Z

Иногда комбинаторную логику формулируют в терминах отношения конверсии, используя для его обозначения символ равенства «=». Для этого достаточно везде заменить символ «?» на «=» и добавить еще одно правило вывода:


загрузка...