Двузначная семантика логики PCont

Тип работы:
Реферат
Предмет:
Физико-математические науки


Узнать стоимость

Детальная информация о работе

Выдержка из работы

Попов В.М. (c)
К. филос. н., доцент кафедры логики философского факультета, Московского государственного университета им. М.В. Ломоносова
ДВУЗНАЧНАЯ СЕМАНТИКА ЛОГИКИ PCONT*
Аннотация
Здесь построена двузначная семантика определяемого ниже пропозиционального языка L, адекватная одной из наиболее активно изучаемых паралогик — логике PCont из [2]. Сконструированная семантика оперирует простыми и интуитивно прозрачными семантическими понятиями, а вычисление значений формул в данной семантике не вызывает затруднений.
Ключевые слова: элементарная формула, PCont-оценка, PCont -означивание при заданной PCont-оценке, PCont-оценочное множество.
Keywords: elementary formula, PCont-valuation, PCont-denotation under the given PCont-valuation, PCont-valuation set.
Предлагаемая Вашему вниманию работа относится к исследованиям паралогик, то есть к исследованиям таких логик, которые являются паранепротиворечивыми или/и параполными логиками (термины «паранепротиворечивая логика» и «параполная логика» используются здесь в смысле работы [1]). Центральный персонаж работы -паранепротиворечивая, но не параполная, логика PCont из [2], которая наделяется двузначной семантикой.
Язык L есть стандартный пропозициональный язык, алфавиту которого принадлежат все следующие символы и только они: & amp-, V, з (бинарные логические связки языка L), 0 (унарная логическая связка языка L)) и ((технические символы языка L), p1, р2, р3,… (пропозициональные переменные языка L). Определение L-формулы индуктивно: (1) всякая пропозициональная переменная есть L-формула, (2) если A и B являются L-формулами, то (A& amp-B), (AvB), (АзВ) и (0A) являются L-формулами, (3) ничто другое L-формулой не является. Логикой называем непустое множество L-формул, замкнутое относительно правила подстановки в L и правила модус поненс в L. Следуя духу, но не букве, работы [2], определим исчисление HPCont гильбертовского типа, которое аксиоматизирует интересующую нас логику PCont (в [2] «PCont» используется для обозначения исчисления, но не логики, а в рамках предлагаемой статьи целесообразно различать исчисление HPCont и аксиоматизируемую им логику PCont). Язык исчисления HPCont есть L. Множество всех аксиом этого исчисления есть, множество всех тех и только тех L-формул, каждая из которых имеет хотя бы один из следующих девятнадцати видов (здесь A, В и C — L-формулы):
(I) ((A3B)3((B3C)3(A3C))), (II) (A3(AvB)), (III) (A3(BvA)), (IV)
((A3C)3((B3C)3((AvB)3C))), (V) ((A& amp-B)3A), (VI) ((A& amp-B)3B), (VII)
((C3A)3((C3B)3(C3(A& amp-B)))), (VIII) ((A3(B3C))3((A& amp-B)3C)), (IX)
(((A& amp-B)3C)3(A3(B3C))), (X) (((A3B)3A)3A), (XI) (KAvB))3((0A)& amp-(0B))), (XII) (((0A)& amp-(0B))3(0(AvB))), (XIII) ((0(A& amp-B))3((0A)v (0B))), (XIV) (((0A)v (0B))3(0(A& amp-B))), (XV) ((0(AdB))d ((0A)& amp-B)), (XVI) (((0A)& amp-B)3(0(A3B))), (XVII) ((0(0^)^), (XVIII) (A3(0(0A))), (XIX) (Av (0A)).
Исчисление HPCont имеет единственное правило вывода — правило модус поненс в L. Вспомним, что правило модус поненс в L — это множество всех упорядоченных троек вида
© Попов В. М., 2016 г.
& lt-A, (ЛзБ), B& gt-, где A и B — L-формулы, а применение правила модус поненс в L — это элемент данного правила. Определение 1: а называем HPCont-выводом длины n (n — целое положительное число) из множества Г L-формул L-формулы A, если существуют такие L-формулы А1з…, An, что, а есть n-членная последовательность L-формул, первый член которой есть Ai,…, n-ный член которой есть An, An есть A, и для всякого целого положительного числа i, которое меньше или равно n, выполняется следующее условие: Ai принадлежит множеству Г, или Ai есть аксиома исчисления HPCont, или существуют такие целые положительные числа k и l, которые строго меньше i, что & lt-Ak, Al, Ai& gt- есть применение правила модус поненс в L. Определение 2: а является HPCont-выводом из множества Г L-формул L-формулы A, если существует такое целое положительное число n, что, а есть HPCont-вывод длины n из множества Г L-формул L-формулы A. Определение 3: L-формула A HPCont-выводима из множества Г L-формул, если существует HPCont-вывод из множества Г L-формул L-формулы A. Определение 4: L-формула A HPCont-доказуема, если существует HPCont-вывод из пустого множества L-формул L-формулы A. Определяем PCont как множество всех HPCont-доказуемых L-формул. Можно доказать, что PCont является логикой.
Элементарной L-формулой называем L-формулу, которая является
пропозициональной переменной языка L или имеет вид ((-iq)), где q есть пропозициональная переменная языка L. Называем PCont-оценкой такое отображение v множества всех элементарных L-формул во множество {0,1}, что для всякой пропозициональной переменной p языка L верно следующее: если v (p)=0, то v ((-ip))=1. Называем PCont-означиванием при PCont-оценке v такое отображение f множества всех L-формул во множество {0,1}, что для всякой пропозициональной переменной p языка L и всяких L-формул A и B выполняются условия:
(1) f (p)= v (pX (2) f ((0p))= ЧЬР^
(3) f ((A& amp-B))=1 тогда и только тогда, когда f (A)=1 и f (B)=1,
(4) f ((AvB))=1 тогда и только тогда, когда f (A)=1 или f (B)=1,
(5) f ((A3B))=1 тогда и только тогда, когда f (A)=0 или f (B)=1,
(6) f ((-1 (A& amp-B)))=1 тогда и только тогда, когда f ((-A))=1 или f ((-B))=1,
(7) f ((-i (AvB)))=1тогда и только тогда, когда f ((-A))=1 и f ((-В))=1,
(8) f ((-1 (A3B)))=1 тогда и только тогда, когда f (A)=1 и f ((-В))=1,
(9) f ((-1 (-A)))=1 тогда и только тогда, когда f (A)=1.
Можно доказать, что для всякой PCont-оценки существует единственное PCont-означивание при этой PCont-оценке. PCont-означивание при PCont-оценке v обозначаем через 9v.
Определение 5: PCont-общезначимой L-формулой является такая L формула A, что для всякой PCont-оценки v 9v (A)=1.
Определение 6: L-формула A PCont-следует из множества Г L-формул, если для всякой PCont-оценки v верно следующее: если для всякой L-формулы B из Г 9v (B)=1, то 9v (A)=1.
Лемма 0.
Для всякой L-формулы A и для всякой PCont-оценки v: если 9v (A)=0,to 9v ((-A))=1.
Лемма 0 доказана индукцией по длине L-формулы.
Лемма 1.
Всякая аксиома исчисления HPCont является PCont-общезначимой L-формулой.
Доказательство леммы 1 сводится к рутинной проверке того, что если L-формула имеет хотя бы один из указанных выше видов (I) — (XVIII), то она является PCont-общезначимой L-формулой, и к доказательству с помощью леммы 0 PCont-общезначимости любой L-формулы вида (XIX).
В свете леммы 1 и определений 5 и 6 очевидна следующая лемма 2.
Лемма 2.
Для всякого множества Г L-формул и для всякой аксиомы A исчисления HPCont верно, что A PCont-следует из Г.
Доказательство нижеследующей леммы 3 легко провести методом от противного, используя определение PCont-означивания при заданной PCont-оценке и определение 6.
Лемма 3.
Для всякого множества Г L-формул и для всяких L-формул A и B: если A PCont-следует из Г и (AzB) PCont-следует из Г, то B PCont-следует из Г.
Лемма 4.
Для всякого множества Г L-формул, для всякого целого положительного числа n и для всяких L-формул Ai,…, An: если для всякого целого положительного числа i, которое меньше или равно n, верно, что Ai принадлежит множеству Г, или Ai есть аксиома исчисления HPCont, или существуют строго меньшие i целые положительные числа k и 1, для которых упорядоченная тройка & lt-Ak, Ai, Ai& gt- есть применение правила модус поненс в L, то An PCont-следует из Г.
Простое доказательство леммы 4 можно провести методом возвратной индукции, опираясь на леммы 2 и 3.
Опираясь на лемму 4 и определения 1, 2 и 3, легко доказать следующую теорему 1.
Теорема 1.
Для всякого множества Г L-формул и для всякой L-формулы A: если A HPCont-выводима из Г, то A PCont-следует из Г.
Теперь нам потребуется еще одно определение. PCont-оценочным множеством называем множество Г L-формул, удовлетворяющее следующим условиям:
(1) для всяких L-формул A и B: (A& amp-B) принадлежит множеству Г
тогда и только тогда, когда A принадлежит множеству Г и B принадлежит множеству Г,
(2) для всяких L-формул A и B: (AvB) принадлежит множеству Г тогда и только тогда, когда A принадлежит множеству Г или B принадлежит множеству Г,
(3) для всяких L-формул A и B: (Az& gt-B) принадлежит множеству Г тогда и только тогда, когда A не принадлежит множеству Г или B принадлежит множеству Г,
(4) для всяких L-формул A и B: (-i (A& amp-B)) принадлежит множеству Г тогда и только тогда, когда (-A) принадлежит множеству Г или (-B) принадлежит множеству Г,
(5) для всяких L-формул A и B: (-i (AvB)) принадлежит множеству Г тогда и только тогда, когда (-A) принадлежит множеству Г и (-B) принадлежит множеству Г,
(6) для всяких L-формул A и B: (-i (A^B)) принадлежит множеству Г тогда и только тогда, когда A принадлежит множеству Г и (-B) принадлежит множеству Г,
(7) для всякой L-формулы A: (-1(-A)) принадлежит множеству Г тогда и только тогда, когда A принадлежит множеству Г.
Лемма 5.
Для всякого множества Г L-формул и для всякой L-формулы A: если неверно, что A HPCont-выводима из Г, то существует такое PCont-оценочное множество А, что Г включается в, А и при этом неверно, что A HPCont-выводима из А.
Доказательство леммы 5 начинаем с допущения о том, что K есть множество L-формул и F есть L-формула, удовлетворяющие условию: неверно, что F HPCont-выводима из K. Затем, используя лемму Цорна, показываем, что во множестве {Е|Е есть множество L-формул, K включается в Е и неверно, что F HPCont-выводима из Е}, упорядоченном отношением теоретико-множественного включения, имеется максимальный элемент.
Далее, зафиксировав произвольный максимальный элемент M указанного множества, показываем, что M является PCont-оценочным множеством. Отсюда, учитывая, что K включается в M и неверно, что F HPCont-выводима из M, заключаем, что существует такое PCont-оценочное множество А, что K включается в, А и неверно, что F HPCont-выводима из А. Доказательство леммы 5 завершаем снятием первоначального допущения и соответствующим обобщением.
Лемма 6.
Для всякого PCont-оценочного множества Г существует такая PCont-оценка v, что для всякой L-формулы A верно следующее: 9v (A)=1 тогда и только тогда, когда A принадлежит множеству Г.
Доказательство леммы 6 начинаем с допущения, что K есть произвольное PCont-оценочное множество и w есть множество {& lt-x, y>-| x есть элементарная L-формула, у принадлежит множеству {0,1}, (y=1 тогда и только тогда, когда x принадлежит множеству K)}. Затем, заметив, что w есть PCont-оценка, доказываем возвратной индукцией по длине L-формулы утверждение, гласящее, что для всякого целого неотрицательного числа n и для всякой L-формулы A длины n верно следующее: 9w (A)=1 тогда и только тогда, когда A принадлежит множеству K. Опираясь на это утверждение, приходим к выводу, что для всякой L-формулы A: 9w (A)=1 тогда и только тогда, когда A принадлежит множеству K. Используя данный вывод и тот факт, что w есть PCont-оценка, получаем, что существует такая PCont-оценка v, что для всякой L-формулы A верно следующее: 9v (A)=1 тогда и только тогда, когда A принадлежит множеству K. Доказательство леммы 6 завершаем снятием первоначального допущения и соответствующим обобщением.
Теорема 2.
Для всякого множества Г и для всякой L-формулы A: если A PCont-следует из Г, то A HPCont-выводима из Г.
Докажем теорему 2.
(1) K есть множество L-формул (допущение).
(2) F есть L-формула (допущение).
(3) F PCont-следует из K (допущение).
(4) Неверно, что F HPCont-выводима из K (допущение).
(5) Существует такое PCont-оценочное множество А, что K включается в, А и неверно, что F HPCont-выводима из, А (из (1), (2) и (4), по лемме 5).
Пусть (6) А0 есть PCont-оценочное множество, K включается в А0 и неверно, что F HPCont-выводима из А0.
(7) А0 есть PCont-оценочное множество (из (6)).
(8) Существует такая PCont-оценка v, что для всякой L-формулы A верно следующее: 9v (A)=1 тогда и только тогда, когда A принадлежит множеству А0 (из (7), по лемме 6).
Пусть (9) w есть PCont-оценка и для всякой L-формулы A верно следующее: 9w (A)=1 тогда и только тогда, когда A принадлежит множеству А0.
(10) K включается в А0 (из (6)).
(11) Для всякой A из K верно, что 9w (A)=1 (из (9) и (10)).
Ясно, что (12) для всякого множества L-формул Г и для всякой формулы A из Г верно, что A HPCont-выводима из Г.
(13) Неверно, что F HPCont-выводима из А0 (из (6)).
(14) А0 есть множество L-формул (из (7), по определению PCont-оценочного множества).
(15) F не принадлежит множеству А0 (из (2), (12), (13) и (14)).
(16) Для всякой L-формулы A верно следующее: 9w (A)=1 тогда и только тогда, когда A принадлежит множеству А0 (из (9)).
(17) Неверно, что 9w (F)=1 (из (2), (15) и (16)).
(18) Для всякой PCont-оценки v верно следующее: если для всякой L-формулы B из K 9v (B)=1, то 9v (A)=1 (из (3), по определению 6).
(19) w есть PCont-оценка (из (9)).
(20) Если для всякой L-формулы B из K 9w (B)=1, то 9w (A)=1 (из (18) и (19)).
(21) 9w (F)=1 (из (11) и (20)).
Утверждение (21) противоречит утверждению (17). Следовательно, неверно допущение (4). Итак, (22) F HPCont-выводима из K. Завершаем доказательство теоремы 2, снимая допущения (1), (2) и (3) и обобщая.
Из теорем 1 и 2 вытекает следующая теорема 3.
Теорема 3.
Для всякого множества Г L-формул и для всякой L-формулы A:
A HPCont-выводима из Г тогда и только тогда, когда A PCont-следует из Г.
Учитывая, что множество всех PCont-общезначимых L-формул равно множеству всех L-формул, PCont-следующих из пустого множества, и опираясь на теорему 3 и определения, получаем, что верна следующая теорема 4.
Теорема 4.
Для всякой L-формулы A: A HPCont-доказуема тогда и только тогда, когда A PCont-общезначима.
Из теоремы 4 и того, что PCont есть логика, равная множеству всех HPCont-доказуемых L-формул, вытекает следующая теорема 5 о семантической характеризации (в терминах построенной двузначной семантики) логики PCont.
Теорема 5.
Для всякой L-формулы A: A принадлежит логике PCont тогда и только тогда, когда A PCont-общезначима.
* Работа выполнена при поддержке РФФИ № 13−06−147а.
Литература
1. Попов В. М. Между Par и множеством всех формул //Шестые Смирновские чтения по логике: материалы Междунар. Науч. Конф., Москва, 17−19 июня 2009 г. -М: Современные тетради, 2009. С. 93−95.
2. Розоноэр Л. И. О выявлении противоречий в формальных теориях. I //Автоматика и телемеханика, № 6,1983. С. 113−124.

ПоказатьСвернуть
Заполнить форму текущей работой