Home » Articole » Articles » Society » Philosophy » Logic » Classical, minimal, and intuitionist logic

Classical, minimal, and intuitionist logic

posted in: Logic 0

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)

The Republic - On Justice (Annotated), by Plato
The Republic – On Justice (Annotated), by Plato

Πολιτεία, published on 375 BC, by Plato (428/427 or 424/423 BC – 348/347 BC) Translation by Benjamin Jowett (1817 – 1893), Published by The Colonial Press in 1901 Special Introduction by William Cranston Lawton (1853 – 1941) Introduction by Nicolae … Read More

not rated $4.99 Select options
Candide
Candide – The best of all possible worlds

Translated and illustrated by Nicolae Sfetcu. A philosophical tale, a story of a journey that will transform the eponymous hero into a philosopher. An important debate on fatalism and the existence of Evil. For a long time Voltaire has been … Read More

not rated $2.99 Select options
Epistemology of experimental gravity - Scientific rationality
Epistemology of experimental gravity – Scientific rationality

The evolution of gravitational tests from an epistemological perspective framed in the concept of rational reconstruction of Imre Lakatos, based on his methodology of research programmes. Unlike other works on the same subject, the evaluated period is very extensive, starting … Read More

not rated $0.00 Select options

Leave a Reply

Your email address will not be published. Required fields are marked *