Matpic
mathematics, in pictures
Concept

Implication

The logical connective written A → B, false only when A holds and B fails. It is proved by assuming A and deriving B, and used by combining it with a proof of A to obtain B, the step called modus ponens.

Named by 4 essays across one field — each of them below, with the objects they name alongside it.

7 steps and 3 withdrawn assumptions. A natural-deduction derivation of (p → q) → (¬q → ¬p). Each horizontal bar is one inference, named on its right; the bracketed formulas are assumptions, and each is withdrawn at the step that names it.

The assumption a proof pays back

A tableau assumes the opposite once and takes it apart. Natural deduction assumes things freely, uses them, and then withdraws them — and the withdrawal is what turns a derivation of a consequence into a proof of an implication.

logic · Proof systems A derivation of ((p → q) ∧ (q → r)) → (p → r), and the term it is. A natural-deduction derivation of ((p → q) ∧ (q → r)) → (p → r) with a lambda term written under each formula. The whole derivation is the term λh₁. λh₂. (π₂ h₁) ((π₁ h₁) h₂), and at every node the type of the term is the formula the derivation proves there.

Every derivation is a term

Write a variable for each assumption, an abstraction where one is discharged, and an application where an implication is used, and a natural-deduction derivation becomes a term. The formula it proves is the term's type, and checking the one is checking the other. A detour in the proof — a lemma introduced and at once used — is a term that simplifies, and simplifying it is removing the detour.

logic · Proof systems A implies B, and r ∨ s sits between them. A = ((p ∨ q) ∧ (p → r)) ∧ (q → s) implies B = (r ∨ s) ∨ t. A resolution refutation of A with the negation of B yields the interpolant r ∨ s. It uses only the shared atoms r, s, follows from A and implies B, and lies between the strongest and weakest interpolants.

The sentence between a premise and its consequence

When one formula implies another, something sits between them written only in the words the two have in common: a sentence the first implies and that implies the second. A refutation of the first together with the denial of the second hands such a sentence over, and every possible one lies between a strongest and a weakest that can be computed outright.

logic · Proof systems Carroll's babies and crocodiles, on four ellipses. Four overlapping ellipses labelled with the four classes of a sorites, the regions emptied by its premises shaded, and the regions its conclusion requires to be empty outlined.

The conclusion is what survives the erasing

Lewis Carroll's puzzles give three premises about four classes — babies, logical people, the despised, crocodile-managers — and ask what follows. Draw all four, shade what the premises rule out, then erase the classes the conclusion is not about: a region survives as empty only if everything above it was. What is left is the conclusion, and erasing a class turns out to be exactly one step of resolution.

logic · Class diagrams

Named alongside it

The objects these essays reach for when they reach for this one.

Proof systemCut eliminationDischargeNatural deductionSatisfiabilitySubformula propertyBoolean functionBranchingCompletenessExhaustive searchRefutationResolution

All concepts