WWW.MASH.DOBROTA.BIZ
БЕСПЛАТНАЯ  ИНТЕРНЕТ  БИБЛИОТЕКА - онлайн публикации
 

«нельсоновского типа1 В. М. Попов abstract. The sequent systems axiomatizing four Nelson’s type logics are presented. Ключевые слова: секвенция, исчисление, паранормальная логика, ...»

Секвенциальные аксиоматизации

пропозициональных логик

нельсоновского типа1

В. М. Попов

abstract. The sequent systems axiomatizing four Nelson’s type

logics are presented .

Ключевые слова: секвенция, исчисление, паранормальная логика,

паранепротиворечивая логика, параполная логика

Формулируются свободные от сечения секвенциальные аксиоматизации четырех пропозициональных логик, родственных логикам, определяемым построенными в [5] и в [6] исчислениями

N и N. В [5] предложены секвенциальные исчисления Ns и Ns, первое из которых эквиполентно исчислению N, а второе — исчислению N. Построенные ниже секвенциальные исчисления GPComp(N) и GPar(N) эквиполентны с точностью до несущественных деталей секвенциальному исчислению, являющемуся пропозициональной частью исчисления Ns, и секвенциальному исчислению, являющемуся пропозициональной частью исчисления Ns соответственно .

Язык L всех рассматриваемых здесь логик есть стандартный пропозициональный язык, алфавиту которого принадлежат все следующие символы и только они: &,, (бинарные логические связки языка L), ¬ (унарная логическая связка языка L), ) и ( (технические символы языка L), p1, p2, p3,... (пропозициональные переменные языка L). Допускаем применение обычных соглашений об опускании скобок в L-формулах и используем «формула» вместо «L-формула». Опишем исчисления Pабота выполнена пpи поддеpжке PГНФ, проект № 10-03-00570а .

Секвенциальные аксиоматизации пропозициональных логик... 247 HPar(N), HPContPComp(N), HPCont(N) и HPComp(N) гильбертовского типа, индуцирующие интересующие нас логики.



Множеству всех аксиом исчисления HPar(N) принадлежат все те и только те формулы, каждая из которых имеет хотя бы один из следующих семнадцати видов (здесь и далее A, B и C есть формулы):

(I) (A B) ((B C) (A C)), (II) A (AB), (III) A (B A), (IV) (A C) ((B C) ((AB) C)), (V) (A & B) A, (VI) (A & B) B, (VII) (C A) ((C B) (C (A & B))), (VIII) (A (B C)) ((A & B) C), (IX) ((A & B) C) (A (B C)), (X) ¬(A B) (¬A & ¬B), (XI) (¬A & ¬B) ¬(A B), (XII) ¬(A & B) (¬A ¬B), (XIII) (¬A ¬B) ¬(A & B), (XIV) ¬(A B) (¬A & B), (XV) (¬A & B) ¬(A B), (XVI) ¬¬A A, (XVII) A ¬¬A .

Множеству всех аксиом исчисления HPContPComp(N) принадлежат все те и только те формулы, каждая из которых имеет хотя бы один из видов (I)-(XVII) или имеет вид (A &¬A) (B ¬B). Множеству всех аксиом исчисления HPCont(N) принадлежат все те и только формулы, каждая из которых имеет хотя бы один из видов (I)-(XVII) или имеет вид (B ¬B). Множеству всех аксиом исчисления HPComp(N) принадлежат все те и только формулы, каждая из которых имеет хотя бы один из видов (I)-(XVII) или имеет вид (A &¬A) B. Каждое из исчислений HPar(N), HPContPComp(N), HPCont(N), HPComp(N) имеет единственное правило вывода — правило modus ponens в L. Во всяком из этих исчислений выводы (в частности, доказательства) строятся обычным для гильбертовского типа исчисВ. М. Попов лений образом. Опираясь на вышеприведенные определения исчислений HPar(N), HPContPComp(N), HPCont(N), HPComp(N) и данные в [2] определения исчислений HPar, HPContPComp, HPCont, HPComp, замечаем, что язык всех указанных исчислений есть L, каждое из этих исчислений имеет единственное правило вывода — правило modus ponens в L, выводы (в частности, доказательства) во всех этих исчислениях строятся обычным для гильбертовского типа исчислений образом, множество всех аксиом исчисления HPar (исчисления HPContPComp, исчисления HPCont, исчисления HPComp) есть объединение множества всех аксиом исчисления HPar(N) (исчисления HPContPComp(N), исчисления HPCont(N), исчисления HPComp(N) соответственно) с множеством всех формул вида ((A B) A) A .



Кроме того, можно доказать, что формула ((p1 p2 ) p1 ) p1 недоказуема ни в одном из исчислений HPar(N), HPContPComp(N), HPCont(N), HPComp(N). Таким образом, исчисления HPar(N), HPContPComp(N), HPCont(N), HPComp(N) являются собственными сужениями исчислений HPar, HPContPComp, HPCont, HPComp соответственно. Определяем Par(N) как множество всех формул, доказуемых в HPar(N). Аналогично определяем PContPComp(N), PCont(N) и PComp(N). Термины «логика», «паранепротиворечивая логика» и «паранормальная логика» далее используем в соответствии с их определениями, данными в [3]. Можно доказать, что (а) Par(N) и PContPComp(N) есть различные паранормальные логики, при этом Par(N) PContPComp(N), (б) PCont(N) есть паранепротиворечивая, но не параполная логика, (в) PComp(N) есть параполная, но не паранепротиворечивая логика, (г) PContPComp(N) PCont(N) PComp(N), но PContPComp(N) и PCont(N) PComp(N) не равны .

Приступим теперь к конструированию секвенциальных исчислений GPar(N), GPContPComp(N), GPCont(N), GPComp(N) .

Построение каждого из этих исчислений аналогично построению исчисления GPContPComp в работе [3]. Обозначая через Секвенциальные аксиоматизации пропозициональных логик... 249 ВИП(N) секвенциальное правило, являющееся множеством всех упорядоченных пар вида (A • ) B, A B, где — последовательность формул, определяем множество всех правил вывода каждого из исчислений GPar(N), GPContPComp(N), GPCont(N) и GPComp(N) как такое множество М, что П М тогда и только тогда, когда П есть ВИП(N) или любое, исключая ВИП, правило вывода исчисления GPContPComp. Множество всех основных секвенций исчисления GPar(N) есть множество всех секвенций вида A A. Множество всех основных секвенций исчисления GPContPComp(N) есть объединение множества всех основных секвенций исчисления GPar(N) с множеством всех секвенций вида A,¬A B,¬B. Множество всех основных секвенций исчисления GPCont(N) есть объединение множества всех основных секвенций исчисления GPar(N) с множеством всех секвенций вида A,¬A. Множество всех основных секвенций исчисления GPComp(N) есть объединение множества всех основных секвенций исчисления GPar(N) с множеством всех секвенций вида A,¬A. Выводы во всех секвенциальных исчислениях GPar(N), GPContPComp(N), GPCont(N) и GPComp(N) строятся обычным для этого типа исчислений образом. Для каждого из этих исчислений доказана теорема об устранимости сечения. С использованием этой теоремы показано, что исчисления GPar(N), GPContPComp(N), GPCont(N), GPComp(N) являются секвенциальными аксиоматизациями логик Par(N), PContPComp(N), PCont(N), PComp(N), соответственно. Точнее, доказана теорема о том, что для всякой логики L из {Par(N), PContPComp(N), PCont(N), PComp(N)} и для всякой формулы A верно, что секвенция A выводима в GL тогда и только тогда, когда A L .



Можно доказать также следующее утверждение: позитивный фрагмент любой из логик Par(N), PContPComp(N), PCont(N), PComp(N) является позитивным фрагментом интуиционистской пропозициональной логики, язык которой есть L. В свете утверждения ясно, что ни одна из логик Par(N), PContPComp(N), PCont(N), PComp(N) не имеет конечной характеристической матрицы. Тем не менее, все эти логики разрешимы. Разрешимость любой из указанных логик вытекает из разрешимости построенного выше секвенциального исчисления, аксиоматизирующего эту логику. В свою 250 В. М. Попов очередь, для каждого исчисления GPar(N), GPContPComp(N), GPCont(N), GPComp(N) разрешимость доказывается генценовским методом, который впервые применен в [1]. При этом в ходе применения генценовского метода для доказательства разрешимости исчисления G из{GPar(N), GPContPComp(N), GPCont(N), GPComp(N)} используется нижеследующая теорема об обобщенной подформульности G-выводов, а не аналог теоремы 2.513 из [1] (теоремы о подформульности LI-выводов и LK-выводов) .

ТЕОРЕМА. Пусть G {GPar(N), GPContPComp(N), GPCont(N), GPComp(N)} .

Если формула A есть подформула формулы, входящей в некоторую секвенцию, принадлежащую G-выводу, последняя секвенция которого есть S, то (1) если A не имеет вид ¬B ни для какой формулы B, то A есть подформула некоторой формулы, входящей в S, (2) если A имеет вид ¬B для некоторой формулы B, то по крайней мере одна из формул B или ¬B есть подформула некоторой формулы, входящей в S .

В заключение заметим, что естественно возникающая проблема построения свободной от сечения секвенциальной аксиоматизации логики PCont(N) PComp(N) открыта .

Литература [1] Генцен Г. Исследования логических выводов // Математическая теория логического вывода. М., 1967. С.9-74 .

[2] Попов В.М. Между Par и множеством всех формул // Шестые смирновские чтения по логике. Материалы международной научной конференции 17-19 июня 2009. М., 2009. С. 93-95 .

[3] Попов В.М. Секвенциальная аксиоматизация паранормальной логики PContPComp // В настоящем сборнике .

[4] Смирнов В.А. Формальный вывод и логические исчисления//Смирнов В.А .

Теория логического вывода. М., 1999. С. 16-233 .

[5] Almukdad A., Nelson D. Constructible falsity and inexact predicates // J. Symb .

Log. 1984. Vol. 49. № 1. P. 231-233.




Похожие работы:

«МИНИСТЕРСТВО МЕЛИОРАЦИИ И ВОДНЫХ РЕСУРСОВ РЕСПУБЛИКИ ТАДЖИКИСТАН ПРОГРАММА РАЗВИТИЯ ООН В ТАДЖИКИСТАНЕ ОТДЕЛ ПОДДЕРЖКИ АССОЦИАЦИЙ ВОДОПОЛЬЗОВАТЕЛЕЙ РЕКОМЕНДАЦИИ ПО ПОДДЕРЖКЕ И РАЗВИТИЮ АССОЦИАЦИЙ ВОДОПОЛЬЗОВАТЕЛЕЙ В РЕСПУБЛИКЕ ТАДЖИКИСТАН МХК ВВУ УК-1 ВВ-1 ПБ ВО РК УК-2 ВВ-2 ПБ ВО ВВ-3 УК-3 ПБ ВО Д...»

«Всероссийская научно-техническая конференция студентов Студенческая научная весна 2014: Машиностроительные технологии http://studvesna.qform3d.ru УДК 658.512.23 ИСПОЛЬЗОВАНИЕ В ПРОФЕССИОНАЛЬНОЙ ДЕЯТЕЛЬНОСТИ ДИЗАЙНЕРА ЗНАНИЙ ПСИХОЛОГИИ ЗРИТЕЛ...»

«ФГБУ "ВСЕРОССИЙСКИЙ ЦЕНТР ГЛАЗНОЙ И ПЛАСТИЧЕСКОЙ ХИРУРГИИ" МИНИСТЕРСТВА ЗДРАВООХРАНЕНИЯ РОССИЙСКОЙ ФЕДЕРАЦИИ РОЛЬ АЛЛОТРАНСПЛАНТАТОВ В РЕКОНСТРУКТИВНОЙ ХИРУРГИИ ВЫВОРОТА НИЖНЕГО ВЕКА Нураева А. Б., Галимова В.У. Москва 2017 г. АКТУАЛЬНОСТЬ Эктропион...»

«ФЕДЕРАЛЬНОЕ АГЕНТСТВО ПО ТЕХНИЧЕСКОМУ РЕГУЛИРОВАНИЮ И МЕТРОЛОГИИ ГО С ТР НАЦИОНАЛЬНЫЙ 54473СТАНДАРТ РОССИЙСКОЙ 2011 ФЕДЕРАЦИИ НАНОПОКРЫТИЯ РЕЖУЩЕГО ИНСТРУМЕНТА НА ОСНОВЕ АЛМАЗА И КУБИЧЕСКОГО НИТРИДА БОРА Общие технические требования и методы испытаний Издание официальное Москва Стандартинформ с...»

«НОВОСТИ ИНВЕСТИЦИОННОГО ПРОЕКТА КОМПАНИИ "МЕТАФРАКС" / № 11 (11) | СЕНТЯБРЬ 2018 Г. НА СТРОЙПЛОЩАДКУ АКМ ДОСТАВЛЕН РЕАКТОР КАРБАМИДА | 1-3 | ГОТОВЫЕ ФУНДАМЕНТЫ СДАЮТСЯ ПОД МОНТАЖ | 4 | НА СТРОЙПЛОЩАДКУ АКМ ДОСТАВЛЕН РЕАКТОР КАРБАМИДА 20 СЕНТЯБРЯ НА СТРОЙПЛОЩАДКУ ИЗ ИТ...»

«Cамообследование авиационного учебного центра (АУЦ) ОАО "Международный аэропорт Минеральные Воды" В соответствии с приказом Министерства образования и науки от 14 июня 2013 г. № 462 "Об утверждении Порядка проведения самообследования образовательн...»

«ГОСТ Р 51242-98 ГОСУДАРСТВЕННЫЙ СТАНДАРТ РОССИЙСКОЙ ФЕДЕРАЦИИ КО НСТРУКЦИ И ЗА Щ И Т Н Ы Е М ЕХАН И ЧЕСКИ Е И ЭЛЕКТРОМ ЕХАНИЧЕСКИЕ ДЛЯ ДВЕРН Ы Х И О КОННЫ Х П РО ЕМ О В Технические требования и методы испытаний на устойчивость к разрушающим воздействиям И здание официал...»




 
2019 www.mash.dobrota.biz - «Бесплатная электронная библиотека - онлайн публикации»

Материалы этого сайта размещены для ознакомления, все права принадлежат их авторам.
Если Вы не согласны с тем, что Ваш материал размещён на этом сайте, пожалуйста, напишите нам, мы в течении 1-2 рабочих дней удалим его.