The D-Completeness of T→

Authors

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

DOI:

https://doi.org/10.26686/ajl.v8i0.1810

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.

Downloads

Download data is not yet available.

Author Biographies

R. K. Meyer, Automated Reasoning, Australian National University

M. W. Bunder, School of Mathematics and Applied Statistics, University of Wollongong

Downloads

Published

2010-09-22