21 марта 2016г.
Логика направленности изменения была построена польским логиком Л. Роговским в виде аксиоматического пропозиционального исчисления[1].
Язык LR системы 4-местных секвенций логики направленности изменения строится обычным образом.
Символы p, g, r, p1,…,pn… обозначают пропозициональные переменные. Символы вида ® (импликация), ~(отрицание), В (оператор «возникает, что…»), И (оператор «исчезает, что…»), Т(оператор сильного утверждения «есть так, что…»), У(оператор «уже есть так, что…»), Е(оператор «еще есть так, что…») являются логическими константами.
Стандартно определяется понятие правильно построенной формулы; множество правильно построенных формул обозначим через For. Cимволы А, С, Д - обозначают произвольные формулы из For ; символы вида G, D,
L, S обозначают конечные наборы формул из For, возможно пустые . Выражения вида Г, А или А, Г есть
сокращение для – Г È {A}.
Определение 1. Помеченной формулой в языке LR называется выражения вида iA, где i Î V4 = {3, 2, 1, 0}, А Î For.
Помеченные формулы 3А, 2А, 1А и 0А соответственно читаются «А истинно», «А подистинно» «А подложно» и «А ложно».
Фактически мы расширили язык LR операциями 3, 2, 1, 0 (т.е. LR+ = LR È {3, 2, 1, 0}), которые являются
синтаксическими копиями истинностных значений из множества V4 = {3, 2, 1, 0}. Графически мы не различаем знаков истинностных значений и знаков операций, соответствующих этим истинностным значениям, так как контекст их употребления всегда позволяет различать синтаксическое и семантическое использование этих знаков.
Задать секвенциональное исчисление означает: указать аксиомы, логические и структурные правила вывода, определить понятие секвенционального вывода и выводимой секвенции. Но сначала дадим семантическое обоснование логических правил.
Определение 2. 4-х местной секвенцией помеченных формул называется выражение вида D = D0 | D1| D2| D3, где для каждого i (0 ≤ i ≤3), Di есть конечные наборы помеченных формул, и называется компонентами секвенции, т.е. Di = {iA| i, A Î LR+}. Например, при явном указании помеченных формул секвенция D имеет вид 0А|1B, 1С|2A|3C. В секвенции D могут отсутствовать те или иные компоненты, например в секвенции D = 0А нет трех последних компонент, они пустые.
Назовем секвенцию D полной, если все ее компоненты Di , i (0 ≤ i ≤3) не являются пустыми. В противном случае, т.е. когда имеется пустая компонента Di , секвенция называется неполной. Назовем секвенцию D пустой, если все ее компоненты Di , i (0 ≤ i ≤3) пустые.
Замечание. Будем предполагать, что компоненты секвенции перестановочны, чтобы не вводить специального структурного правила перестановки компонент секвенции.
Метазнак ―|‖ понимается дизъюнктивно, т.е. выражение D0| D1| D2| D3 читается как D0, или D1, или D2, или D3.
Введем сокращения для записи секвенции. Разделительный знак в записи секвенций ―|‖ устраняется; одна и та же формула, принадлежащая различным компонентам секвенции, обозначается как единое целое. Например, секвенция вида 0А|1B,1С|2A|3C будет иметь вид 02А, 1В, 13С. При желании легко восстанавливается полная запись секвенции. Такое сокращение мотивировано интересами лучшего обозрения шагов секвенционального вывода.
В определении понятий, относящихся к описанию вывода, следуем Г. Такеути, но с поправками, уместными для 4-х- значной логики [2].
есть непосредственный вывод, где S1, S2, S3, S секвенции; S1, S2, S3 назовем верхними секвенциями, а S – нижней секвенцией, т.е в непосредственных выводах бывают одна или две, или три посылки.
Аксиома (начальная секвенция): 0123А (VA – сокращенное обозначение).
Начальные секвенции – это секвенции, которые не являются заключением никакого правила вывода. Непосредственные выводы получаем применением логических и структурных правил вывода. Логические правила SR4:
Правила введения импликации
Секвенции, расположенные выше черты в сформулированных правилах, называются посылками правил, секвенции находящиеся ниже черты – заключением правил.
Помеченные формулы в посылках логических правил называются боковыми формулами. Помеченные формулы в заключении логических правил называются главными формулами. Будем также считать боковой формулой помеченные формулы посылки правила сокращения.
Определение 4.1. Выводом Р в логике SR4 направленности изменения называется дерево секвенций, которое удовлетворяет следующим условиям:
(1). Самые верхние секвенции в Р являются аксиомами (начальными секвенциями);
(2). Каждая секвенция в Р, кроме самой нижней, является верхней секвенцией непосредственного вывода. Самая нижняя секвенция принадлежит Р.
Из этого определения следует, что самая нижняя секвенция в Р единственна.
Определение 4.2. Самая нижняя секвенция S в Р называется
заключительной секвенцией. Вывод Р с заключительной секвенцией S называется выводом секвенции S, а сама секвенция S называется выводимой. Формула Д называется выводимой, если выводима секвенция 3Д.
Требование построить секвенциональный вывод формулы Д будем обозначать через «ÞД».
Определение. 4.3. Выводом с сечением в SR4 называется вывод, в котором применяется правило сечения. В противном случае вывод называется выводом без сечения.
Принимается стандартное определение формулы в данном выводе
(секвенции) как формулы, рассматриваемой с фиксированным местом, которое она занимает в данном выводе (секвенции). Подвыводом вывода Р называется всякая часть Р, которая сама является выводом.
Список литературы
1.
Rogowski L.S. Logika kierunkowa a heglowska teza o spreczności zmiany. Toruń: Towarzystwo naukowe w Toruniu. 1964. T. XY. Zeszyt 2.
2.
Такеути Г. Теория доказательства. М.: Мир. 1978
