Разрешимые классы псевдопредваренных формул

Для конструктивного (интуиционистского) исчисления предикатов без функциональных символов и равенства приводится полное описание, в терминах префикса и сигнатуры, классов сведения и разрешимых классов псевдопредваренных формул, т.е. формул, представимых в виде $PM$, где $M$ – бескванторная формула, $P$ – конечная последовательность кванторных комплексов и выражений $\rceil\rceil$.
При построении разрешимых классов основную роль играет операция $L^p$. Эта операция по любой псевдопредваренной формуле $A$ строит, сохраняя сигнатуру, такой список формул $\Gamma$, что $A$ тогда и только тогда выводима в конструктивном исчислении, когда какая-нибудь формула из $\Gamma$ выводима в классическом исчислении.
В работе сформулированы условия, достаточные для того, чтобы вынесение квантора $\forall$ из дизъюнкции и перестановки кванторов $\forall$ и $\exists$ сохраняли выводимость в конструктивном исчислении. Описывается также сохраняющий сигнатуру способ элиминации положительных вхождений равенства. Этот способ и указанные условия играют важную роль при построении классов сведения.
Рассматривается также проблема распознавания опровержимости псевдопредваренных формул на вполне конечных моделях Крипке, т.е. на таких моделях Крипке, у которых конечны как множество “моментов времени”, так и объединение предметных областей, дается полное описание, в терминах префикса и сигнатуры, классов псевдопредваренных формул, для которых разрешима проблема распознавания опровержимости на вполне конечных моделях Крипке. Это описание существенно расходится с описанием разрешимых классов псевдопредваренных формул для конструктивного исчисления предикатов. Библ. 25 назв.