Simple Tableaus for Simple Intuitionistic Logics

This paper continues earlier work and extends it to an intuitionistic setting. Kripke frames are used to semantically define a family of intuitionistic-like logics for which the “local” part of the truth definition is supplied by many-valued logics whose semantics are algebraically simple and natural. A uniform tableau system is given and soundness and completeness are proved. The tableau connection entails that the semantic family collectively determines just four logics, intuitionistic logic itself, and intuitionistic-like versions of FDE, K3, and LP. These, apparently, are new logics, and are of natural interest. For instance, all have the disjunction property, and standard double negation embeddings are applicable. In addition, intuitionistic analogues of ST (strict-tolerant logic) and TS (tolerant-strict) logics are defined, and shown to have the same relationships to intuitionistic logic that the usual ST and TS have to classical logic.