Математическая логика и теория алгоритмов

Приведем описание модальной системы S1 К. И. Льюиса (согласно [13]). В языке исчисления вводятся символы: \ ) р , д , г ...-символы для высказываний; 2) • , 0 - отрицание, конъюнкция (логическое произведение), возможность; 3) ),( - скобки. Определение формул: 1) каждый из символов p,q,r,... считается формулой; 2) если А и В формулы, то следующие выражения тоже формулы; ~А - отрицание А', А - В - конъюнкция А и В; ОА- возможно А; def AvB = ~((~^).(~S)); def Az:)B=~ A v B - материальная импликация (отметим, что в материальной импликации высказывание Az:)B истинно, если А ложно, что не всегда удобно. Почему, например, из того, что 2x2=5 следует, что Иванов - студент. В строгой импликации это уже устраняется); def А < В = ~ о ( А - (~В)) - строгая импликация Льюиса. « А ^ Б» читается «А имплицирует В» (здесь В выражает строгую имплика­ цию в отличие от ранеер а с с м о т р е н н о йВ строгой импликации из ложности высказывания 2x2=5, не следует, что Иванов ~ студент, ибо должно быть, что А-< В необходимо истинно); def А^В - (А<В) • (В ^ А),-г- знак строгой эквивалентности; def As В =i (А'эВ) • {BzdA) - материальная эквивалентность. Аксиомы: 210