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 2 essays across one field — each of them below, with the objects they name alongside it.

Also named here as literal, proof system, refutation, 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

Named alongside it

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

LiteralProof systemRefutationSatisfiabilitySoundnessBranchingDecision procedureNormal formResolutionTableau

All concepts