20 марта 2016г.
Предлагаемая Вашему вниманию работа относится к исследованиям паралогик, то есть к исследованиям таких логик, которые являются паранепротиворечивыми или/и параполными логиками (термины «паранепротиворечивая логика» и «параполная логика» используем в смысле работы [1]). Здесь построена двузначная семантика определяемого ниже пропозиционального языка L, адекватная одной из активно изучаемых паралогик – логике PComp. Эта паралогика является параполной, но не паранепротиворечивой логикой. Сконструированная семантика логики PComp оперирует простыми и интуитивно прозрачными семантическими понятиями, а вычисление значений формул в данной семантике не вызывает затруднений.
Язык L есть стандартный пропозициональный язык, алфавиту которого принадлежат все следующие символы и только они: &, Ú, É (бинарные логические связки языка L), Ø (унарная логическая связка языка L), ) и ( (технические символы языка L), p1, p2, p3,… (пропозициональные переменные языка L). Определение L- формулы индуктивно: (1) всякая пропозициональная переменная есть L-формула, (2) если A и B являются L- формулами, то (A&B), (AÚB), (AÉB) и (ØA) являются L-формулами, (3) ничто другое L-формулой не является. Логикой называем непустое множество L-формул, замкнутое относительно правила подстановки в L и правила модус поненс в L. Следуя [1], определим исчисление HPComp гильбертовского типа, которое аксиоматизирует логику PComp. Язык исчисления HPComp есть L. Множество всех аксиом этого исчисления есть множество всех тех и только тех L-формул, каждая из которых имеет хотя бы один из следующих девятнадцати видов (здесь A, B и C – L-формулы):
Исчисление HPComp имеет единственное правило вывода – правило модус поненс в L. Вспомним, что правило модус поненс в L – это множество всех упорядоченных троек вида , где A и B – L- формулы, а применение правила модус поненс в L – это элемент данного правила. Определение 1: α называем HPComp-выводом длины n (n – целое положительное число) из множества Γ L-формул L-формулы A, если существуют такие L-формулы A1,…, An, что α есть n-членная последовательность L-формул, первый член которой есть A1,…, n-ный член которой есть An , An есть A, и для всякого целого положительного числа i, которое меньше или равно n, выполняется следующее условие: Ai принадлежит множеству Γ, или Ai есть аксиома исчисления HPComp, или существуют такие целые положительные числа k и l, которые строго меньше i, что есть применение правила модус поненс в L. Определение 2: α является HPComp-выводом из множества Γ L-формул L-формулы A, если существует такое целое положительное число n, что α есть HPComp-вывод длины n из множества Γ L-формул L-формулы A.Определение 3: L-формула A HPComp-выводима из множества Γ L- формул, если существует HPComp-вывод из множества Γ L-формул L-формулы A. Определение 4: L-формула A HPComp-доказуема, если существует HPComp-вывод из пустого множества L-формул L-формулы A. Определяем PComp как множество всех HPComp-доказуемых L-формул. Можно доказать, что PComp является логикой.
Элементарной L-формулой называем L-формулу, которая является пропозициональной переменной языка L или имеет вид (Øq), где q есть пропозициональная переменная языка L. Называем PComp-оценкой такое отображение v множества всех элементарных L-формул во множество {0,1}, что для всякой пропозициональной переменной p языка L верно следующее: если v(p)=1, то v((Øp))=0. Называем PComp-означиванием при PComp- оценке v такое отображение f множества всех L-формул во множество {0,1}, что для всякой пропозициональной переменной q языка L и всяких L-формул A и B выполняются условия:
(1) f(q)= v(q), (2) f((Øq))= v((Øq)),
Можно доказать, что для всякой PComp-оценки существует единственное PComp-означивание при этой PComp-оценке. PComp-означивание при PComp-оценке v обозначаем через φv.
Определение 5: PComp-общезначимой L-формулой является такая L формула A, что для всякой PComp-
оценки v φv(A)=1.
Определение 6: L-формула A PComp-следует из множества Γ L-формул, если для всякой PComp-оценки v верно следующее: если для всякой L-формулы B из Γ φv(B)=1, то φv(A)=1.
Лемма 0.
Для всякой L-формулы A и для всякой PComp-оценки v: если φv(A)=1, то φv((ØA))=0.
В свете принимаемого здесь традиционного определения длины L-формулы A как числа всех вхождений логических связок &, Ú, É, Ø языка L в A ясно, что лемма 0 вытекает из следующего утверждения 1. Утверждение 1: для всякого целого неотрицательного числа n, для всякой L-формулы A длины n и для всякой PComp-оценки v: если φv(A)=1, то φv((ØA))=0. Доказательство утверждения 1 возвратной индукцией по длине L-формулы стандартно.
Лемма 1.
Всякая аксиома исчисления HPComp является PComp-общезначимой L-формулой.
Доказательство леммы 1 сводится к рутинной проверке того, что если L-формула имеет хотя бы один из указанных выше девятнадцати видов (I) – (XIX), то она является PComp-общезначимой L-формулой. При этом проверка того, что если L-формула имеет вид (XIX), то она является PComp-общезначимой L-формулой, легко осуществляется с использованием леммы 0.
В свете леммы 1 и определений 5 и 6 очевидна следующая лемма 2.
Лемма 2.
Для всякого множества Γ L-формул и для всякой аксиомы A исчисления HPComp верно, что A PComp- следует из Γ.
Доказательство нижеследующей леммы 3 легко провести методом от противного, используя определение PComp-означивания и определение 6.
Лемма 3.
Для всякого множества Γ L-формул и для всяких L-формул A и B:если A PComp-следует из Γ и (AÉB) PComp-следует из Γ, то B PComp-следует из Γ.
Лемма 4.
Для всякого множества Γ L-формул, для всякого целого положительного числа n и для всяких L-формул A1,…, An : если для всякого целого положительного числа i, которое меньше или равно n, верно, что Ai принадлежит множеству Γ , или Ai есть аксиома исчисления HPComp, или существуют строго меньшие i целые положительные числа k и l, для которых упорядоченная тройка есть применение правила модус поненс в L, то An PComp-следует из Γ.
Простое доказательство леммы 4 можно провести методом возвратной индукции, опираясь на леммы 2 и 3. Опираясь на лемму 4 и определения 1, 2 и 3, легко доказать следующую теорему 1.
Теорема 1.
Для всякого множества Γ L-формул и для всякой L-формулы A: если A HPComp-выводима из Γ , то A
PComp-следует из Γ.
Теперь нам потребуется еще одно определение. PComp-оценочным множеством называем множество Γ L- формул, удовлетворяющее следующим условиям:
(1) для всякой пропозициональной переменной p языка L верно, что если p принадлежит множеству Γ, то (Øp) не принадлежит множеству Γ,
(2) для всяких L-формул A и B: (A&B) принадлежит множеству Γ тогда и только тогда, когда A принадлежит множеству Γ и B принадлежит множеству Γ,
(3) для всяких L-формул A и B: (AÚB) принадлежит множеству Γ тогда и только тогда, когда A принадлежит множеству Γ или B принадлежит множеству Γ,
(4) для всяких L-формул A и B: (AÉB) принадлежит множеству Γ тогда и только тогда, когда A не принадлежит множеству Γ или B принадлежит множеству Γ,
(5) для всяких L-формул A и B: (Ø(A&B)) принадлежит множеству Γ тогда и только тогда, когда (ØA) принадлежит множеству Γ или (ØB) принадлежит множеству Γ,
(6) для всяких L-формул A и B: (Ø(AÚB)) принадлежит множеству Γ тогда и только тогда, когда (ØA) принадлежит множеству Γ и (ØB) принадлежит множеству Γ,
(7) для всяких L-формул A и B: (Ø(AÉB)) принадлежит множеству Γ тогда и только тогда, когда A
принадлежит множеству Γ и (ØB) принадлежит множеству Γ,
(8) для всякой L-формулы A: (Ø(ØA)) принадлежит множеству Γ тогда и только тогда, когда A
принадлежит множеству Γ. Лемма 5.
Для всякого множества Γ L-формул и для всякой L-формулы A: если неверно, что A HPComp-выводима из Γ, то существует такое PComp-оценочное множество Δ, что Γ включается в Δ и при этом неверно, что A HPComp- выводима из Δ.
Доказательство леммы 5 начинаем с допущения, что K есть множество L-формул и F есть L-формула, удовлетворяющие условию:
неверно, что F HPComp-выводима из K. Затем, используя лемму Цорна,
показываем, что во множестве {Σ|Σ есть множество L-формул, K включается в Σ и неверно, что F HPComp-выводима из Σ}, упорядоченном отношением теоретико-множественного включения, имеется максимальный элемент.
Далее, зафиксировав произвольный максимальный элемент M указанного множества, показываем, что M является PComp-оценочным множеством, выполняющим условие: неверно, что F HPComp-выводима из M. Отсюда, учитывая, что K включается в M, заключаем, что существует такое PComp-оценочное множество Δ, что K включается в Δ и неверно, что F HPComp-выводима из Δ. Доказательство леммы 5 завершаем снятием первоначального допущения и соответствующим обобщением.
Лемма 6.
Для всякого PComp -оценочного множества Γ существует такая PComp-оценка v, что для всякой L- формулы A верно следующее: φv(A)=1 тогда и только тогда, когда A принадлежит множеству Γ.
Доказательство леммы 6 начинаем с допущения к рассмотрению произвольного PComp-оценочное
множества K и Par-оценки w, являющейся множеством всех упорядоченных пар , выполняющих следующие три условия: (1) x есть элементарная L-формула, (2) если x принадлежит множеству K, то y=1, (3) если x не принадлежит множеству K, то y=0. Затем, возвратной индукцией по длине L-формулы доказываем утверждение 2, гласящее, что для всякого целого неотрицательного числа n и для всякой L-формулы A длины n: φw(A)=1 тогда и только тогда, когда A принадлежит множеству K. Опираясь на утверждение 2 приходим к выводу, для всякой L- формулы A: φw(A)=1 тогда и только тогда, когда A принадлежит множеству K. Используя этот вывод и тот факт, что w есть PComp-оценка, получаем, что существует такая PComp-оценка v, что для всякой L-формулы A: φv(A)=1 тогда и только тогда A принадлежит множеству K. Доказательство леммы 6 завершаем снятием первоначального допущения и соответствующим обобщением.
Теорема 2.
Для всякого множества Γ и для всякой L-формулы A: если A PComp-следует из Γ, то A H PComp-выводима из Γ.
Докажем теорему 2.
(1) K есть множество L-формул (допущение).
(2) F есть L-формула (допущение).
(3) F Par-следует из K (допущение).
(4) Неверно, что F HPComp-выводима из K (допущение).
(5) Существует такое PComp-оценочное множество Δ, что K включается в Δ и неверно, что F HPComp- выводима из Δ (из (1), (2) и (4), по лемме 5).
Пусть (6) Δ0 есть PComp-оценочное множество, K включается в Δ0 и неверно, что F HPComp-выводима из Δ0.
(7) Δ0 есть PComp-оценочное множество (из (6)).
(8) Существует такая PComp-оценка v, что для всякой L-формулы A верно следующее: φv(A)=1 тогда и только тогда, когда A принадлежит множеству Δ0 (из (7), по лемме 6).
Пусть (9) w есть PComp-оценка и для всякой L-формулы A верно следующее: φw(A)=1 тогда и только тогда, когда A принадлежит множеству Δ0.
(10) K включается в Δ0 (из (6)).
(11) Для всякой A из K верно, что φw(A)=1 (из (9) и (10)).
Ясно, что (12) для всякого множества L-формул Γ и для всякой формулы A из Γ верно, что A HPComp- выводима из Γ.
(13) Неверно, что F HPComp-выводима из Δ0 (из (6)).
(14) Δ0 есть множество L-формул (из (7), по определению PComp-оценочного множества).
(15) F не принадлежит множеству Δ0 (из (2), (12), (13) и (14)).
(16) Для всякой L-формулы A верно следующее: φw(A)=1 тогда и только тогда, когда A принадлежит множеству Δ0 (из (9)).
(17) Неверно, что φw(F)=1 (из (2), (15) и (16)).
(18) Для всякой PComp-оценки v верно следующее: если для всякой L-формулы B из K φv(B)=1, то φv(A)=1 (из (3), по определению 6).
(19) w есть PComp-оценка (из (9)).
(20) Если для всякой L-формулы B из K φw(B)=1, то φw(A)=1 (из (18) и (19)). (21) φw(F)=1 (из (11) и (20)).
Утверждение (21) противоречит утверждению (17). Следовательно, неверно допущение (4). Итак, (22) F HPComp-выводима из K. Завершаем доказательство теоремы 2, снимая допущения (1), (2) и (3) и обобщая.
Из теорем 1 и 2 вытекает следующая теорема 3.
Теорема 3.
Для всякого множества Γ L-формул и для всякой L-формулы A:
A HPComp-выводима из Γ тогда и только тогда, когда A PComp-следует из Γ.
Учитывая, что множество всех PComp-общезначимых L-формул равно множеству всех L-формул, PComp- следующих из пустого множества, и опираясь на теорему 3 и определения, получаем, что верна следующая теорема 4.
Теорема 4.
Для всякой L-формулы A: A HPComp-доказуема тогда и только тогда, когда A PComp-общезначима.
Из теоремы 4 и того, что PComp есть логика, равная множеству всех HPComp-доказуемых L-формул, вытекает следующая теорема 5 о семантической характеризации (в терминах построенной двузначной семантики) логики PComp.
Теорема 5.
Для всякой L-формулы A: A принадлежит логике PComp тогда и только тогда, когда A PComp- общезначима.
Работа выполнена при поддержке РФФИ № 13-06-00147а.
Список литературы
1. Попов В.М. Между Par и множеством всех формул//Шестые Смирновские чтения по логике: материалы Междунар. Науч.конф., Москва, 17-19 июня 2009 г. – М.: Современные тетради, 2009. С. 93-95.
