The D-Completeness of T→

  • R. K. Meyer Automated Reasoning, Australian National University
  • M. W. Bunder School of Mathematics and Applied Statistics, University of Wollongong

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.

Author Biographies

R. K. Meyer, Automated Reasoning, Australian National University
M. W. Bunder, School of Mathematics and Applied Statistics, University of Wollongong
Published
2010-09-22
How to Cite
MEYER, R. K.; BUNDER, M. W.. The D-Completeness of T→. The Australasian Journal of Logic, [S.l.], v. 8, sep. 2010. ISSN 1448-5052. Available at: <https://ojs.victoria.ac.nz/ajl/article/view/1810>. Date accessed: 23 may 2019. doi: https://doi.org/10.26686/ajl.v8i0.1810.