View source for Implicative propositional calculus

<!--
i0503001.png
$#A+1 = 7 n = 0
$#C+1 = 7 : ~/encyclopedia/old_files/data/I050/I.0500300 Implicative propositional calculus
Automatically converted into TeX, above some diagnostics.
Please remove this comment and the {{TEX|auto}} line below,
if TeX found to be correct.
-->

{{TEX|auto}}
{{TEX|done}}

A [[Propositional calculus|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|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 [[#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>