Positive propositional calculus
A propositional calculus in the language specified by the following 8 axiom schemes:
A\supset(B\supset A),\quad(A\supset(B\supset C))\supset((A\supset B)\supset(A\supset C)),
A\&B\supset A,\quad A\&B\supset B,\quad A\supset(B\supset A\&B),
A\supset A\lor B,\quad B\supset A\lor B,\quad(A\supset C)\supset((B\supset C)\supset(A\lor B)\supset C),
and the modus ponens derivation rule. This calculus contains the part of the intuitionistic propositional calculus I (see Intuitionism) that is not dependent on negation: Any propositional formula not containing \neg (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) \neg A\supset(A\supset B) (antecedent negation law),
2) (A\supset B)\supset((A\supset\neg B)\supset\neg A) (reductio ad absurdum law).
To derive I, instead of 2) one can take the weaker scheme:
2') (A\supset\neg A)\supset\neg A (law of partial reductio ad absurdum).
See also Implicative propositional calculus.
References
[1] | A. Church, "Introduction to mathematical logic" , 1 , Princeton Univ. Press (1956) |
[2] | D. Hilbert, P. Bernays, "Grundlagen der Mathematik" , 1–2 , Springer (1968–1970) |
Positive propositional calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Positive_propositional_calculus&oldid=32857