Math 2.0

Mathematical logic and foundations Definition

Natural deduction

Builds on Propositional logicLogical connective

Definition

Consider formulas of propositional logic with the connectives ∧\land, ∨\lor, →\to and the constant ⊥\bot for falsity; ¬φ\neg \varphi abbreviates φ→⊥\varphi \to \bot. A natural deduction derivation is a finite tree of formulas. Each leaf is an assumption, and each inner node follows from its children by one of these rules:

  1. ∧\land-introduction: from φ\varphi and ψ\psi, infer φ∧ψ\varphi \land \psi. ∧\land-elimination: from φ∧ψ\varphi \land \psi, infer φ\varphi, and also ψ\psi.
  2. ∨\lor-introduction: from φ\varphi, infer φ∨ψ\varphi \lor \psi and ψ∨φ\psi \lor \varphi.
  3. ∨\lor-elimination: from φ∨ψ\varphi \lor \psi, a derivation of χ\chi from φ\varphi, and one of χ\chi from ψ\psi, infer χ\chi, discharging φ\varphi and ψ\psi.
  4. →\to-introduction: from a derivation of ψ\psi from the assumption φ\varphi, infer φ→ψ\varphi \to \psi, discharging φ\varphi.
  5. →\to-elimination, or modus ponens: from φ\varphi and φ→ψ\varphi \to \psi, infer ψ\psi.
  6. ⊥\bot-elimination: from ⊥\bot, infer any formula φ\varphi.
  7. Reductio ad absurdum: from a derivation of ⊥\bot from the assumption ¬φ\neg \varphi, infer φ\varphi, discharging ¬φ\neg \varphi.

A discharged assumption is no longer open. One writes Γ⊢φ\Gamma \vdash \varphi if some derivation has root φ\varphi and all its open assumptions in Γ\Gamma.

Remarks

A derivation of ⊢φ∧ψ→ψ∧φ\vdash \varphi \land \psi \to \psi \land \varphi: assume φ∧ψ\varphi \land \psi. By ∧\land-elimination get ψ\psi and φ\varphi, and by ∧\land-introduction get ψ∧φ\psi \land \varphi. Then →\to-introduction discharges the assumption, so no open assumption remains. The tree with the single node pp is a derivation of pp, but only from the open assumption pp; it does not show ⊢p\vdash p. Without rule 7, the system is natural deduction for intuitionistic logic; with it, the system is classical. Quantifier rules extend the system to predicate logic.

Reading path

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

Show the path as a graph
Logical connective, concept, no evidence levelLogical connectiveconceptProposition, concept, no evidence levelPropositionconceptConjunction, definition, no evidence levelConjunctiondefinitionDisjunction, definition, no evidence levelDisjunctiondefinitionImplication, definition, no evidence levelImplicationdefinitionNegation, definition, no evidence levelNegationdefinitionBiconditional, definition, no evidence levelBiconditionaldefinitionPropositional logic, concept, no evidence levelPropositional logicconceptNatural deduction, definition, no evidence levelNatural deductiondefinition
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. Logical connective concept
  2. Proposition concept
  3. Conjunction definition
  4. Disjunction definition
  5. Implication definition
  6. Negation definition
  7. Biconditional definition
  8. Propositional logic concept
  9. Natural deduction definition

Further reading

  1. Web https://en.wikipedia.org/wiki/Natural_deduction
About this page
TagPAQ4ZX2TX1
URIm2://PAQ4ZX2TX1
Kinddefinition
WritingW0 stub
MSC03F03, 03B05
DefinesNatural deduction
UsesPropositional logic, Logical connective
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.