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 3 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

Named alongside it

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

Proof systemCut eliminationDischargeNatural deductionSubformula propertyBranchingCompletenessRefutationSatisfiabilitySoundnessTableau

All concepts