THE NATURAL DEDUCTION

Proof in the shape reasoning actually takes: introduce a connective, then eliminate it. Assumptions are made, used, and discharged. The engine below is a real natural-deduction proof checker for propositional logic — rendered, not quoted.

source Gentzen, Untersuchungen über das logische Schließen (1935), Mathematische Zeitschrift 39, 176–210 · doi:10.1007/BF01201353

Blue Team · builds & defends
3

The Model

A proof is a tree of rule applications. Leaves are assumptions; each internal node names a rule that derives its formula from the formulas above it.

Rules come in pairs per connective:

→ introduction: discharge [A], derive B ⇒ A→B → elimination: from A→B and A ⇒ B (modus ponens) ∧ intro/elim, ∨ intro/elim, ¬ intro/elim

A formula is proved only when the tree is closed — every assumption has been discharged — and the proved formula is a tautology.

5

The Lineage

Intro-and-elim is Gentzen's frame. the-syllogism handled Aristotle's fixed forms; this sphere generalises the same discipline to full propositional logic with arbitrary connectives and nested assumptions.

The proof term here (a tree of rule nodes) is exactly the computational content read off by the-curry-howard — this is its logic half.

7

The Witness

Live re-check. Recomputes rule soundness over full truth tables and re-validates the proof tree on every render.

The Machine
4

Data In in ↓

Rule set — 8 sound inference rules (intro/elim for ∧ ∨ → ¬).

Goal — the hypothetical syllogism, a tautology:

(A→B) → ((B→C) → (A→C))

Proof term — a tree using three assumptions [A→B]u, [B→C]v, [A]w, two →E steps, three →I discharges.

↓
0

The Panel LIT

The checker walks the tree, verifies each node against its rule, tracks open assumptions, and confirms the goal is a tautology by exhaustive truth table.

↓
8

Data Out out ↓

Red Team · attacks & breaks
1

The Adversary WALL

This checker is propositional only. It cannot express quantifiers — first-order natural deduction (∀I with its eigenvariable side-condition, ∃E) is beyond it.

AMBER — per-rule soundness is checked, but that is not the full meta-theorem. Global soundness/completeness (Gentzen's cut-elimination result) is assumed here, not reproven.

AMBER — the rules are classical. Drop double-negation elimination and you get intuitionistic logic, where some classical tautologies are unprovable. That boundary is real.

2

The Graveyard

  • “If the premises look plausible, the conclusion is proved.” Validity is truth-preservation under every valuation — not plausibility.
  • “Affirming the consequent is a valid rule.” Unsound: from A→B and B you cannot infer A. Falsified at A=false, B=true.
  • “A proof of a theorem may leave assumptions standing.” Assumptions may be used, but every one must be discharged; an open leaf means the tree is not closed.
6

The Tamper

Planted void (disclosed): add affirming the consequent (A→B, B ⊢ A) to the allowed rules. An invalid formula becomes “provable”. The Witness (7) recomputes soundness and catches it live.