Matpic
mathematics, in pictures
Series

Non classical logic — the series

5 essays on one idea, from the one that introduces it to the one that assumes the rest.
  1. 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.

    part 1 · logic
  2. 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.

    part 2 · logic
  3. 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.

    part 3 · logic
  4. 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.

    part 4 · logic
  5. 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.

    part 5 · logic

All series