Matpic
mathematics, in pictures
Concept

Finite model property

The property of a logic that every sentence with a model has a finite one. With a bound on the size needed, it turns the question of whether a sentence is satisfiable into a search that is certain to end.

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

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 A smallest model of ∀x (Ax → ∃y (By ∧ ¬Cy)) ∧ ∃x (Ax ∧ Cx) ∧ ∀x (Bx → ¬Ax). Three overlapping circles with some regions shaded as empty and a single dot in each occupied region, forming a model of a sentence of monadic first-order logic.

One thing in each region is enough

Give first-order logic its full apparatus of nested quantifiers but only one-place predicates, and every question about truth is still settled by the regions of a diagram. A predicate cannot tell apart two things in the same region, so no model ever needs more than one thing per region — and with three predicates there are only 255 models to try.

logic · Class diagrams

Named alongside it

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

Decision procedureBisimulationCompletenessEquivalence relationExhaustive searchKripke modelModal logicModelQuantifierQuotientSatisfiabilityVenn diagram

All concepts