Предикатный вариант совместной логики задач и высказываний

Я расскажу про совместную логику задач и высказываний QHC, введённую С. А. Мелиховым. Эта логика объединяет классическую и интуиционистскую предикатные логики. В QHC имеются формулы двух сортов: высказывания (классическая часть) и задачи (интуиционистская часть). Эти два сорта связаны между собой модальностями ? и !. Применив ! к высказыванию p, мы получим задачу !p – «доказать высказывание p». Наоборот, применив ? к задаче α, мы получим высказывание ?α – «задача α имеет решение». В докладе будут построены модели типа Крипке с проверяющими мирами этой логики и показана корректность и полнота логики QHC относительно этого типа моделей. Мы покажем консервативность логики QHC относительно интуиционистской модальной логики QH4 (в некотором смысле двойственной к предикатной логике S4). Наконец, мы покажем, что в интуиционистской части QHC имеют место дизъюнктивное и экзестенциальное свойства.