32    Исследование выполнено при поддержке РГНФ, грант № 13-03-00088а.

В работе [4] рассматриваются логики вида Int<x,y>, где 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.