Промежуточная Логика

Высказываний — произвольное непротиворечивое множество пропозициональных формул, замкнутое относительно правила вывода модус поненс и правила подстановки и содержащее все аксиомы интуиционистского исчисления высказываний I. Наиболее естественным способом задания П. л. являются промежуточные пропозициональные исчисления. Каждое такое исчисление задается указанием нек-рого числа классически общезначимых пропозициональных формул, добавляемых к аксиомам исчисления I. Совокупность всех П. л. образует дистрибутивную решетку относительно включения , причем конечно аксиоматизируемые П. л, образуют в ней подрешетку, в к-рую изоморфно вложима любая конечная дистрибутивная решетка. П. л. Lназ. разрешимой, если существует алгоритм, к-рый по каждой пропозициональной формуле Араспознает, принадлежит АП. л. L или нет. Так, разрешимыми являются интуиционистская и классическая П. л. Вообще, всякая финитно аппроксимируемая (см. ниже) конечно аксиоматизируемая П. л. разрешима. Построен пример конечно аксиоматизируемой неразрешимой П. л. (см. [7]). П. л. Lназ. дизъюнктивной, если из следует, что или . Этим свойством обладает, напр., интуиционистская П. л., но не обладает классическая П. л. Существует бесконечно много дизъюнктивных П. л. Интерполяционное свойство П. л. (теорема Крейга) состоит в том, что если формула принадлежит П. л. L, то существует формула С, содержащая только общие для Аи Впеременные и такая, что и ; если Аи Вне имеют общих переменных, то или . Показано, что интерполяционным свойством, кроме интуиционистской и классической П. л., обладают еще ровно пять П. л. (см. [6]). Формула Аназ. выразимой через формулы В 1, В 2,... в П. л. L, если Аможно получить из B1, В2, ... с помощью конечного числа замен на эквивалентные (в L) формулы и конечного числа подстановок ранее полученных формул вместо переменных. Список формул функционально полон в П. л. L, если всякая формула выразима в Lчерез S. Алгоритмическая проблема распознавания функциональной полноты любого списка формул разрешима для интуиционистской и нек-рых других П. л. (см. [3]). Другая алгоритмич. проблема — проблема распознавания выразимости Ачерез S по данным формуле Аи списку S — положительно решена лишь для нек-рых П. л.; она остается пока (1983) открытой для интуиционистской П. л. Другой способ задания П. л. дает т. н. семантич. подход. Под семантикой здесь понимается нек-рое множество S структур (моделей) , на к-рых определено отношение истинности данной пропозициональной формулы Апри данной оценке q (оценка — отображение, сопоставляющее переменным формулы Анек-рые значения в ). Формула А, истинная в при любой оценке, наз. общезначимой на (обозначение ). Если , то П. л. L(S1).есть совокупность всех формул, общезначимых на любой структуре . Для данной семантики Sестественно определяется отношение семантического следования , где Г состоит из формул; это отношение означает, что для любой структуры из для всех следует Семантики S1 и S2 наз. эквивалентными, если отношения и совпадают. Основное требование, предъявляемое к семантике,- это ее корректность: из должно следовать . Все упоминаемые ниже семантики корректны. Другое важное свойство семантики — полнота. П. л. Lназ. полной относительно семантики S, если . Алгебраическая семантика SA состоит из псевдобулевых алгебр, т. е. алгебр вида где — унарная, а — бинарные операции на М, соответствующие связкам причем — дистрибутивная решетка, а 1 и 0 — наибольший и наименьший элементы в М. Операции и удовлетворяют свойствам: для любых Отношение здесь означает, что Апринимает в значение 1 при данной оценке q. Каждая П. л. полна относительно конечно порожденных псевдобулевых алгебр. Если П. л. Lполна относительно множества конечных псевдобулевых алгебр (одной конечной псевдобулевой алгебры), то она наз. финитно аппроксимируемой (соответственно табличной). Простейшей табличной П. л. является классическая П. л. Дизъюнктивные П. л., в частности интуиционистская, табличными не являются. Имеется пример не финитно аппроксимируемой конечно аксиоматизируемой П. л. (см. [3]). Семантика Кринке SK состоит из Крипке моделей, имеющих в данном случае вид , где — частично упорядоченное множество, наз. также остовом, или шкалой, а значениями оценки 6 . являются подмножества М, причем для любых из и следует . Между семантиками SA и SK имеется тесная связь (см. [5]), однако они не эквивалентны; в частности, существуют П. л., не полные относительно SK (см. [3]). Конструктивные семантики — это семантика реализуемости SR (см. [1]) и семантика финитных задач SF. Эти семантики не полны даже для интуиционистской П. л., более того, существуют формулы, общезначимые в SK и не общезначимые в SF, и наоборот. Предикатные П. л. определяются по аналогии с II. л. высказываний, т. е. это — расширения интуиционистской логики предикатов LI, содержащиеся в классич. логике предикатов. В отличие от пропозициональных П. л. все предикатные П. л. неразрешимы. Семантика предикатных П. л. аналогична соответствующей семантике П. л. высказываний (см. [2]). Лит.:[1] Новиков П. С., Конструктивная математическая логика с точки зрения классической, М., 1977; [2] Драгалин А. Г., Математический интуиционизм. Введение в теорию доказательств, М., 1979; [3] Кузнецов А. В., в кн.: Логический вывод, М., 1979, с. 5-33; [4] его уже, "Математические исследования", 1975, т. 10, в. 2, с. 150-58; [5] Эсакиа Л. Л., в кн.: Логический вывод, М., 1979, с. 147-72; [6] Максимова Л. Л.."Алгебра и логика", 1Й77, т. 16, с. 643-81; [7] Шехтман В. Б., "Докл. АН СССР", 1978, т. 340, № 3, с. 549-52; [8] Hosoi Т.. Ono H., "J. Tsuda College", 1073, v. 5, p. 67-82. С. К. Соболев.