Positive propositional calculus

A propositional calculus in the language $\{\&,\lor,\supset\}$ 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[edit]