Intuitionistic/Constructive logic

\\frac{A \\quad B}{A \\land B} & & (\\land\\text{-intro}) \\\\ \\\\

• Inference rules

  • Conjunction

    $$\begin{array}{ccc}\frac{AB}{A\wedge B}& & (\wedge \text{-intro})\\ & & \\ \frac{A\wedge B}{A}& & (\wedge {\text{-elim}}_1)\\ & & \\ \frac{A\wedge B}{B}& & (\wedge {\text{-elim}}_2)\end{array}$$

  • Disjunction

    $$\begin{array}{ccc}\frac{A}{A\vee B}& & (\vee {\text{-intro}}_1)\\ & & \\ \frac{B}{A\vee B}& & (\vee {\text{-intro}}_2)\\ & & \\ \frac{A\vee BA⊢CB⊢C}{C}& & (\vee \text{-elim})\end{array}$$

  • Implication

    $$\begin{array}{ccc}\frac{A⊢B}{A\to B}& & (\to \text{-intro})\\ & & \\ \frac{A\to BA}{B}& & (\to \text{-elim})\end{array}$$

  • Universal quantification

    $$\begin{array}{ccc}\frac{P(x)x\text{ fresh}}{\forall x.P(x)}& & (\forall \text{-intro})\\ & & \\ \frac{\forall x.P(x)}{P(t)}& & (\forall \text{-elim})\end{array}$$

  • Existential quantification

    $$\begin{array}{ccc}\frac{P(t)}{\exists x.P(x)}& & (\exists \text{-intro})\\ & & \\ \frac{\exists x.P(x)P(y)⊢Cy\text{ fresh}}{C}& & (\exists \text{-elim})\end{array}$$

  • Negation

    $$\begin{array}{ccc}\frac{A⊢\perp }{\neg A}& & (\neg \text{-intro})\\ & & \\ \frac{A\neg A}{\perp }& & (\neg \text{-elim})\end{array}$$

  • Absurdity

    $$\frac{\perp }{A}(\perp \text{-elim})$$

Pitfall. The rules define which derivations are valid. They say nothing about meaning-that is the role of an interpretation such as Brouwer-Heyting-Kolmogorov (BHK) interpretation.