A logic characterized by the class of connected models with nested domains (Q1264135)

This paper raises interesting questions about limitations of canonical model completeness proofs. QE is a quantified intuitionistic logic with an existence predicate, Q-LC and QE-LC are Q and QE plus an axiom schema: (A\(\to B\vee B\to A)\), and QE-T is QE with an axiom schema: \(\neg A\vee \neg \neg A\). The author's proofs that QE is complete with respect to Kripke E-models and that QE-LC is complete with respect to connected Kripke E-models reveal the dependence upon the language having the E- predicate. So, it remains open whether or not Q-LC is complete with respect to connected Kripke models. The author observes that there is no ``natural'' way to modify the completeness proof for QE-LC to show the completeness of QE-T with respect to directed Kripke E-models.