Содержание к диссертации
Введение
Глава 1 Простые паранормальные логики I0, WP, AIP и IAP ...8
1.1 Исчисления HIo, HVVP, HAIP и HIAP и аксиоматизируемые ими логики I0, WP, AIP и IAP 8
1.2 Простая паранормальность логик I0, WP, AIP и IAP 16
1.3 Погружающие отображения, устанавливающие связь логик 1о и WP с классической пропозициональной логикой и логик AIP и IAP с интуиционистской пропозициональной логикой. Аналог теоремы В.И.Гливенко, устанавливающий связь логики 1о с логикой AIP и логики VVP с логикой IAP 50
Глава 2 Семантический анализ логик 10 и VVP 70
2.1 Семантика обобщённых описаний состояния для логики 10 и четырёхзначная характеризация этой логики 70
2.2 Семантика квазиописаний состояния для логики WP 115
2.3 Несуществование конечной характеристической матрицы для логики WP 117
Глава 3 Семантический анализ логик AIP и IAP 121
3.1 Семантика в стиле С.Крипке для логики AIP 121
3.2 Семантика в стиле С.Крипке для логики IAP 154
3.3 Несуществование конечных характеристических матриц для логикАІРиІАР 160
Заключение 162
Литература 163
- Простая паранормальность логик I0, WP, AIP и IAP
- Погружающие отображения, устанавливающие связь логик 1о и WP с классической пропозициональной логикой и логик AIP и IAP с интуиционистской пропозициональной логикой. Аналог теоремы В.И.Гливенко, устанавливающий связь логики 1о с логикой AIP и логики VVP с логикой IAP
- Семантика квазиописаний состояния для логики WP
- Семантика в стиле С.Крипке для логики IAP
Введение к работе
В предлагаемом диссертационном исследовании проводится семантический анализ ряда простых паранормальных логик \ Что такое простая паранормальная логика? Точный ответ на этот вопрос будет дан в главе 1. Здесь укажем только на то, что простые паранормальные логики являются разновидностью паранормальных логик, т.е. логик, которые одновременно являются паранепротиворечивыми и параполными. При этом паранепротиворечивая логика - это логика, для которой существует паранепротиворечивая теория, основывающаяся на этой логике (т.е. такая противоречивая теория, основывающаяся на этой логике, которой (теории) не принадлежит некоторое высказывание, сформулированное в языке этой теории), а параполная логика это - логика, для которой существует параполная теория, основывающаяся на этой логике (т.е. такая неполная теория Т, основывающаяся на этой логике, что всякая полная теория, сформулированная в языке теории Т, основывающаяся на этой же логике и включающая Т, является множеством всех высказываний языка теории Т).
Заметим, что часто употребляемый в логической литературе термин «паралогика» используется для обозначения любой логики, которая является паранепротиворечивой или\и параполной логикой. Таким образом, всякая паранормальная (а значит, и всякая простая паранормальная) логика есть паралогика.
У истоков исследований паралогик стоят Н.А. Васильев и Я.Лукасевич, пионерские работы [11] и [48], которых в области паралогик относятся к 10-м годам XX столетия. С полным основанием паралогиками могут быть названы логика, построенная И.Е.Орловым в [29], логика, построенная Д.А. Бочваром в [8], и, конечно, дискуссивная логика, построенная С.Яськовским в [46]. Изучение паралогик принадлежит сфере научных интересов: австралийских логиков Р.К.Мейера (R.K.Meyer), Г.Приста (G.Prist), Р.Роутли (R.Routley), Д.Хайда (D.Haid), австрийского логика П.Вайнгартнера (P.Weingartner), бельгийского логика Д.Батенса (D.Batens), бразильских логиков А.Арруды (A.Arruda), Н.Да Косты (N.C.A.Da Kosta), И.М.Л.Д Оттавиано (I.M.L.D Ottaviano), А.М.Сетте (A.M.Sette), грузинского логика Л.И.Мчедлишвили, израильского логика А.Аврона (A.Avron), испанского логика Л.Пена (L.Pena), немецких логиков В.Аккермана (W.Ackermann), В.А.Карниелли (W.A. Carnielli), Г.Вансинга (H.Wansing), польских логиков Е.Зарнецка-Биали (E.Zamecka-Bialy) Г.Малиновского (G.Malinowski), Е.Пежановского (J.Perzanowski), логиков из США А.Р.Андерсона (A.R.Anderson), Н.Д.Белнапа (N.D.Belnap), Дж.М.Данна (J.M.Dunn), Г.Е.Минца (G.Mints), Д.Фауста (D.Faust), А.Чёрча (A.Church), украинских логиков А.Т.Ишмуратова и Я.Шрамко, японских логиков С.Акама (S.Akama) , К.Накаматсу (K.Nakamatsu), Х.Оно (Н.Опо), Т.Сугихара (T.Sugihara). В России паралогики изучались В.А.Бажановым, П.И.Быстровым, В.Л.Васюковым, Е.К.Войшвилло, В.В.Донченко, Н.М.Ермолаевой, Д.В.Зайцевым, А.А.Ивиным, Ю.В.Ивлевым, А.С.Карпенко, Л.Л.Максимовой, А.А.Мучником, С.П.Одинцовым, В.М.Поповым, О.В.Поповым, М.И.Семененко, О.Ф.Серебрянниковым, Е.А.Сидоренко, А.В.Смирновым, В.А.Смирновым, Е.Д.Смирновой, В.К.Финном,В.И.Шалаком.
Исследование паралогик конституировалось в самостоятельный раздел современной логики во второй половине 70-х годов XX века. Особенно интенсивно идет изучение паранепротиворечивых логик. К настоящему времени массив работ по паранепротиворечивым логикам труднообозрим, работ по паралогикам значительно меньше, а работы, специально посвященные анализу паранормальных логик, единичны.
Актуальность темы обусловлена тем, что в настоящее время всё большее значение приобретает применение неклассических логик при решении вопросов философского, методологического и конкретно-научного характера. При этом плодотворным оказывается использование специального типа неклассических логик - паралогик.
Общеизвестно, что при изучении логических систем важную роль играет исследование проблемы их семантической характеризации. В предлагаемой работе проведен семантический анализ ряда хорошо мотивированных с дедуктивной точки зрения паранормальных логик.
Целью работы является проведение семантического анализа простых паранормальных логик.
Для достижения указанной цели решены следующие задачи:
(1) задача, состоящая в доказательстве адекватности варианта семантики обобщённых описаний состояния паранормальной логике 10 (этот вариант семантики обобщённых описаний состояния и логика 10 сформулированы в [49]);
(2) задача, состоящая в доказательстве адекватности варианта семантики квазиописаний состояния паранормальной логике VVP (этот вариант семантики квазиописаний состояния и логика VVP сформулированы в [32]);
(3) задача, состоящая в доказательстве адекватности четырёхзначной матрицы М0 из [49] логике 10;
(4) задача, состоящая в доказательстве того, что не существует конечной характеристической матрицы для логики VVP;
(5) задача, состоящая в доказательстве адекватности семантики, основанной на понятии AIP-модели, паранормальной логике AIP (эта семантика и логика AIP сформулированы в [33]);
(6) задача, состоящая в доказательстве адекватности семантики, основанной на понятии IAP-модели, паранормальной логике IAP (эта семантика и логика IAP сформулированы в [33]).
Научная новизна исследования состоит в следующем:
(1) проведён семантический анализ паранормальных логик Io, VVP, AIP и IAP, являющихся важнейшими логиками в классе всех простых паранормальных логик, и установлены (посредством аналогов теоремы В.И.Гливенко) связь логики 1о с логикой AIP и логики VVP с логикой IAP;
(2) доказана адекватность варианта семантики обобщённых описаний состояния логике 10 и доказана адекватность варианта семантики квазиописаний состояния логике VVP;
(3) доказано, что логика 1о имеет четырёхзначную характеристическую матрицу, но ни одна из логик VVP, AIP и IAP не имеет конечной характеристической матрицы;
(4) доказана адекватность семантики базарующейся на понятии AIP- модели, логике AIP, и доказана адекватность семантики, базирующейся на понятии ІАР-модели, которое, наряду с понятием АІР-модели, является обобщением понятия модели Крипке для интуиционистской пропозициональной логики, логике ІАР.
Методологическая основа исследования.
В ходе исследования применяются классическая математическая логика первого порядка с равенством и теоретико-множественные принципы, не выходящие за рамки системы ZFC.
Используются методы построения семантик, основывающихся на различных понятиях родственных понятию описания состояния, метод построения семантик крипкевского типа, алгебраический метод изучения логики с помощью её характеристической матрицы, а также методы изучения логик посредством соответствующих гильбертовских и секвенциальных исчислений.
Основные результаты, полученные в диссертации:
(1) предложено доказательство сформулированной в [49] теоремы адекватности варианта семантики обобщённых описаний состояния логике 1о;
(2) предложено доказательство теоремы адекватности сформулированного В.М.Поповым варианта семантики квазиописаний состояния логике VVP;
(3) предложено доказательство сформулированной в [49] теоремы о четырёхзначной характеристической матрице логике 10;
(4) предложено оригинальное доказательство теоремы о несуществовании конечной характеристической матрицы логики VVP;
(5) предложено доказательство сформулированной в [33] теоремы адекватности семантики, основанной на понятии AIP-модели, логике АІР;
(6) предложено доказательство сформулированной в [33] теоремы адекватности семантики, основанной на понятии IAP-модели, логике ІАР.
(7) предложено доказательство следующего аналога теоремы В.И.Гливенко , доказанной им в [44]:
формула принадлежит логике 10 тогда и только тогда, когда двойное отрицание этой формулы принадлежит логике АІР;
сформулирован и доказан также ещё один аналог указанной теоремы В.И.Гливенко:
формула принадлежит логике VVP тогда и только тогда, когда двойное отрицание этой формулы принадлежит логике ІАР.
Практическая значимость работы
Описанные в диссертации подходы к построению семантик паранормальных логик могут применяться при конструировании семантик и для других паралогик. Изученные здесь семантики находят применение при решении вопроса о принадлежности формулы логикам, соответствующим этим семантикам. Результаты диссертационного исследования можно использовать при чтении спецкурсов по неклассическим логикам.
Символы «V», «3», «= » и « = » используются в метаязыке в качестве сокращения для «все», «некоторые», «если..., то...» и «тогда и только тогда, когда» соответственно, а символ «N» - для обозначения множества всех натуральных чисел, отождествляемого со множеством всех целых положительных чисел. Остальная символика вводится в основном тексте диссертации. Допускается автонимное употребление символов.
Автор приносит глубокую благодарность заведующему кафедрой логики философского факультета МГУ им. М.В.Ломоносова профессору В.И.Маркину за предоставленную автору возможность прочитать 27.09.05 доклад по теме диссертационного исследования на заседании кафедры, заведующему сектором логики ИФРАН профессору А.С.Карпенко за необходимые автору консультации по библиографии паранормольных логик и за предоставленную автору возможность выступить с докладом по теме диссертации на заседании сектора логики ИФРАН 20.09.05, профессору Ю.В.Ивлеву и кандидату философских наук В.О.Шангину за ценные указания по оформлению текста диссертации, профессору В.А.Бочарову и доценту Д.В.Зайцеву, прочитавшим текст диссертации и давших автору ряд полезных советов, научному руководителю диссертационного исследования доценту В.М.Попову за интеллектуальную помощь и моральную поддержку.
Простая паранормальность логик I0, WP, AIP и IAP
24 (21) (V 5 ІЯІЛЄЕІМ}) \А « v-MG{l,t}. В є Г Снимая допущение (16) и обобщая, получаем, что (22)Vv((V5 \B\VME {l,t})= I A ti \vMe {l,t}). v есть оценка языка C в матрице М0 В є Г Снимая допущение (15), получаем, что (23) А п есть аксиома исчисления HI0 = V v ((V В В VM є {1, t}) == v есть оценка языка в матрице М0 В є Г = \А п. Iv e {l,t». (24) 3 к 3 I (Ak, А і, Ап ) есть применение MP (допущение) к, /є N, 1 ,/ " Пусть (25) к?, І є N, 1 к!, I ri и (A , Ay, An) есть применение MP. (26) Формула Л/ есть формула (А D Ап) (из того, что (АКь Af, Ап) есть применение MP (см. (25)), по определению применения MP) (27)Vv((V \в\ущ є {l,t})= \АК vMe {1, t}) (из того, что я v есть оценка языка в матрице М0 В є Г (см. (25)), по индуктивному допущению) (28)Vv((V ІЯІЛє {l,t})= ( D „0lvMe {l,t}) (из того, что v есть оценка языка в матрице М0В еГ Г п (см. (25)) и (26), по индуктивному допущению) (29) Vv ((V В В VM є {1, t}) = \Ап. І „ є {1, t}) (из (27) и (28), по v есть оценка языка в матрице М0 В є Г лемме 1.2.3) Снимая допущение (24), получаем, что (30) 3 к 3 / ЛЬ Ah Ап) есть применение MP = Vv ((V В \ В VM є {1, t}) = к, І є Н, ] к, 1 п v есть оценка языка в матрице М0 В є Г U lvMe{l,t}). (31)Уу((У5І5кМоє{1,1}) Л кМє{1,1})(из(7),(14),(23)и(30)) v есть оценка языка в матрице М0 В є Г Снимая допущение (3), получаем, что (32)Г \-ШоА Vv((V в\в\« є {l,t}) UJvMG{l,t}). v есть оценка языка в матрице М0 В є Г Снимая допущения (1), (2) и обобщая, получаем, что \/А\/Г(ГЫъА = Vv((V я„мє {l,t})= Ы„Моб {l,t})). А есть формула Г есть множество формул v есть оценка языка в матрице М0 В є Г Теорема 1.2.1 доказана. Теорема 1.2.2 V (I-H,O = VV ULM=i). А есть формула v есть оценка языка X в матрице М0 Доказательство (1) 4 есть произвольная формула такая, что h-шА (допущение) (2) 0 У-цьА (из (1), по соглашению об обозначении) (3)0hH1,/= Vv((V5 \в\,ме {l,t})= U vMe {1,і})(изтого, v есть оценка языка X в матрице М0 В є 0 что А есть формула и 0 есть множество формул, по теореме 1.2.1) Очевидно, что (4)Vv((V„Me {U})= \A \vMoe {l,t}) = Vv \A \vMoe {l,t} v есть оценка языка X в матрице М0 В є 0 v есть оценка языка X в матрице М0 (5)VvU vM"e{l,t}(H3(2),(3)H(4)) v есть оценка языка , в матрице М0 Возвратной индукцией по длине Н10-доказательства легко установить, что (6) V А (Нню А = А не есть пропозициональная переменная) А есть формула (7) А не есть пропозициональная переменная (из (1) и (6)) (8) Vv \А VMO є {1, 0} (из (7), по лемме 1.2.1) v есть оценка языка в матрице М0 (9)Vv М„м=1(из(5)и(8)) v есть оценка языка X в матрице М0 Снимая допущение (1) и обобщая, получаем, что V (I-HI. = VV \A\VMO=\). А есть формула v есть оценка языка X в матрице М0 Теорема 1.2.2 доказана. Следствием теоремы 1.2.2 и того, что 1«, = {А \ \ нъ А }, является теорема 1.2.3. Теорема 1.2.3 \/А(А eI„= Vv UvMo=l). А есть формула v есть оценка языка X в матрице М0 Лемма 1.2.4 Логика 10 является паранепротиворечивой логикой. Доказательство Обозначим через w множество {(/?, 0) І р є Prop up не есть/?,} \J {(/?„ t)}. Ясно, что w есть оценка языка в матрице MQ. Докажем, что {А\ А є Form и \А \ „м є {1, t}} есть 10-теория. Согласно определению 10-теории достаточно доказать, что: (І)І0с{ЛІ А Є Form И \А \WM Є {l,t}}, (II) для всяких формул А И В верно следующее: А є {А А є Form и \А LM Є {1, t}} и (A D В) є {A \ А є Form и ULMoe {l,t}}= є И I Л e Form и \A\WME {l,t}}. Справедливость утверждения (I) очевидна в силу теоремы 1.2.3. Докажем теперь утверждение (II). (1) А и В есть формулы (допущение) (2) А е {А А є Fom и U WM є {1, t}} (допущение) (3) (Л D 5 ) є {А Л є Form и \А \WM Є {1, t}} (допущение) (4) U LMoe{l,t}(H3(2)) (5) lG4 DB )LMoe{l,t}(H3(3)) (6) U LMo = 1 или \A LMO = t (из (4)) (7) I (Л D B ) LMo = 1 или (Л D 5 ) LMo = t (из (5)) Используя лемму 1.2.1, получаем, что (8) l04 D )LM t. (9) I {A1 D В ) LM = 1 (из (7) и (8)) (10) \А \ WM = 1 (допущение) (11) В \WM = 1 или В LMo = t (из (9) и (10), по определению \ущ и по табличному определению операции Э+) (12) i? LMoe{l,t}(H3(ll)) Снимая допущение (10), получаем, что (із) U LM = i= \B \WM {i,t . (14) U LM = t (допущение) (15) B LMo = 1 или B LMo = t (из (9) и (14), по определению I VM и по табличному определению операции Э+) (16) kLMe{l,t}(H3(15)) Снимая допущение (14), получаем, что (17) ULMo = t= \B \wMe {l,t}. (18) Ы„Мое{и}(из(6),(13)и(17)) Снимая допущения (1), (2), (3) и обобщая, получаем, что (II). Утверждение (II) доказано. Итак, {А А є Form и \А J e {1, t}} есть 10-теория. Эта 10-теория является паранепротиворечивой 10-теорией. Действительно, обе формулы рх и (-і /?i) принадлежат данной теории, но она не является тривиальной теорией т.к. р2, например, не принадлежит этой теории. Таким образом, существует паранепротиворечивая 10-теория. А значит, согласно определению паранепротиворечивой логики (см. определение Df 1.1.9), получаем, что 10 является паранепротиворечивой логикой. Лемма 1.2.4 доказана. Нам потребуется следующая лемма 1.2.5. Лемма 1.2.5 Пусть L\ есть логика, L2 есть паранепротиворечивая логика и L\ c:L2. Тогда L\ есть паранепротиворечивая логика. Доказательство (1) L\ есть логика (условие) (2) L2 есть паранепротиворечивая логика (условие) (3) L\ с L2 (условие) (4) Существует паранепротиворечивая 1,2-теория (из (2), по определению паранепротиворечивой логики) Пусть (5) Т есть паранепротиворечивая Х2-теория. (6) Т есть замкнутое относительно MP множество формул и12сТ (из (5), по определению /,2-теории) (7) Т есть замкнутое относительно MP множество формул и L\ сТ (из (3) и (6)) (8) Т есть L\-теория (из (7), по определению L\-теории) (9) Т Ф Form и З А (А є Ти(— А) є Т) (из (5), по определению А есть формула паранепротиворечивой / -теории) (10) Т есть паранепротиворечивая / -теория (из(8) и (9), по определению паранепротиворечивой теории заданной логики) (11) Существует паранепротиворечивая Z-i-теория (из(10)) (12) Li есть паранепротиворечивая логика (из (1) и (11), по определению паранепротиворечивой логики) Лемма 1.2.5 доказана. Теорема 1.2.4 Всякая логика из {I0, VVP, AIP, IAP } является паранепротиворечивой логикой. Доказательство Из леммы 1.2.4, леммы 1.2.5 и того, что каждая логика из {I0, VVP, AIP, IAP } включается в 10 (см. стр.15), получаем, что всякая логика из {I0, WP, AIP, LAP } является паранепротиворечивой логикой. Теорема 1.2.4 доказана. Очевидна следующая лемма 1.2.6 Лемма 1.2.6 Пусть L є {I0, WP, АІР, ІАР }, Т есть теория логики L и (-і (/?, D /?і)) є Т. Тогда Т есть тривиальная теория. Лемма 1.2.7 Пусть А есть формула и w = {(/?, 0) І р є Prop ир не есть/?,} и { /?„ f)}. Тогда (a) w есть оценка языка в М0, (б) \А \ wMo є {1, 0, f}. Доказательство (1) А есть формула (условие) (2) w ={ /?, 0) І /? є Pro/? и/? не есть/?,} и { /?„ t)} (условие) Справедливость утверждения (а) в условиях данной леммы очевидна. Согласно определению формулы верно, что (3) А є Prop, или ЗА\А есть (—і 41), или 3 А\ 3 А2 А есть (А\ & А2), или Л, є Form AhA2 є Form ЗА\ЗАгА есть (Лі V А2), или ЗА\ЗА2А есть (41 D Л2). Ai,A2s Form AuA2e Form (4) Л є Pro/? (допущение) (5) \A\WM= w {А) (из (4) и (а), по определению значения формулы при заданной оценке X в М0) (6) w (А) є {0, f) (из (2) и (4)) В свете (6) очевидно, что (7)w(A)e{l,0,f}. (8) ULMe{l,0,f}(ro(5)H(7)) Снимая допущение (4), получаем, что (9)А eProp \A\wMe {l,0,f}. (10) З А і А есть (-і А і) (допущение) А\ є Form Пусть (11) А! \ есть формула и А есть (—, А \). (12) I (-. А і) и,м= -i+ A } I WM (из того, что А і есть формула (см. (11) и (а), по определению значения формулы при заданной оценке X в М0) (13)-п+ \А\\„М«Є {1,0} (из того, что А \ есть формула (см. (11) и (а), по табличному определению операции -.+) В свете (13) очевидно, что (14) -п+ U ,LMoe {1,0, f}. (15) \(г,АЧ) /ЧЕ{1,0,1}(ИЗ(12)И(14)) Снимая допущение (10), получаем, что (16)ЭЛ,Лесть(-,Л,)= \A\WMOE {1,0, f}. А і є Form (\7)ЗАіЗА2А есть (Аі & A2), (допущение) AuA2e Form Пусть (18) A\, A 2 есть формулы, А есть (A \ & A 2). (19) (Л , & Л 2) LMo= \A i LMO &+ U 2LM (из того, что Л ,, Л 2 есть формулы (см. (18)) и (а), по определению значения формулы при заданной оценке языка в матрице Мо) (20) U i „M &+ \А 2 І „МЄ {1, 0} (из того, что А\, А 2 есть формулы см. (18) и (а), по табличному определению операции &+) В свете (20) очевидно, что (21) U ,LMo&+ \A 2\wMoe{l,0,f}. (22) \(А\&А 2) \wMe {1, 0, f} (из (19) и (21)) Снимая допущение (17), получаем, что (23)ЗАіЗА2Ае(Угь(Аі&А2)= Ы„,ме {l,0,f}. Ai,A2e Form Рассуждениями, аналогичными приведенному выше рассуждению, обосновывающему утверждение (23), обосновываются следующие два утверждения ( ) и ( ): ( ) ЗАХЗА2 А есть (Л, V 2)= ULMe {1,0, f}, А\,А2е Form ( ) З Ах З А2 А єсть (Ах Э Л2) = \А\„М Є {l,0,f}. А\, А2 є Form ( ) \Л LMO Є {1,0, f} (из (3),(9), (16),(23), ( ) и ( )) Итак, в условиях доказываемой леммы верно, что (б). Лемма 1.2.7 доказана. Лемма 1.2.8 Пусть Н є {HIo, HWP, НАІР, НІАР }, п є N, Аи ..., Ап є Form, последовательность А\9 ...9 Ап формул есть Н-вывод из множества {(р, D (-. (р, D /?,))), ((-./?,) Э (-, (р, D р,)))}, и = { р, 0) I р є Prop ир не есть/?,} u { p„f }. Тогда (а) и есть оценка языка X в М0, (б) Ап \ WM = 1. Доказательство (1) Н є {HIo, HWP, НАІР, НІАР} (условие) (2) п є N (условие) (3) Ах, ...,Ап є Form (условие) (4) последовательность А\ ...9 Ап формул есть Н-вывод из множества {(р, D D (-, (p, D/?,))), ((-і/?,) Э (-, (p, Dp,)))} (условие) (5) и = {(p, 0) I /? є Prop ир не естьр,} u {(/?„ f } (условие) Справедливость утверждения (а) в условиях данной леммы очевидна. зо Используя возвратную индукцию по п, покажем, что в условиях доказываемой леммы верно утверждение (б). Согласно определению Н-вывода из множества формул, верно, что (6) А„ есть аксиома исчисления Н, или Ап есть формула (р, D (— (р, Э Эpi))), или Ап есть формула ((-ірО Э (-і (рх Dр())), или 3 i3j(Аь AJt Ап) /,ує N, 1 i,j n есть применение MP). (7) Л„ есть аксиома исчисления Н (допущение) (8) А„ есть Н-доказательство (из (7), по определению Н-доказательства) Очевидно, что (9) А„ есть последняя формула в Н-доказательстве А„. (10) Ап есть Н-доказуемая формула (из (9), по определению D/1.1.29) (11) Нн Ап (из (10), и того, что для всякой формулы A: f-H А = А есть Н-доказуемая формула (см. стр.15)) Очевидно, что (12) V А (Ьн А = \ moA). (13)кш. (из(11)и(12)) (14) М А (1-нюЛ = V v Ы I vMo= 1) (теорема 1.2.2) А есть формула v есть оценка языка ївМ0 (15) Л„ є For/w (из (3)) (16) НніоЛ = V v U I vM = 1(из (14) и (15)) v есть оценка языка ХвМ0 (17) V v \А „МО = 1 (из (13) и (16)) v есть оценка языка вМ0 (18) ULMo=l(H3(17)H(a)) Снимая допущение (7), получаем, что (19) Ап есть аксиома исчисления Н == \А „,м = 1. (20) Ап есть формула (р, Э (-i (р, D р,))) (допущение) (21) (р, Э (-п (р, Э р,))) LMo = и (р,) Э+ -+ (и (р.) Э+ iv (р,)) (из того, что (р, Э (-. (р, Э р,))), р„ (-. (р, D р,)), (pi Э рх) есть формулы, р, є Prop, и есть оценка языка X в М0, по определению значения формулы при заданной оценке X в Мо) (22) w (р,) Э+ -!+ (w (р,) D+ и (р,)) = 1 (из того, что w (р,) = f (по определению w ), по табличным определениям операций Э+ и -i+) Снимая допущение (20), получаем, что (23) А„ есть формула (р, Э (- (р, Э р,))) = LM = 1. (24) А„ есть формула ((-.р,) D (-, (р, Эр,))) (допущение) (25) ((-.p.) Э (-, (р, D р,))) I ,Мо = -+ (Рд D+ S (w (р.) Э+ и (р,)) (из того, что (р, Э (-. (р, Э р,))), р„ (-пр,), (-і (р, Э р,)), (р, Э р,) есть формулы, р, є Prop, w есть оценка языка X в Мо, по определению значения формулы при заданной оценке X в М0) (26) -i+ w (р,) Э+ -.+ (w (р,) Э+ w (р,)) = 1 (из того, что w (р,) = f (по определению w ), по табличным определениям операций Э+ и -i+) Снимая допущение (24), получаем, что (27) А„ есть формула ((-, р.) Э (-і (р, D р,))) = U WM = 1. (28) 3/3/ (Д, у, Л„) есть применение MP (допущение) ij є N, 1 i,j n Пусть (29) / ,/ є N, 1 Г,/ п, (At, Af, Ап) есть применение MP. (30) последовательность А\ ...у4. формул есть Н-вывод из множества {(р, D (-- (р, Э р,))), ((-л р,) D (-і (р, D /?,)))} формулы г (из (4), / є N, 1 г «, по лемме о начальном отрезке вывода) (31) последовательность Ai9...jAf формул есть Н-вывод из множества {(р, Э (-п (р, Э / ,))), ((-,/?,) D (-і (р, D р,)))} формулы 4- (из (4),/ є N, 1 f п, по лемме о начальном отрезке вывода) (32) I At и,м = 1 (из (30), по индуктивному допущению) (33) Af I WM= 1 (из (31), по индуктивному допущению) (34) формула Ау есть формула (At D Ап) (из того, что (At, Af, Ап) есть применение MP (см. (29)), по определению применения MP) (35) (At D Ая) LMo = 1 (из (33) и (34)) (36) І (Аґ D A„) wMo = \At H-MO D+ \A„\ WUO (из того, что (Ae D A„) есть формула, по определению значения формулы при заданной оценке X в Мо) (37) At I wMo D+\An\ WM = 1 (из (37) и (38)) (38) U„LMe {1, 0, f} (из (15) и (а), по лемме 1.2.1) (39) \An\w є {1, t} (из (32) и (37), по табличному определению операции Э+) Используя (40) и (41), получаем, что (42) ULMo=l Снимая допущение (30), получаем, что (43) 3/3/ (Ah Aj, Ап) есть применение MP = \А \ WM = 1. i,j є N, 1 i,j n (44) U LMO = 1 (из (6), (21), (25), (29) и (43)) Итак, в условиях доказываемой леммы верно, что (б). Лемма 1.2.8 доказана. Очевидна следующая лемма 1.2.9 Лемма 1.2.9 V lbtp.Dp,))}!-
Погружающие отображения, устанавливающие связь логик 1о и WP с классической пропозициональной логикой и логик AIP и IAP с интуиционистской пропозициональной логикой. Аналог теоремы В.И.Гливенко, устанавливающий связь логики 1о с логикой AIP и логики VVP с логикой IAP
Дано полное доказательство адекватности варианта семантики обобщённых описаний состояния, сформулированного в [49], простой паранормальной логике 1о из [49]; предложено использующее эту семантику доказательство того, что логическая матрица с четырёхэлементным носителем, построенная в [49], является характеристической матрицей логики 10; в 2.2 доказана теорема адекватности варианта семантики квазиописаний состояния простой паранормальной логике VVP из [32], а в 2.3 доказано, что никакая конечная логическая матрица не является характеристической матрицей для логики VVP. 2.1 Семантика обобщённых описаний состояния для логики 1о и четырёхзначная характеризация этой логики. Обобщённым описанием состояния (оос) называется отображение множества всех элементарных формул в {0, 1 } Понятие обощённого описания состояния введено Е.К.Войшвилло (см.,например, [13]). Здесь воспроизводится определение оос, данное в [49]. Можно доказать, что для каждого оос v существует единственное отображение v (называемое означиванием при v) множества всех формул в {0, 1}, удовлетворяющее условиям (а), (б), (в), (г) и (д): (a) Vp (\p\v = v(p) и lbp)v = v(bp))), р - проп. пер. (6)VA(\( A)\v=l \A\v = 0) Л-формула, которая не является проп. пер. (в) УА VB(\(A&B)\v=l = Mv= 1 и \B\V= 1), А, В- формулы (г) \/А VB{\(A V J?)v= 1 = Uv= 1 или \B\V= 1), А, В- формулы (д) \/А VB(\(АЭВ)\у=1о\А\у = 0 или \B\V = 1). А, В- формулы Лемма 2.1.1 VА (А есть аксиома исчисления HI0 = Vv \A\V= 1). V есть оос Доказательство Из того, что множество всех аксиом исчисления Н1о есть Ах 1 и Ах 2 и и Ах 3 и Ах 4 и Ах 5 и Ах 6 и Ах 7 и Ах 8 и Ах 9 и Ах 10 и Ах 1Г и и Ах 12 , вытекает, что для доказательства леммы 2.1.1 достаточно доказать следующие утверждения (а) - (л): (а) А, В и С есть формулы = Vv \((А D В) D ((В D С) D (A D Q))v = 1, V есть оос (б) А и В есть формулы = Vv \{А D {А V B))\v = 1, V есть оос (в) А и В есть формулы = Vv \{В D (А V ))v = 1, V есть оос (г)А,В и Сесть формулы= \((А D Q D ((В D С) D ((А V В) D Q))\v= V есть оос = 1, (д)АиВ есть формулы = Vv \{{А & В) D A)\v = 1, v есть оос (е) А и В есть формулы = Vv \((A & В) D B)\v = 1, v есть ooc (ё)Л,Я и С есть формулы= Уу ((С D A) D ((С D5)D(CD( 1& #))))v= V есть ooc = 1, (ж) А, В и С есть формулы = Vv ((Л D(5DC))D(( &5)DC))V = V есть оос = 1, (з) А, В и С есть формулы = Vv (((Л &5)DC)D( D(5DC)))V = v есть оос = 1, (и) А, В и С есть формулы = Vv (((Л D 5) Э Л) D Л)„ = 1, v есть оос (к) А есть формула и D есть формула не являющаяся пропозициональной переменной = Vv 1((-. D) D (D D AJ)\V = 1, v есть оос (л) А есть формула и D есть формула не являющаяся пропозициональной переменной = Vv \((D D (- (А D A))) D (-і D))\v = V есть оос = 1. Доказажем утверждение (а). (1) А, В и С есть формулы (допущение) (2) v есть оос (допущение) (3) \((А D В) D ((В Э С) D (A D C)))\v I (допущение) (4) {(A D В) Э ((В D Q D (A Э С))) v = О (из (3) и того, что значение всякой формулы при заданном оос принадлежит {0, 1}) (5) {A D В) „ = 1 и ((В D С) D (A D С)) „- = 0 (из (4),по определению значения формулы при заданном оос) (6) {{В Э С) D {A D Q) „ = 0 (из (5)) (7) I (В D С) I у- = 1 и {A D С) I у- = 0 (из (6), по определению значения формулы при заданном оос) (8) (ЛЭС), = 0(из(7)) (9) Л I,/ = 1 и СI = 0 (из (8), по определению значения формулы при заданном оос) (10) 04ЭЯ)„=1(из(5)) (11)(ЯЭО,= 1(из(7)) Используя (9) и (10), получаем, по определению значения формулы при заданном оос,что (12) В „=1. (13) С 1,/=1 (из (11) и (12), по определению значения формулы при заданном оос) (14) с, = 0(нз(9)) (15) с, 1(из(14)) Утверждение (15) противоречит утверждению (13). Следовательно, допущение (3) неверно. Но тогда (18) ((A D В) Э ((В D Q D (A D Q)) ,, = 1. Снимая допущение (2) и обобщая, получаем, что (19) V v ((A D В) D ((В D С) D (A D Q)) v= 1. V есть оос Снимая допущение (1), получаем, что (а). Утверждение (а) доказано. Аналогично доказываются утверждения (б) - (л). Лемма 2.1.1 доказана. Лемма 2.1.2 VA УВ Vv(Uv= 1 и \{А D 5)v= 1 = 5v= 1). А, В естьф-лы v есть оос Доказательство (\)А и В есть формулы (допущение) (2) V есть оос (допущение) (3) \A \V = 1 и \(А DB )\v.= l (допущение) (4)Иг =1(из(3)) (5) \B \V 1 (допущение) (6) \В \ = 0 (из (5) и того, что значение всякой формулы при заданном оос принадлежит {0, 1}) (7)04 ЭЯ%, = 1(из(3)) (8) \{А D B )\v = 0 (из (4) и (6), по определению значения формулы при заданном оос) (9)M DS )V. 1(H3(8)) Утверждение (9) противоречит утверждению (8). Следлвательно допущение (5) неверно. Но тогда (Ю)яг-=1. Снимая допущение (3), получаем, что (11) \A \V = 1 и \(А D ff)\v =\= B \V= 1. Снимая допущения (1), (2) и обобщая, получаем, что VA VB VV(MV=1H \(ADB)\V=\= 5V=1). А, В естьф-лы v есть оос Лемма 2.1.2 доказана. Теорема 2.1.1 (о непротиворечивости исчисления НІ0 относительно семантики обобщённых описаний состояния) VA УГ (Г ЫюА = Vv ((VB 5V=1)= UV=1)) А есть ф-ла Г есть множество формул v естьоос В є Г Доказательство (l)A есть формула (допущение) (2) Г есть множество формул (допущение) (З)Г \-шА (допущение) (4)Существует Н10-вывод из множества Г формулы А (из (3), по соглашению об обозначении) (5) 3 п 3 А\ ... 3 Ап последовательность At9 ... Ап есть Н10-вывод из п є N А\, ...,А„ є Form множества Г формулы Ап и А„ есть А (из (4), по определению Df 1.1.29) Пусть (6) п є N, А \, ..., А п є Form последовательность А \ 9...9 А п-есть HIo-вывод из Г формулы А а и А п- есть А . (7) А П є Г , или A rf есть аксиома исчисления Н10, или 3 к 3 / (Ак, Ai, А,) к, Is N, 1 k,l i есть применение MP (из (6), по определению ) (8) А п є Г (допущение) (9) v есть оос (допущение) (10) У В \B\V = \ (допущение) В є Г (11) \А п , = 1(ИЗ(8)И(10)) Снимая допущение (10), получаем, что (12) VB \B\V =1= А п 1,,= 1. В є Г Снимая допущение (9) и обобщая, получаем, что (13)Vv(V5 5v=l= I А п у=1). v есть оос В є Г Снимая допущение (8), получаем, что (14)i4 „ er= Vv(V ДУ=1= I А п- L = l). v есть оос В є Г 75 (15) А\ есть аксиома исчисления Н10 (допущение) (16) V есть оценка языка X в матрице М0 (допущение) (17) V В \B\V = 1 (допущение) Be г (18) V v (\А а I V = 1)) (из (15), по лемме 2.1.1) v есть оос (19) UV „=1 (ИЗ (16) И (18))(20) UV 1,= 1 (из (19)) Снимая допущение (17), получаем, что (21) V В #v.= l= А п V =1. В є Г Снимая допущение (16) и обобщая, получаем, что (22)Vv(V яу=1= А п. v=l). v есть оос В є Г Снимая допущение (15), получаем, что (23) А п- есть аксиома исчисления Н10 = V v (V 5 5v=l= M n-v=l. v есть оос В є Г (24) 3 к 3 I (Ак, А/, Ап) есть применение MP (допущение) kleN, \ k,l ri Пусть (25) к!, І є N, 1 А7, / гі и (А , А?, Ап) есть применение MP (26) формула Af есть формула {АК D Ап ) (из того, что {Ац, Af, Ап) єсть применение MP (см. (25)), по определению применения MP) (27)Vv(V Uv=l= \A K I v= 1) (из того, что к! ri (см. 25)), v есть оос В є Г по индуктивному допущению) (28)Vv(V5 яу=1) = (ЛОЛОи=1)(изтого,что/ и v есть оос В є Г (см. (25)) и (26), по индуктивному допущению) (29) Vv ((V В В v = 1) = \Ап. V = 1) (из (27) и (28), по лемме 2.1.2) v есть оос В є Г Снимая допущение (24), получаем, что (30) 3 к 3 I (Ак, А,, Ап) есть применение MP = Vv ((V В \ В \ v = 1) = к, І є N,1 к, 1 п v есть оценка языка в матрице М0 В є Г = UJV=1). (31)Vv(VSi8v=l= v=l)(H3(7),(14),(23)H(30)) v есть оос ВєГ
Семантика квазиописаний состояния для логики WP
Квазиописанием состояния (кос) называется отображение множества всех квазиэлементарных формул в {О, I}. Можно доказать, что для каждого кос v существует единственное отображение v (называемое означиванием при v) множества всех формул в {0, 1}, удовлетворяющее условиям (а), (б), (в), (г) и (д): Доказательство леммы 2.2.1 аналогично приведённому выше (см. 2.1) доказательству леммы 2.1.1 Лемма 2.2.2 \/А УВ VV(MV=1H( D5)V=1= \B\v=l). А, В- ф-лы v есть кос Доказательство леммы 2.2.2 аналогично приведённому выше (см. 2.2) доказательству леммы 2.1.2 Теорема 2.2.1 VA УГ (Г I-HVVP = Vv((V \B\V=\)= \A\V=\)) А есть ф-ла Г есть мн-во формул v естькос ВеГ Доказательство теоремы 2.2.1 аналогично приведённому выше (см. 1.1) доказательству теоремы 2.1.1. Вместо лемм 2.1.1 и 2.1.2 используются соответственно лемма 2.2.1 и лемма 2.2.2. Определение Df 2.2.1: HVVP-перенасыщенным множеством формул называем любое такое множество Г формул, что \/А (Г І-HVVP А) А есть формула Очевидна следующая лемма 2.2.3 Лемма 2.2.3 Г есть HVVP-перенасыщенное множество формул о Г f-Hvvp (- (Р\ Э Эр.)) Лемма 2.2.4 \/А \/Г (Г ffiivvp = ЗД (Д есть насыщенное множество А есть ф-ла Г есть мн-во ф-л формул, и Д не есть HVVP-перенасыщенное множество формул, и Ги{04Э(-п(р.ЭА)))} =Д). Доказательство леммы 2.2.4 аналогично доказательству леммы 2.1.4. При этом используется лемма 2.2.3 вместо леммы 2.1.3. Лемма 2.2.5 Пусть Е есть насыщенное множество формул, но не HWP-перенасыщенное множество формул. Тогда существует такое кос а, что для всякой формулы А верно следующее: A el« U«=l. Доказательство леммы 2.2.5 аналогично доказательству леммы 2.1.5. Теорема 2.2.2 (о полноте исчисления HVVP относительно семантики квазиописаний состояния) УА VT (Vv((V ЯУ=1)= И„=1)= Г I-HVVP4) А есть ф-ла Г есть мн-во ф-л v есть кос В є Г Доказательство теоремы 2.2.2 аналогично доказательству теоремы 2.1.2. При этом используется лемма 2.2.5 вместо леммы 2.1.5. Теорема 2.2.3 (об адекватности исчисления HVVP семантике квазиописаний состояния) УА VT (Г І-HVVP А = Vv ((V \B\V= 1) = \A\V= 1)) А есть ф-ла Г есть мн-во ф-л v естькос В є Г Очевидно, что теорема 2.2.3 вытекает из теорем 2.2.2 и 2.2.1. Следующая теорема 2.2.4 является очевидным следствием теоремы 2.2.3. Теорема 2.2.4 V A (I-HVVP = Vv \A\v=l) А есть ф-ла v есть кос Следствием теоремы 2.2.4 и того, что VVP = {A I I-HVVP А}, является следующая теорема 2.2.5. Теорема 2.2.5 (об адекватности логики VVP семантике квазиописаний состояния) VA ( eWP о Vv Uv=l) А есть ф-ла v естькос 2.3 Несуществование конечной характеристической матрицы для логики VVP. Следуя [32], (а) условимся, что для всякого целого неотрицательного числа к и всякой пропозициональной переменной/? I р, если к = О, {( ( к-1)р)),есшк 0, и (б) определим квазиэлементарную формулу как -i(k)p, где к есть целое неотрицательное число ир есть пропозициональная переменная. Ясно, что данное определение квазиэлементарной формулы эквивалентно определению Df 1.1.1, данному в Главе 1. Лемма 2.3.1 Пусть К есть и-элементное («-целое положительное число) множество, / есть отображение множества К в себя, есть операция композиции отображений множества К в себя, и для всякого целого неотрицательного числа/ \ f, если / = О, 1/ / "",если/ 0. Тогда 3k 3/:/(к)=/(0 к, I есть целые неотрицательные числа, к Ф I Доказательство Очевидно, что VA::/(k) есть отображение множества К в себя. к есть целое неотрицательное число Отсюда получаем, что множество {/\/х\/2\ ...} является подмножеством множества всех отображений множества К в себя. Но множество всех отображений множества К в себя конечно, т.к. К есть конечное множество (известно, что число всех отображений конечного множества в себя равно тт, где m-число элементов данного конечного множества). Поэтому множество {f\ /1\ /2\ ...} конечно. Значит, f\ fl\ f2\ ... не являются попарно различными отображениями. Но тогда существуют такие целые неотрицательные числа к и /, что к Ф I и/(1с) =/(/). Лемма 2.3.1 доказана. Лемма 2.3.2 Если некоторая матрица, носитель которой есть «-элементное (п есть целое положительное число) множество, является характеристической матрицей для VVP, то существуют такие целые неотрицательные числа к и /, что кФІи формула ( -i(k)pi Р\) принадлежит множеству WP. Доказательство (1) существует матрица, носитель которой есть «-элементное (п есть целое неотрицательное число) множество, являющаяся характеристической матрицей для VVP (допущение) Пусть (2) 771 есть матрица, носитель которой есть и-элементное (и-целое положительное число) множество, являющаяся характеристической матрицей для WP. Не ограничивая общности рассуждений, положим: (3) 771 = (М, N, {& , V, Э , -, } , & , V, Э есть бинарные, а -, есть унарная операции на М. Оценка языка X в 771 определяется стандартно (как отображение множества всех пропозициональных переменных в М), обычным образом определяется (индукцией по построению формулы) значение формулы в 771 при заданной оценке языка X в 771 (значение формулы F в 771 при оценке v языка в 171 обозначаем через \F\vm): (і) \p\vm = v(p) для всякой пропозициональной переменной/?, (ii) \(A & B)\vm = \A\v & \B\ для всяких формул А и В, (Ш) \{А V )vm = \A\V V vm для всяких формул А и В, (iv) (Л Э B)\vm = \A\vm D \B\ для всяких формул А и В, (у) (-i Л)„т = -i 4vm для всякой формулы А. Покажем теперь, что (4) Vx: х Э х є N х є М Пусть а є М и va есть оценка языка С в 771 такая, что va(p ) = а для всякой пропозициональной переменной р. Тогда \{р\ D p\)\vam = piLm Э \P\\vam - va(P\) Э va(pi) = a D а. Но для всякой оценки v языка в 771 \(р] D pi)\vm є N (из (2), (3) и того, что формула (р\ Э р\) доказуема в HVVP). Поэтому а Э а є N. Отсюда, поскольку а есть произвольный элемент множества М, получаем, что Vx: х D х є N. хєМ В силу теоремы 2.2.3 для доказательства леммы 2.3.3 достаточно доказать, что () для всяких неотрицательных чисел киї таких, что к Ф I, существует кос а такое, что (-i(k)/?i — (/)/?і)а 1 Пусть ко и /0 есть произвольные целые неотрицательные числа такие, что #о А)- Пусть ао есть {(е, 0) е есть квазиэлементарная формула и е Ф -i(ko)/ i} U { -i(ko)/?i, 1)}. Ясно, что ао есть кос такое, что -і(ко)/?іІао = 1 и - (/Vilao = 0- Очевидно, что (-i(ko)/?i Э -і(/о)р\)\ф Ф 1. Итак, существует кос а такое, что (-, (ko) рх D —і (/о) р\)\а Ф 1. Но тогда, поскольку ко и /о есть произвольные целые неотрицательные числа такие, что ко Ф /о, получаем, что для всяких целых неотрицательных чисел к и / таких, что к Ф I, существует кос а такое, что (-i(k)/?i -1 Р\)\а 1-Утверждение () доказано. Лемма 2.3.3 доказана. Следствием леммы 2.3.2 и леммы 2.3.3 является следующая теорема 2.3.1. Теорема 2.3.1 Не существует конечной характеристической матрицы для логики VVP. Краткое изложение главы 3: в 3.1 вводится, следуя [33], понятие АІР-модели, являющегося обобщением понятия модели Крипке для интуиционистской пропозициональной логики, и предлагается полное доказательство адекватности семантики, основанной на понятии АІР-модели, логике АІР; в 3.2 определяется ещё одно обобщение понятия модели Крипке для интуиционистской пропозициональной логики - понятие ІАР-модели, и предлагается доказательство адекватности семантики, основанной на понятии ІАР-модели логике ІАР; в 3.3 констатируется факт несуществования конечной характеристической матрицы как для логики АІР, так и для логики ІАР. Следуя [33], АЇР-моделью называем упорядоченную тройку (G, R, 1=) такую, что G есть непустое множество, R есть рефлексивное и транзитивное бинарное отношение на G, 1= есть подмножество множества G X Form, и выполняются следующие условия: (1) для всякой элементарной формулы е и всяких ос и р из G, верно, что если а 1= е и а R (3, то р 1= е, (2) для всяких формул А и В, всякой формулы С, не являющейся пропозициональной переменной, и всякого а из G верно, что (2.1) а 1= (А & В) = а \= А и а 1= В, (2.2) а N= (А V В) о а 1= А или а 1= В, (2.3) а t= {A D В) о V р (Р N А = р 1= В), aRP (2.4) а t= (-, Q О V Р (р Ф Q. aRp Для всякой АІР-модели называем носителем этой АІР-модели её первый член (всякая AIP-модель есть упорядоченная тройка), называем отношением достижимости в этой АІР-модели её второй член и называем отношением вынуждения в этой АІР-модели её третий член. Вспомним, что в [45] модель Крипке для интуиционистской логики высказываний Int определяется как такая упорядоченная тройка (G, R, 1= , что G есть непустое множество, R есть рефлексивное и транзитивное
Семантика в стиле С.Крипке для логики IAP
Опираясь на это утверяедение, нетрудно доказать, что всякая модель Крипке для Int является IAP-моделью. С другой стороны, очевидно, что не всякая IAP-модель является моделью Крипке для Int \ Таким образом, понятие ІАР-модели является обобщением понятия модели Крипке для Int;. Соглашение об обозначении: для всякой ІАР-модели ffll условимся обозначать через G носитель ІАР-модели Ш, через R , - отношение достижимости в ІАР-модели Ш, а через 1= , - отношение вынуждения в ІАР-модели 9Ю. Определение Df 3.2.1 А называем формулой общезначимой в ІАР-модели Ш, если V a: a )= А. aGw Определение Df 3.2.2 Из Г следует в логике IAP А(из Г IAP-следует А, или А ІАР-следует из Г), если Г есть множество формул, А есть формула и для всякой ІАР-модели Ш1 V a ((V5 a t=m В) = a \=т А). а є Gw В є Г Определение Df 3.2.3 А называем ІАР-общезначимой формулой, если V SH А есть формула общезначимая в ІАР-модели Ш. 9W есть ІАР -модель Определение Df 3.2.4 НІАР-дизъюнктным множеством называем такое множество Г формул, что V В V С (Г I-HIAP (В V С) = Г г-НІАР В или В, С є Form г ьШАР Q Определение Df 3.2.5 HIAP-нетривиализуемым множеством называем такое множество Г формул, что ЗАТ У-ШАР А. А є Form Лемма 3.2.1 Л есть IAP-общезначимая формула = Л ІАР-следует из 0. Доказательство леммы 3.2.1 аналогично доказательству леммы 3.1.1. Здесь, конечно, модели Крипке для Int понимаются в смысле данного выше определения. Здесь, конечно, модели Крипке для Int понимаются в смысле данного выше определения. Лемма 3.2.2 Пусть (G, R, И) есть ІАР-модель, а, 3 є G, А есть формула. Тогда at=AnaRfi= fii=A. Доказательство леммы 3.2.2 аналогично доказательству леммы 3.1.2 Лемма 3.2.3 Всякая аксиома исчисления HIAP является 1АР-общезначимой формулой. Доказательство леммы 3.2.3 аналогично доказательству леммы 3.1.3 и опирается на лемму 3.2.2. Лемма 3.2.4 Если п є N, А\, ..., А„ есть формулы и последовательность А) 9...9 Ап формул есть HIAP-вывод из множества М, то из М IAP-следует А„. Доказательство леммы 3.2.4 аналогично доказательству леммы 3.1.4. Теорема 3.2.1 М ЬНІАР А = из М ІАР-следует А. Следует из леммы 3.2.4. Теорема 3.2.2 ЬніАР А= А есть 1АР-общезначимая формула. Следует из теоремы 3.2.1 и леммы 3.2.1. Используя теорему 3.2.2 и определение логики ІАР получаем, что имеет место следующая теорема 3.2.3. Теорема 3.2.3 А є ІАР = А есть IAP-общезначимая формула. Лемма 3.2.5 Если М есть множество формул, А есть формула и М If НІАР А, то существует множество М формул такое, что а) М с М , b) М If НІАР А, с) М есть HIAP-дизъюнктное множество. Доказательство леммы 3.2.5 аналогично доказательству леммы 3.1.5. Лемма 3.2.6 М есть множество формул, А есть формула и М If НІАР А = = З Ш 3 a ((V В a \=т В) и a frm А). 9И есть AIP-модель a е GM В є М Доказательство леммы 3.2.6 аналогично доказательству леммы З.І.б.При этом вместо леммы 3.1.5 используется лемма 3.2.5 и определения D/32A и Df 3.2.5 используются вместо определений Df 3.1.4 и Df3A.5 соответственно. Теорема 3.2.4 Из М ІАР-следует Л = М (-ШАРЛ. Доказательство теоремы 3.2.4 аналогично доказательству теоремы 3.1.4, при этом опирается на лемму 3.2.6. Теорема 3.2.5 А есть IAP-общезначимая формула = Н-ШАР А. Следует из теоремы 3.2.4 и леммы 3.2.1. Используя теорему 3.2.5 и определение логики ІАР, получаем, что имеет место следующая теорема 3.2.6 Теорема 3.2.6 А есть ІАР-общезначимая формула = І4Є ІАР. Из теоремы 3.2.1 и теоремы 3.2.4 вытекает следующая теорема 3.2.7 Теорема 3.2.7 М І-НІАР А = Из М IAP-следует А. Из теоремы 3.2.2 и теоремы 3.2.5 вытекает следующая теорема 3.2.8. Теорема 3.2.8 ЬНІАР Л = А есть ІАР-общезначимая формула. Из теоремы 3.2.3 и теоремы 3.2.6 вытекает следующая теорема 3.2.9 Теорема 3.2.9 А є ІАР = А есть ІАР-общезначимая формула. Теперь мы готовы выполнить данное на стр. 15 обещание - доказать, что множества Io, VVP, АІР, и ІАР попарно различны. Докажем, что (a) Io VVP. Доказательство (1) Формула ((-. (-. /?,)) Э ((- /?,) Э ( -і О?, Э /?,)))) принадлежит множеству всех аксиом исчисления Н1о (по определению множества всех аксиом исчисления Н1о) (2) Формула ((-, (-і /?,)) Э ((-, /?,) Э ( -, (р, Э /?,)))) есть Н1о-доказательство (из (1), по определению Н1о-доказательства) (3) ((-1 (-1 Рд) ((-1 /?i) 3(—i (р, Z Pi)))) есть НІо-доказуемая формула (из (2), по определению Шо-доказуемой формулы) (4) Ьню ((-- (-./?,)) Э ((-. ,) D (-,(/?, D /?,)))) (из (3) и утверждения (#), сформулированного на стр. 14) (5) ((-. (-і /?,)) D ((-і р,) D ( -і (р, D р,)))) є Io (из (4), по определению множества Io) Обозначим посредством v квазиописание состояния такое, что v (q) = 1 для всякой квазиэлементарной формулы q. Ясно, что (6) ((-, (-.р,)) D ((-,/ ,) D ( -, (р, D р,)))) I v = 0. (7) Неверно, что Vv \А v = 1 (из (6)) v естькос (8) ((-п (-,р,)) = ((-Р.) ( -, (р, Э р,)))) VVP (из (7), того, что ((-і (-/?0) Э ((-i/?i) Э (-і (р. Эр,)))) есть формула, по теореме 2.2.5) Из (5) и (8) следует утверждение (а). Утверждение (а) доказано. Докажем, что (б) AIP IAP. Доказательство (1) Формула ((-і (-і р,)) Э ((-, р,) Э ( - (р, Э р,)))) принадлежит множеству всех аксиом исчисления HAIP (по определению множества всех аксиом исчисления HAIP) (2) Формула ((-, (-, р,)) = ((і р,) Э ( -, (р, Э р,)))) есть HAIP-доказательство (из (1), по определению НАІР-доказательства) (3) ((-і (—і/?,)) Э ((-іpi) Э ( -і (p, Э pi)))) єсть НАІР-доказуемая формула (из (2), по определению HAIP-доказуемой формулы) (4) Нню ((-. (-.р,)) D ((-.р.) D ( -, (р, Эр,)))) (из (3) и утверждения (#), сформулированного на стр. 14) (5) ((-. (-і р,)) Э ((-. р.) Э ( -, (р, Э р,)))) є AIP (из (4), по определению множества AIP) Можно доказать, что (6) IAP-моделью является упорядоченная тройка ({0}, R, (= , где R есть {(0, 0)}, 1= есть подмножество множества {0} X Form, выполняющее следующие условия: (і) для всякой квазиэлементарной формулы q верно, что 0 \= q , (іі) для всяких формул А и В, всякой формулы С, не являющейся квазиэлементарной формулой, верно, что (іі.1) 0\=(А&В)о0ї=Аи0\=В, (іі.2) 0 1= (А V В) О 0 N А или 0 N 5, (іі.З) 01=(4эЯ)о01=Л= 01=Я, (іі.4) 0 1= (-, Q = 0 fefc С. Ясно, что (7) 0 Ф ((-п Ьр,)) Э (Ьр.) Э ( -і (р, Э р,)))). (8) Неверно, что ((-і (-, р,)) Э ((-, р,) Э ( -, (р, Э р,)))) есть IAP-общезначимая формула (из (7), по определению 1АР-общезначимой формулы) (9) ((-і (-/ .)) Э (Ьр.) Э ( -п (р, Эр,)))) IAP (из (8), того, что ((-1 С-1/ !)) D (С-1/7!) Э ( -і (р, D р,)))) есть формула, по теореме 3.2.9) Из (5) и (9) следует утверждение (б). Утверждение (б) доказано. Докажем, что (в) AIP Ф VVP.
