A Normalized Natural Deduction System for the Logic MC

Abstract

Currently, there is no decidability proof for the sentential logic MC of meaning containment, due it not quite fitting standard semantic or Gentzen methods. This paper presents a normalized Fitch-style natural deduction system for MC, building on one previously published by the author for the neighbouring logic DW, but with modifications due to the presence in MC of Conjunctive Syllogism and the absence of Distribution. Decidability is achieved for MC through the use of the Subformula Property associated with normalization and the identity between the depth of a subformula in the final formula under test and the depth of subproof in which such a subformula can be located in the normalized natural deduction proof.