View source for Positive propositional calculus

A [[Propositional calculus|propositional calculus]] in the language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739501.png" /> specified by the following 8 axiom schemes:

<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/p/p073/p073950/p0739502.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/p/p073/p073950/p0739503.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/p/p073/p073950/p0739504.png" /></td> </tr></table>

and the [[Modus ponens|modus ponens]] derivation rule. This calculus contains the part of the intuitionistic propositional calculus I (see [[Intuitionism|Intuitionism]]) that is not dependent on negation: Any propositional formula not containing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739505.png" /> (negation) is derivable in the positive propositional calculus if and only if it is derivable in I. One obtains the calculus I if one adds two axiom schemes to the positive propositional calculus:

1) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739506.png" /> (antecedent negation law),

2) <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739507.png" /> (reductio ad absurdum law).

To derive I, instead of 2) one can take the weaker scheme:

2') <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/p/p073/p073950/p0739508.png" /> (law of partial reductio ad absurdum).

See also [[Implicative propositional calculus|Implicative propositional calculus]].

====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">  D. Hilbert,   P. Bernays,   "Grundlagen der Mathematik" , '''1–2''' , Springer  (1968–1970)</TD></TR></table>