Matpic
mathematics, in pictures
Concept

Completeness

The property of a proof system that every statement true in all models of its axioms can be derived in it. With soundness it makes derivability and truth-in-every-model the same relation, which is what makes searching for a derivation worth doing.

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

A tableau for ((p → q) ∧ (q → r)) → (p → r). A branching tree of formulas, each branch ending in a contradiction or in a description of a counterexample.

The tree that closes

To prove a formula, assume it false and take it apart. Every branch ends in a contradiction, or one of them describes exactly how it could have been false — and either way the tree is the answer, drawn.

logic · Proof systems A resolution refutation of four clauses on three variables. A derivation tree: the given clauses at the top, each later clause obtained by cancelling one variable between two clauses above it, ending in the empty clause.

A proof with one rule

Two clauses that disagree about exactly one variable can be combined into a third that forgets it; repeat, and if the clauses cannot all be true the empty clause eventually appears — a complete proof system with a single move.

logic · Resolution A model whose worlds are sets of sentences. Worlds labelled by which of a fixed finite set of formulas they accept, with an arrow wherever every boxed formula accepted by one has its inside accepted by the other.

Worlds built out of sentences

A Kripke model needs worlds, and nothing so far has said where worlds come from. They can be made of the syntax: a world is a set of formulas it commits to, one world sees another when the boxed commitments line up, and in the model that results every formula is true exactly where it was assumed.

logic · Modal logic A chain of 18 worlds, and the 3 the formulas can tell apart. A row of 18 circles for the worlds of the model, shaded by which of the 3 classes each falls into, above the quotient model's 3 worlds with the arrows the collapse gives them.

How many worlds a formula can need

A modal formula can be true in a model with infinitely many worlds. It can also be true in a small one — and the small one is built from the large one by throwing away every distinction the formula was never able to make.

logic · Modal logic 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 lemma, and the proof that never mentions one. Two derivations of ((p → q) ∧ (q → r)) → (p → r) compared: the cut-free one uses 8 nodes and only subformulas of the goal, and the one through a lemma uses 21 and mentions a formula the goal does not contain.

A lemma, and the proof that never mentions one

Proving something by first proving a lemma is what makes mathematics readable, and it is exactly what makes a proof system impossible to search — because the lemma can be any formula at all. Gentzen proved the step can always be removed, and the removal is not free.

logic · Proof systems Closed after 3 uses of the universal. The Herbrand expansion of a first-order question at 5 stages, with the number of remaining models at each. It reaches nought after 3 instantiations.

The instance that has to be guessed

Every rule of a propositional tableau replaces a formula by shorter ones, which is why it stops. The rule for a universal claim does not replace it — it keeps it and adds an instance — and one word changing turns a decision procedure into a search that may run forever.

logic · Proof systems A countable structure grown by adding witnesses. Stages of a structure built from 0 and 1 by adding sums, products, negatives and roots of quadratics: 2, 4, 12, 158 elements between −3 and 3.

A countable field that passes for the line

The real numbers are uncountable, and every first-order sentence about their addition, multiplication and order is also true of a countable field inside them — the real algebraic numbers. Löwenheim and Skolem showed this is no quirk of the reals: every theory with an infinite model has a countable one, including set theory, which then contains sets it calls uncountable.

logic · Models Whole-number points in a strip, and the shadow they cast. The lattice points satisfying 2x ≤ 5y ≤ 2x + 1 for x from 0 to 30, and their projection onto the x-axis, which repeats every 5.

Arithmetic with addition alone

Over the real numbers, a quantifier's shadow is described by inequalities. Over the whole numbers with addition and multiplication, a shadow can be any set a computer can list. In between lies arithmetic with addition and no multiplication, and there the shadows are always the same kind of thing: a finite exception, then a pattern that repeats. The whole numbers made from coins worth 6, 9 and 20 are every number from 44 on; the squares, which need multiplication, never repeat at all.

logic · Quantifiers Six formulas on the interval of truth values. Graphs on [0, 1] of six one-variable formulas of Łukasiewicz logic, each a zigzag of whole-number slopes with values 0 or 1 at the ends.

The zigzags a formula can draw

Let truth be any number from 0 to 1, and Łukasiewicz's connectives turn every formula in one variable into a graph. Every graph that appears is a zigzag of straight pieces with whole-number slopes, ending at 0 or 1 — and McNaughton proved in 1951 that every such zigzag appears. A logic of degrees of truth turns out to be a theory of piecewise-linear functions with integer coefficients.

logic · Non classical logic

Named alongside it

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

Decision procedureProof systemSoundnessTableauQuantifierSatisfiabilityBranchingKripke modelLiteralModal logicModelNatural deduction

All concepts