Теорема об устранимости сечения для GPContPComp

Рассматриваемая логика PContPComp принадлежит логическому интервалу между логикой Par и множеством всех формул. Установлено, что логика PContPComp является пересечением паранепротиворечивой логики PCont Батенса- Розоноэра с параполным напарником последней. Представляется, что логика PContPComp - наименее изученная логика из указанного интервала. Она является расширением наиболее известной паранормальной логики Par, которую в свое время открыло несколько человек (Брэди, Попов, Аврон). Всего нетривиальных расширений логики Par четыре – паранормальная логика PContPComp, паранепротиворечивая логика PCont, параполная логика PComp и классическая логика Cl. В работе дано подробное доказательство теоремы об устранимости сечения для предложенного В. М. Поповым секвенциального исчисления, аксиоматизирующего эту логику PContPComp. Впервые изучается дедуктивная система секвенциального исчисления, аксиоматизирующего данную логику. Устранимость сечения в данном исчислении значительно облегчает процедуру поиска доказательства, а также позволяет дать синтаксическую разрешающую процедуру.