# Implicative propositional calculus

A propositional calculus using only the primitive connective \$ \supset \$( implication). Examples of an implicative propositional calculus are the complete (or classical) implicative propositional calculus given by the axioms

\$\$ p \supset ( q \supset p ) ,\ \ ( ( p \supset q ) \supset \ ( ( q \supset r ) \supset \ ( p \supset r ) ) ) , \$\$

\$\$ ( ( p \supset q ) \supset p ) \supset p \$\$

and the rules of inference: modus ponens and substitution; another example is the positive implicative propositional calculus given by the axioms

\$\$ p \supset ( q \supset p ) ,\ \ ( p \supset ( q \supset r ) ) \supset \ ( ( p \supset q ) \supset \ ( p \supset r ) ) \$\$

and the same rules of inference. Every implicative formula, that is, a formula only containing the connective \$ \supset \$, is deducible in complete (or positive) implicative propositional calculus if and only if it is deducible in classical (respectively, intuitionistic) propositional calculus. For any finite set \$ V \$ of variables, among the formulas with variables in \$ V \$ there is only a finite number of pairwise inequivalent ones in the positive implicative propositional calculus (see ). There exist undecidable finitely-axiomatizable implicative propositional calculi (see ).

How to Cite This Entry:
Implicative propositional calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Implicative_propositional_calculus&oldid=47319
This article was adapted from an original article by S.K. Sobolev (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article