Matpic
mathematics, in pictures
Concept

Proof system

A fixed stock of axioms and inference rules together with a definition of what counts as a derivation. Its value is measured twice: whether everything true is derivable in it, and how long the derivations are forced to be.

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

Also named here as soundness — the same set of essays touches all of them, so they are one junction rather than several.

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

Named alongside it

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

CompletenessSoundnessDecision procedureLiteralRefutationSatisfiabilityBranchingConsistencyKripke modelModal logicModelNormal form

All concepts