Аннотация:Решение проблемы разрешимости для матричных модальных логик
Solution of the decition problem for matrix model logic
Ивлев Ю.В.
Московский государственный университет им. М.В. Ломоносова, г. Москва
E-mail: ivlev.logic@yandex.ru
Разрешимость исчислений является следствием доказательства метатеорем об их семантической полноте. Последнее доказательство осуществляется разработанным автором тезисов методом, являющимся обобщением известного метода Кальмара. По набору значений пропозициональных переменных образуется множество гипотез следующим образом. Пусть множество элементов матрицы есть {n,c,i}, а выделенное значение - n. Пусть переменной p, входящей в формулу D, приписано значение с. Образуем формулу, содержащую только указанную переменную и принимающую выделенное значение при указанном значении этой переменной. Так делается для каждой переменной, входящей в D. Пусть при данном наборе значений переменных, входящих в рассматриваемую формулу, эта формула принимает значение i. Образуем из D формулу, принимающую выделенное значение при рассматриваемом наборе значений входящих в нее переменных. Доказываем лемму о том, что для каждого множества гипотез, образованных из переменных указанным способом, следует формула, образованная из D как указано. Далее доказываем, что если формула является общезначимой, то она следует из образованных из D формул, а затем доказываем, что все гипотезы устранимы, т.е. формула D является теоремой. Проблема разрешимости решена. Разрешимость может быть использована при технических приложениях матричных многозначных логик. Описанное обобщение метода Кальмара применимо к квазиматричным многозначных логикам с конечным числом значений.
Исследование выполнено при финансовой поддержке РГНФ в рамках научного проекта № 15-03-00372.