Математическая энциклопедия - промежуточная логика

высказываний произвольное непротиворечивое множество пропозициональных формул, замкнутое относительно правила вывода модус поненс и правила подстановки и содержащее все аксиомы интуиционистского исчисления высказываний I.

Наиболее естественным способом задания П. л. являются промежуточные пропозициональные исчисления. Каждое такое исчисление задается указанием нек-рого числа классически общезначимых пропозициональных формул, добавляемых к аксиомам исчисления I.

Совокупность всех П. л. образует дистрибутивную решетку относительно включения , причем конечно аксиоматизируемые П. л, образуют в ней подрешетку, в к-рую изоморфно вложима любая конечная дистрибутивная решетка.

П. л. Lназ. разрешимой, если существует алгоритм, к-рый по каждой пропозициональной формуле Араспознает, принадлежит АП. л. L или нет. Так, разрешимыми являются интуиционистская и классическая П. л. Вообще, всякая финитно аппроксимируемая (см. ниже) конечно аксиоматизируемая П. л. разрешима. Построен пример конечно аксиоматизируемой неразрешимой П. л. (см. [7]).

П. л. Lназ. дизъюнктивной, если из следует, что или . Этим свойством обладает, напр., интуиционистская П. л., но не обладает классическая П. л. Существует бесконечно много дизъюнктивных П. л.

Интерполяционное свойство П. л. (теорема Крейга) состоит в том, что если формула принадлежит П. л. L, то существует формула С, содержащая только общие для Аи Впеременные и такая, что и ; если Аи Вне имеют общих переменных, то или . Показано, что интерполяционным свойством, кроме интуиционистской и классической П. л., обладают еще ровно пять П. л. (см. [6]).

Формула Аназ. выразимой через формулы В 1, В 2,... в П. л. L, если Аможно получить из B1, В2, ... с помощью конечного числа замен на эквивалентные (в L) формулы и конечного числа подстановок ранее полученных формул вместо переменных. Список формул S={B1, В 2,...} функционально полон в П. л. L, если всякая формула выразима в Lчерез S. Алгоритмическая проблема распознавания функциональной полноты любого списка формул разрешима для интуиционистской и нек-рых других П. л. (см. [3]). Другая алгоритмич. проблема проблема распознавания выразимости Ачерез S по данным формуле Аи списку S положительно решена лишь для нек-рых П. л.; она остается пока (1983) открытой для интуиционистской П. л.

Другой способ задания П. л. дает т. н. семантич. подход. Под семантикой здесь понимается нек-рое множество S структур (моделей) , на к-рых определено отношение истинности данной пропозициональной формулы Апри данной оценке q (оценка отображение, сопоставляющее переменным формулы Анек-рые значения в ). Формула А, истинная в при любой оценке, наз. общезначимой на (обозначение ). Если , то П. л. L(S1).есть совокупность всех формул, общезначимых на любой структуре . Для данной семантики Sестественно определяется отношение семантического следования , где Г состоит из формул; это отношение означает, что для любой структуры из для всех следует Семантики S1 и S2 наз. эквивалентными, если отношения и совпадают. Основное требование, предъявляемое к семантике,это ее корректность: из должно следовать . Все упоминаемые ниже семантики корректны. Другое важное свойство семантики полнота. П. л. Lназ. полной относительно семантики S, если .

Алгебраическая семантика SA состоит из псевдобулевых алгебр, т. е. алгебр вида