A Syntactic Characterization of the Gabbay-de Jongh Logics

Skura [12] syntactically characterised intuitionistic propositional logic among all intermediate logics by means of a Lukasiewicz-style refutation system. Another such syntactic characterisation is given by Iemho [5] in terms of admissible rules. Here we oer a bridge between these results. That is to say, we provide sucient conditions under which admissible rules yield a refutation system fully characterising the logic. In particular, we give a characterisation of the Gabbay{de Jongh logics by means of refutation systems employing ideas from admissibility. Lukasiewicz [9] introduced refutation systems as a formal means of reasoning about derivability and non-derivability within the same system. A refutation system inductively denes non-derivability, so in a very real way a refutation system is a proof system for non-provability. Proofs in this system are called \refutations", and when a refutation can be built for a formula we call it refutable, denoted bya . A refutation system is said to be sound (with respect to a certain logic) if all refutable formulae are non-derivable and we call it complete when the converse holds. Whenever the logic at hand comes with semantics and a sound refutation system one can reada as \there exists a counter model of ". The original refutation system given by Lukasiewicz was intended for classical propositional logic (CPC). It consisted of the rules Ax, Subs and MT (modus tollens) as shown below, where ‘ is to be read as derivability within CPC. Bearing in mind that CPC is complete with respect to Boolean algebras one can readily derive both soundness and completeness of the system. Lukasiewicz [10] proposed another refutation system for intuitionistic propositional logic (IPC), which consisted of the rules listed below. Naturally, here‘ is to be read as derivability within IPC. In stating that this system is a complete refutation system for IPC he, in essence, conjectured that IPC is the sole intermediate logic with the disjunction property. The situation turned out to be more subtle, for there are continuum many such intermediate logics [13].