DETERMINISTIC SQEMA AND APPLICATION FOR PRE-CONTACT LOGIC

Abstract

SQEMA is a set of rules for finding first-order correspondents of modal formulas, and can be used for proving axiomatic completeness. SQEMA succeeds for the Sahlqvist and Inductive formulas. A deterministic, terminating, but sometimes failing algorithm based on SQEMA for a modal language with nominals, reversed modalities and the universal modality - $ML(T,U)$ - is presented. Deterministic SQEMA finds first-order correspondents, and it can be used to prove di-persistence. It succeeds for the Sahlqvist and Inductive formulas. The axiomatic system for $ML(T,U)$ is shown and its strong completeness is proven. It is shown that adding di-persistent formulas as axioms preserves strong completeness. Deterministic SQEMA is extended for the language of pre-contact logics using a modified translation into $ML(T,U)$. Deterministic SQEMA succeeds for the Sahlqvist class of pre-contact formulas.