Intuitionistic propositional calculus

2020 Mathematics Subject Classification: Primary: 03B20 [MSN][ZBL]

A logical calculus describing rules for the derivation of propositions that are valid from the point of view of intuitionism. The generally accepted formulation of intuitionistic propositional calculus was proposed by A. Heyting in 1930. Its fundamental difference from classical propositional calculus is in the replacement of the law of the excluded middle (or the law of double negation) by the weaker contradiction principle

$$A\supset(\neg A\supset B).$$

A common variant of intuitionistic propositional calculus is formulated as follows. Let $A,B,C$ be arbitrary formulas in the logical language considered. The axioms of the calculus are the following formulas:

1) $A\supset(B\supset A)$;

2) $(A\supset B)\supset((A\supset(B\supset C))\supset(A\supset C))$;

3) $A\supset(B\supset A\land B)$;

4) $A\land B\supset A$;

5) $A\land B\supset A$;

6) $A\supset A\lor B$;

7) $B\supset A\lor B$;

8) $(A\supset C)\supset((B\supset C)\supset(A\lor B\supset C))$;

9) $(A\supset B)\supset((A\supset\neg B)\supset\neg A)$;

10) $A\supset(\neg A\supset B)$.

The only derivation rule of intuitionistic propositional calculus is the rule of modus ponens: If formulas $A$ and $A\supset B$ are derivable, then $B$ is derivable.

Every derivable formula of this calculus is valid from the intuitionistic point of view; the problem of completeness of the calculus described is more subtle. Intuitionistic propositional calculus is complete, e.g., with respect to algebraic semantics, the Kripke and Beth models, but it is incomplete with respect to the recursive realizability interpretation of Kleene; see also Constructive propositional calculus.

For references, see Intuitionism.