Math 2.0

Mathematical logic and foundations Definition

Intuitionistic logic

Builds on Propositional logicHilbert systemModus ponensLaw of excluded middle

Definition

The formulas of intuitionistic propositional logic are built from propositional variables and ⊥\bot with ∧\land, ∨\lor and →\to. The negation ¬φ\neg\varphi abbreviates φ→⊥\varphi \to \bot. Intuitionistic propositional logic is the set of formulas derivable in the Hilbert system with the following axiom schemes, for all formulas φ\varphi, ψ\psi, χ\chi.

  1. φ→(ψ→φ)\varphi \to (\psi \to \varphi).
  2. (φ→(ψ→χ))→((φ→ψ)→(φ→χ))(\varphi \to (\psi \to \chi)) \to ((\varphi \to \psi) \to (\varphi \to \chi)).
  3. φ∧ψ→φ\varphi \land \psi \to \varphi and φ∧ψ→ψ\varphi \land \psi \to \psi.
  4. φ→(ψ→φ∧ψ)\varphi \to (\psi \to \varphi \land \psi).
  5. φ→φ∨ψ\varphi \to \varphi \lor \psi and ψ→φ∨ψ\psi \to \varphi \lor \psi.
  6. (φ→χ)→((ψ→χ)→(φ∨ψ→χ))(\varphi \to \chi) \to ((\psi \to \chi) \to (\varphi \lor \psi \to \chi)).
  7. ⊥→φ\bot \to \varphi.

The only rule is modus ponens: from φ\varphi and φ→ψ\varphi \to \psi, derive ψ\psi.

Remarks

Adding the scheme φ∨¬φ\varphi \lor \neg\varphi, the law of excluded middle, gives classical propositional logic. Intuitionistic first-order logic adds quantifiers with the usual axioms and rules, again without excluded middle.

Example: φ→¬¬φ\varphi \to \neg\neg\varphi, that is, φ→((φ→⊥)→⊥)\varphi \to ((\varphi \to \bot) \to \bot), is derivable. By the deduction theorem it suffices to derive ⊥\bot from φ\varphi and φ→⊥\varphi \to \bot, which is one step of modus ponens.

Non-example: p∨¬pp \lor \neg p is not derivable for a variable pp. In the Kripke model with worlds u≤vu \le v and pp true only at vv, neither pp nor ¬p\neg p holds at uu, and derivable formulas hold at every world.

Likewise ¬¬p→p\neg\neg p \to p is not derivable, while ¬¬¬p→¬p\neg\neg\neg p \to \neg p is.

Reading path

To understand this page from the ground up, read these 11 pages in order. The foundations come first.

Show the path as a graph
Hilbert system, concept, no evidence levelHilbert systemconceptProposition, concept, no evidence levelPropositionconceptConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionLaw of excluded middle, statement, no evidence levelLaw of excluded middlestatementModus ponens, concept, no evidence levelModus ponensconceptPropositional logic, concept, no evidence levelPropositional logicconceptIntuitionistic logic, definition, no evidence levelIntuitionistic logicdefinition
Each page uses the pages above it. The colour of the bar on a box shows how strong the evidence is, and the box also gives it as text. The list has the same pages.
  • no evidence level
  1. Hilbert system concept
  2. Proposition concept
  3. Conjunction definition
  4. Disjunction definition
  5. Implication definition
  6. Negation definition
  7. Biconditional definition
  8. Law of excluded middle statement
  9. Modus ponens concept
  10. Propositional logic concept
  11. Intuitionistic logic definition

Further reading

  1. Web https://en.wikipedia.org/wiki/Intuitionistic_logic
About this page
Tag52XCYMK0WW
URIm2://52XCYMK0WW
Kinddefinition
WritingW0 stub
MSC03B20, 03F55
DefinesIntuitionistic logic
UsesPropositional logic, Hilbert system, Modus ponens, Law of excluded middle
Changed2 November 2026

Markdown · JSON · Edit on GitHub

What this page needs for W1

  • a source with a locator (0 of 1)

The writing levels say how complete the text of a page is. They do not measure its truth.

What links here

No page links to this page yet.