Concept

Constructive proof

An argument that establishes something exists by exhibiting one, rather than by ruling out its absence. It is the stronger of the two: it settles existence and hands over an example, at the cost of usually being harder to find.

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

A set, its negation, and its double negation. Four bars on one number line showing an open set, its negation, their union, and the double negation.

The middle that is not excluded

Either it is raining or it is not. Drop that as an axiom and what is left is still a logic — one with models made of open sets and of stages of knowledge, in which a set and its negation between them miss the boundary.

logic · Non classical logic

One matching that is not stable, and all 24 counted by blocking pairs. An unstable matching with its blocking pair ringed and both members' rankings marked, above an exhaustive census of every matching of the instance by how many blocking pairs it has.

Nobody has a reason to run away

A matching is stable when no two people on opposite sides would both rather have each other than what they have — a condition that names nothing to build and everything to rule out. The surprise is that something always satisfies it, however perverse the rankings are made.

applied · Stable matching

Gluing two countermodels: p ∨ ¬p. Two small Kripke models, each refuting one half of a disjunction, and the model made by placing both above a new first stage, at which neither half is forced.

A proof that says which half

Classical logic proves p ∨ ¬p without any idea which half is true. The constructive system never does that: whenever it proves a disjunction, it proves one of the two halves. The reason is a picture — two countermodels placed side by side above a new first stage that forces neither — and the logics between the two lose the property exactly when their pictures are not allowed to be glued.

logic · Non classical logic

Named alongside it

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

Excluded middle Heyting algebra Intuitionistic logic Kripke model Bijection Blocking pair Counterexample Deferred acceptance Disjunction property Double negation Exhaustive search Existence proof

All concepts