Математическая логика и теория алгоритмов. Для изучающих компьютерные науки

не следует, что Иванов - студент, ибо должно быть, что А-<:В необходимо ис­ тинно); def А-^В= (А -<В) • (В -< А), ^ знак строгой эквивалентности; def А =В = (А^В) (В^А) - материальная эквивалентность. Аксиомы: А1) р •q^q •р-, А2) р A3) р^р *р; А4) (р »q)r^p • (q » г) А5) р^~(~р); А6) (p^q) • (q^r) -^ф А7) р • (р^ч) Правила вывода следующие. Р1. Правило замены строго эквивалентным: любые два эквивалентных друг другу выражения взаимозаменяемы. Р2. Вместо любых переменных р, q, г,... можно подставить произвольную формулу. РЗ. Введение конъюнкции: из^, В выводится^4 •В. Р4. Modus pones со строгой импликацией: из А яА-^В выводится В. Если добавить к аксиомам системы S1 аксиому А8) 0(р • q) -<Ор, то получается система S2 Льюиса и S2 считается системой строгой импликации. Льюисом были предложены и другие системы модальной логики, в частности, системы S3- S5 и другие. Отметим, что в классической логике, например, из лжи следует, что угод­ но. Это иногда противоречит нашему содержательному, практическому пони­ манию логического следования. Для устранения этого парадокса материальной импликации Льюис и создал свои системы со строгой импликацией. По появи­ лись парадоксы и для строгой импликации. Для исключения парадоксов стро­ гой импликации Аккерман Ф. В. построил свою систему модальной логики. Кроме систем Льюиса и Аккермана, существуют системы Лукасевича и некоторые другие. Па втором этапе развития современной модальной логики были построены так называемые семантики возможных миров. Основным понятием в них явля­ 207