26 марта 2016г.
32 Исследование выполнено при поддержке РГНФ, грант № 13-03-00088а.
В работе [4] рассматриваются логики вида Int, где x и y принадлежат множеству {0,1,2,3,...ω}. Все эти логики, исключая логику Int<0,0>, являются согласно [4] паралогиками, а согласно [2] - Int-логиками васильевского типа. Int<0,0> есть (см.[4]) интуиционистская пропозициональная логика. В предлагаемой статье строится для произвольных фиксированных α и β из {0,1,2,3,...ω} разрешимое секвенциальное исчисление, аксиоматизирующее логику Int<α,β>.
Язык L всех рассматриваемых здесь логик есть стандартно определяемый пропозициональный язык, алфавиту которого принадлежат следующие символы: p1, p2, p3,…(пропозициональные переменные языка L), &,
Ú, É (бинарные логические связки языка L), Ø (унарная логическая связка языка L), левая и правая круглые скобки. Никакие другие символы не принадлежат алфавиту языка L. Определение L-формулы обычно. Допускаем применение известных соглашений об опускании скобок в L-формулах и используем «формула» как сокращение для « L-формула». Квазиэлеменарной формулой называем формулу, в которую не входит ни одна бинарная логическая связка языка L. Длиной формулы называем, как это принято, число всех вхождений логических связок в эту формулу. Логикой называем, следуя [3], непустое множество формул, замкнутое относительно правила modus ponens в L и относительно правила подстановки формулы в формулу вместо пропозициональной переменной языка L. Термины «паранепротиворечивая логика», «параполная логика»,
«паранормальная логика», «паралогика» понимаем в соответствии с их определениями, данными в [3]. Пусть α и β — произвольные элементы множества {0,1,2,3,...ω}. Определим исчисление HInt < α,β> . HInt<α,β> есть исчисление гильбертовского типа, язык этого исчисления есть L. Единственное правило вывода этого исчисления есть modus ponens в L. Понятие доказательства в HInt<α,β> и понятие доказуемой в HInt< α,β > формулы определяются обычным для исчислений гильбертовского типа образом. Множество всех аксиом исчисления HInt<α,β> принадлежат все те и только те формулы, каждая из которых имеет хотя бы один из следующих одиннадцати видов (A, B и C есть формулы):
Int<α,β> есть паранормальная логика, (2) если α≠0 и β=0,
то Int<α,β> есть паранепротиворечивая логика, не являющаяся параполной логикой, (3) если α=0 и β≠0,
то Int<α,β> есть параполная логика, не являющаяся паранепротиворечивой логикой, (4) если α=0 и β=0,
то Int< α,β > есть множество всех интуиционистских тавтологий в языке L (то есть Int<0,0> есть интуиционистская пропозициональная логика в
языке L). Определим исчисление GInt<α,β>. GInt<α,β> есть секвенциальное исчисление генценовского типа. Секвенциями называем выражения вида π→ ρ, где π и ρ — конечные последовательности формул (пустая
последовательность формул есть конечная
последовательность формул),
при этом π — не более, чем одночленная последовательность формул. Множество всех основных секвенций
исчисления GInt<α,β> есть множество всех секвенций вида A →A, где A есть формула. Множеству всех правил исчисления GInt<α,β> принадлежат все нижеследующие правила R1-R12, R13(α), R14(β), правило сечения и не принадлежат никакие другие правила.
Во избежание типографских трудностей, связанных
с набором двумерных
комплексов формальных выражений, мы формулируем поименованные выше правила, используя
не стандартное двумерное
их представление, но одномерное (линейное) представление соответствующих упорядоченных пар секвенций
и соответствующих упорядоченных
троек секвенций. Мы используем жирную запятую , в качестве знака, отделяющего секвенции друг от друга. Условимся, что
здесь A и B — формулы, а Γ и Δ — конечные
последовательности формул, Θ — не более чем одночленная последовательность формул.
Доказательства в GInt<α,β> строятся обычным для секвенциальных исчислений генценовского типа
образом, определение секвенции, доказуемой в GInt<α,β> ,
также обычно для подобного рода исчислений. Методами, предложенными в [1], доказаны
теорема об устранимости сечения для GInt<
α,β > и разрешимость этого исчисления. Доказано, что GInt<α,β> является секвенциальной аксиоматизацией логики Int<α,β> , то есть доказано следующее утверждение: для всякой формулы
A верно, что AϵInt < α,β > тогда и только тогда, когда секвенция
→ A доказуема в GInt< α,β >. Таким образом, логика Int<α,β> разрешима.
Список литературы
1.
Генцен Г. Исследование логических выводов // Математическая теория логического вывода. М., 1967. С. 9- 74.
2.
Попов В.М.
Секвенциальная
аксиоматизация и семантика I-логик васильевского
типа // Логические исследования. № 22 (в печати).
3.
Попов В.М. Секвенциальные аксиоматизации простых паралогик // Логические исследования. Вып.
16. М.- СПб, ЦГИ, 2010.
С. 205-220.
4.
Popov V. M. Between Int<ω,ω> and intuitionistic propositional logic // Logical Investigations. Vol. 19. M.-S.-Pb.: C.G.I., 2013. P.197-199.
