АНАЛИТИКО-ТАБЛИЧНАЯ АКСИОМАТИЗАЦИЯ ИНТУИЦИОНИСТСКИХ ВАСИЛЬЕВСКИХ ЛОГИК Солощенков А.А.

Московский государственный университет им. М.В. Ломоносова


Номер: 12-1
Год: 2014
Страницы: 270-271
Журнал: Актуальные проблемы гуманитарных и естественных наук

Ключевые слова

васильевская логика, интуиционистская пропозициональная логика, аналитическая таблица, правило редукции, Vasiliev’s logic, intuitionistic propositional logic, analytical table, rule of reduction

Просмотр статьи

⛔️ (обновите страницу, если статья не отобразилась)

Аннотация к статье

В статье описан метод построения аналитико-табличных аксиоматизаций интуиционистских васильевских локиг. Эти аксиоматизации удобны в применении и предназначены для организации машинного поиска вывода.

Текст научной статьи

В [1] введены в рассмотрение логики Int , где x и y принадлежат множеству {0, 1, 2,…ω }. Интуиционистской васильевской логикой принято называть любую логику Int , где x и y принадлежат множеству {0, 1, 2,…ω } и при этом хотя бы одно из чисел x или y не равно 0. Заметим, что Int< 0,0> есть интуиционистская пропозициональная логика. В предлагаемой работе описан метод построения по любым таким числам x и y из {0, 1, 2,…ω }, что x или y не равно 0, аналитико-табличной аксиоматизации интуиционистской васильевской логики Int. Получаемые аналитико-табличные исчисления имеют простые правила и удобны для поиска вывода. Язык L, являющийся языком всех рассматриваемых здесь логик, есть стандартно определяемый пропозициональный язык, алфавиту которого принадлежат только следующие символы: p1, p2, p3, …(пропозициональные переменные языка L), &, Ú, É (бинарные логические связки языка L), Ø (унарная логическая связка языка L), левая и правая круглые скобки. Принимаем обычные соглашения об опускании скобок в L - формулах и используем «формула» как сокращение для « L- формула». Следуя [1], квазиэлементарной формулой называем формулу, в которую не входит ни одна бинарная логическая связка языка L, а длиной квазиэлементарной формулы называем число всех вхождений Ø в эту формулу. Условимся, что α и β являются произвольными фиксированными числами из {0, 1, 2,…ω }. Воспроизведем данное в [1] определение исчисления HInt< α,β> . Исчисление HInt< α,β> является исчислением гильбертовского типа, язык которого есть L. Правило модус поненс в L - единственное правило этого исчисления. Выводы в этом исчислении (в частности, доказательства в этом исчислении) строятся обычным для гильбертовского типа исчислений образом. Множеству всех аксиом исчисления HInt< α,β> принадлежат все те и только те формулы, каждая из которых имеет хотя бы один из следующих видов (здесь и далее A, B и C - формулы): (A É B) É ((B É C) É (A É C)) , (II) A É (A Ú B), (III) B É (A Ú B), (IV) (A ÉC) É ((B ÉC) É ((A ÚB) É 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, α) Ø D É (D É A), где D есть формула, не являющаяся квазиэлементарной формулой длины меньше α, (XI, β) (E É Ø (A É A)) É Ø E, где E есть формула, не являющаяся квазиэлементарной формулой длины меньше β. Построим в стиле работы [3] аналитико-табличное исчисление TInt< α,β>, эквиполентное исчислению HInt< α,β> в смысле сформулированной ниже Теоремы. Отмеченной формулой называем выражение вида QA, где Q есть символ T или символ F, а A есть формула рассматриваемого языка. Условимся букву M использовать для обозначения конечных множеств отмеченных формул. Условимся также, что MT есть множество всех отмеченных формул из M, каждая из которых начинается символом T. Правила редукции исчисления TInt<α,β> (TInt<α,β>-правила редукции) есть следующие правила. Правило [T&] есть множество всех упорядоченных пар , где TA&BÎM. Правило [F&] есть множество всех упорядоченных троек , где FA&BÎM. Правило [TÚ] есть множество всех упорядоченных троек , где TAÚBÎM. Правило [FÚ] есть множество всех упорядоченных пар , где FAÚBÎM. Правило [TÉ] есть множество всех упорядоченных троек , где TAÉBÎM. Правило [FÉ] есть множество всех упорядоченных пар , где FAÉBÎM. Правило [TØ] есть множество всех упорядоченных пар , где TØAÎM и A не является квазиэлементарной формулой длины меньше α. Правило [FØ] есть множество всех упорядоченных пар , где FØAÎM и A не является квазиэлементарной формулой длины меньше β. Определения применения TInt<α,β>-правила редукции к множеству отмеченных формул, однопосылочного, двухпосылочного TInt<α,β>-правил редукции, конфигурации, результата применения TInt<α,β>-правила редукции к конфигурации, аналитической TInt<α,β>-таблицы, начальной конфигурации данной аналитической TInt<α,β>-таблицы, последней конфигурации данной аналитической TInt<α,β>-таблицы, замкнутого множества отмеченных формул, замкнутой конфигурации, замкнутой аналитической TInt<α,β>-таблицы и формулы, доказуемой в TInt<α,β>, аналогичны соответствующим определениям из этой работы [3]. Теорема. Для всякой формулы А верно: формула А доказуема в HInt< α,β> тогда и только тогда, когда существует замкнутая аналитическая TInt<α,β> -таблица, начальная конфигурация которой есть {{FA}}.

Научные конференции

 

(c) Архив публикаций научного журнала. Полное или частичное копирование материалов сайта возможно только с письменного разрешения администрации, а также с указанием прямой активной ссылки на источник.