View source for Implicative propositional calculus

A [[Propositional calculus|propositional calculus]] using only the primitive connective <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i050/i050300/i0503001.png" /> (implication). Examples of an implicative propositional calculus are the complete (or classical) implicative propositional calculus given by the axioms

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i050/i050300/i0503002.png" /></td> </tr></table>

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i050/i050300/i0503003.png" /></td> </tr></table>

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

<table class="eq" style="width:100%;"> <tr><td valign="top" style="width:94%;text-align:center;"><img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i050/i050300/i0503004.png" /></td> </tr></table>

and the same rules of inference. Every implicative formula, that is, a formula only containing the connective <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i050/i050300/i0503005.png" />, 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 <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i050/i050300/i0503006.png" /> of variables, among the formulas with variables in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/i/i050/i050300/i0503007.png" /> there is only a finite number of pairwise inequivalent ones in the positive implicative propositional calculus (see [[#References|[3]]]). There exist undecidable finitely-axiomatizable implicative propositional calculi (see [[#References|[4]]]).

====References====
<table><TR><TD valign="top">[1]</TD> <TD valign="top">  A. Church,   "Introduction to mathematical logic" , '''1''' , Princeton Univ. Press  (1956)</TD></TR><TR><TD valign="top">[2]</TD> <TD valign="top">  J. Łukasiewicz,   A. Tarski,   "Untersuchungen über den Aussagenkalkül"  ''C.R. Soc. Sci. Letters Varsovie, Cl. III'' , '''23'''  (1930)  pp. 30–50</TD></TR><TR><TD valign="top">[3]</TD> <TD valign="top">  A. Diego,   "Sur les algèbres de Hilbert" , Gauthier-Villars  (1966)  ((translated from the Spanish))</TD></TR><TR><TD valign="top">[4]</TD> <TD valign="top">  M.D. Gladstone,   "Some ways of constructing a propositional calculus of any required degree of unsolvability"  ''Trans. Amer. Math. Soc.'' , '''118'''  (1965)  pp. 192–210</TD></TR></table>