Classical, minimal, and intuitionist logic

The axioms and rules of propositional calculus for the classical logic induce the proposition p ∨ ¬p, called the principle of excluded middle, the proposition ¬¬p → p, called elimination of double negation and the proposition ((p → q) → p) → p called Peirce’s law. This logic is based on the principle that a property P is necessarily true or false. It is one of the pillars of the so-called formalist position adopted by Hilbert and others. However, this position which implies that there are demonstrations which do not construct the object satisfying the proven proposition has been called into question by several mathematicians, the best known of whom is Brouwer, leading to the subsequent creation of intuitionist logic.

There are variants of non-classical logic, notably the minimal logic of Ingebrigt Johansson (1936) and the intuitionistic logic of Heyting (1930). The primitive connectives are →, ∧, ∨ and ¬. These variants differ from each other in the choice of axioms they use.

Absolute logic

Absolute logic uses the following axioms relating to implication, conjunction and disjunction. It does not deal with negation.

Axioms of implication → (these are the first two axioms of classical logic):

• ax.1: p → ( q → p )
• ax.2: ( p → ( q → r ) ) → ( ( p → q ) → ( p → r ) )

Axioms of conjunction ∧:

• ax.3: ( p ∧ q ) → p
• ax.4: ( p ∧ q ) → q
• ax.5: ( p → q ) → ( ( p → r ) → ( p → ( q ∧ r ) ) )

Axioms of the disjunction ∨ , (duals of the previous ones):

• ax.8: p → ( p ∨ q )
• ax.9: q → ( p ∨ q )
• ax.10: ( p → r ) → ( ( q → r ) → ( ( p ∨ q ) → r ) )

The set of theorems of this logic is strictly included in the set of theorems of classical logic which do not use negation. It is impossible for example to prove there the formula p ∨ (p → q) or Peirce’s law ((p → q) → p) → p.

Positive logic

If we add to axioms ax.1 to ax.8 the following axiom:

• ax.9: p ∨ ( p → q )

we get the positive logic. The set of theorems of this logic is identical to the set of theorems of classical logic which do not use negation.

Minimal logic

If we add to axioms ax.1 to ax.8 the following two axioms, relating to negation:

• ax.10: ¬p → (p → ¬q)
• ax.11: (p → ¬p) → ¬p

we obtain the minimal logic. The first axiom defines the behavior of logic vis-à-vis a contradiction. The second axiom expresses that, if p implies its own negation, then p is invalid.

Intuitionist logic

The only difference between intuitionist logic and minimal logic concerns the axiom ax.10 which we replace by:

• ax.12: ¬p → (p → q)

In the presence of a proposition and its negation, the three logics, classical, intuitionist and minimal, all three conclude in a contradiction ⊥. But the difference lies in how we use this contradiction:

• Classical logic deduces from ¬P → ⊥ the fact that P is true (reductio ad absurdum).
• Intuitionist logic deduces from a contradiction that every proposition is demonstrable. From ¬P → ⊥, it deduces the validity of ¬¬P, a property weaker than P.
• Minimal logic deduces from a contradiction that any negation of a proposition is demonstrable, which is weaker than what intuitionist logic proposes.

Minimal logic and intuitionistic logic both have the proposition ¬(p ∧ ¬p) as their theorem. On the other hand, p ∨ ¬p is not a theorem of these logics.

Similarly, they allow to prove p → ¬¬p but not the converse. On the other hand, they make it possible to demonstrate the equivalence between ¬p and ¬¬¬p. Finally, the proposition (¬p ∨ q) → (p →q) is a theorem of intuitionistic logic, but not a theorem of minimal logic.

Glivenko proved in 1929 that p is a theorem of classical propositional calculus if and only if ¬¬p is a theorem of intuitionistic propositional calculus. This result does not extend if we replace “intuitionistic” with “minimal”. It also does not apply to predicate calculus; a translation is however possible, but depends on the structure of the formulas.

Finally, to have a proof of p ∨ q in intuitionistic logic, one needs either a proof of p or a proof of q, whereas in classical logic, a proof of ¬(¬p ∧ ¬q) suffices.

Quantified propositional calculus

We can introduce the quantifiers ∃ (there exists) and ∀ (whatever) to quantify the propositions (which is to be distinguished from the quantification of the calculus of predicates). Thus, for examples, we will have as valid formulas of the quantified propositional calculus, also called second-order propositional calculus:

• ∀p (⊥ → p): For any proposition, the false implies it;
• ∀p (p → T): The true is implied by every proposition;
• ∃p (p ∨ q): Take p ↔ ¬q (in classical logic) or p ↔ T (more generally), for examples.

(Includes texts from Wikipedia translated and adapted by Nicolae Sfetcu)