The D-Completeness of T→

Abstract

A Hilbert-style version of an implicational logic can be represented by a set of axiom schemes and modus ponens or by the corresponding axioms, modus ponens and substitution. Certain logics, for example the intuitionistic implicational logic, can also be represented by axioms and the rule of condensed detachment, which combines modus ponens with a minimal form of substitution. Such logics, for example intuitionistic implicational logic, are said to be D-complete. For certain weaker logics, the version based on condensed detachment and axioms (the condensed version of the logic) is weaker than the original. In this paper we prove that the relevant logic T→, and any logic of which this is a sublogic, is D-complete.