Concept

Double negation

Denying a denial, which classically returns the original statement and constructively does not. In a model made of open sets the first negation loses the boundary and the second hands it back, so the double negation is larger than what it started from.

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

Also named here as excluded middle, heyting algebra, intuitionistic logic, open set, topology of 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

Named alongside it

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

Excluded middle Heyting algebra Intuitionistic logic Open set Topology of logic Kripke model Constructive proof Decidability Exhaustive search Lattice

All concepts