Concept

Heyting algebra

A lattice with an operation standing in for implication, taking the largest element whose meet with the antecedent lies below the consequent. The open sets of any space form one, and the constructive propositional logic proves exactly what holds in every such structure.

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

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

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

4 axioms against 4 finite algebras. A table of candidate axioms against finite Heyting algebras built from small orders, marking which algebras validate which axiom at every valuation.

Not one step but a continuum

Classical logic is the constructive system plus one axiom, which makes it sound as though there are two logics and one gap. There are uncountably many logics in that gap, each one a class of algebras, and the smallest separations between them fit in five elements.

logic · Non classical logic

The smallest algebra that refutes each formula. A table of formulas against the smallest finite Heyting algebra refuting each, found by searching every order on a few points, with the formulas no such algebra refutes marked.

Refutable in something small

A formula that is not a theorem of the constructive system fails in some finite algebra, and the algebra can be found by search. That single property is what makes the propositional logic decidable — and the predicate version loses the property and the decidability with it.

logic · Non classical logic

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

Which chains of truth values validate Gödel's disjunctions. A grid of Gödel's pigeonhole formulas in m letters against chains of n truth values, marking which chains validate which formula, forming a staircase where m exceeds n.

No table of truth values is enough

Two truth values decide classical logic. Gödel asked in 1932 whether some longer list of values could decide the constructive system, and answered with a pigeonhole: with n values, some two of n + 1 statements must share one, so a formula saying exactly that holds in every n-valued table and is not a theorem. The chains of truth values then descend forever, and what they share is a logic of its own — the logic of the real interval.

logic · Non classical logic

Named alongside it

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

Intuitionistic logic Excluded middle Double negation Kripke model Open set Topology of logic Constructive proof Disjunction property Exhaustive search Chain Decidability Lattice

All concepts