Generator

A set, its negation, and its double negation

A generator in the logic library, called 25 times across 5 essays. Below: what it draws with nothing chosen and at each mode an essay asks for, what it checks while drawing, and everywhere it is used.

opens is one function. Everything below came out of it during this build, at parameters taken from the essays rather than invented for this page — so a figure here is the same figure a reader meets in an essay, and if the generator changes, this page changes with it.

With nothing chosen

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.

Gluing two countermodels: p ∨ ¬p

Which logics survive gluing

Which chains of truth values validate Gödel's disjunctions

Gödel's disjunction in 4 letters, refuted in a chain of 4

The smallest chain of truth values refuting each formula

What it checks while it draws

Collected by running the family and recording what it asserted, not written here. The count is how many separate times the claim was put to the test while these drawings were made.

the 2-chain validates G2 exactly when 2 > 2 ×30
G3 holds in the 2-chain and fails in the 3-chain ×5
an algebra of 2 elements validates Gödel's disjunction in 3 letters ×4
¬¬¬p → ¬p holds in every algebra searched ×1
¬p → q ∨ r ⟹ (¬p → q) ∨ (¬p → r) holds in every algebra searched ×1
a formula that survives three values fails at four ×1
a set is contained in its double negation ×1
and fails under Łukasiewicz's ×1
and here it is strictly contained — the punched-out points come back ×1
and it keeps rising, so the classes are not exhausted by short formulas ×1
and so does double-negation elimination ×1
and the value really is not the top ×1
between one and four points are punched out ×1
both models are chain frames and the glued one is not ×1
both models are one-top frames and the glued one is not ×1
collapsing the top two values respects implication ×1
contraction holds under Gödel's implication ×1
every element sits below its double negation ×1
every glued frame is a frame of the constructive system ×1
every punched-out point is inside the set ×1
every smaller algebra validates (p → q) ∨ (q → p) ×1
every smaller algebra validates ¬¬p → p ×1
every smaller algebra validates ¬p ∨ ¬¬p ×1
every smaller algebra validates p ∨ ¬p ×1
excluded middle fails somewhere in this algebra ×1
excluded middle first fails in the three-chain ×1
excluded middle holds on each one-stage model and fails once they are glued ×1
formulas of up to 3 to 6 nestings ×1
G4 first fails in the four-chain ×1
Gödel–Dummett logic's axiom picks out its frames ×1
Gödel's implication is linear ×1
more than four formulas in one variable are distinguished ×1
no open set larger than the implication satisfies the condition ×1
no two chains glue into a chain ×1
no two frames with one last stage glue into one ×1
so does Peirce's law ×1
so is Łukasiewicz's ×1
some axiom holds in one algebra and fails in another ×1
the algebra has at least two elements ×1
the count never falls as the formulas grow ×1
the disjunction's value is the second-highest truth value ×1
the first model refutes the first disjunct at its root ×1
the first model's root forces the same things after gluing ×1
the formulas are among em, wem, dnn, gd, kp, triple ×1
the glued valuation only ever grows ×1
the implication really does meet the antecedent inside the consequent ×1
the implication really is the largest element whose meet lies below ×1
the logic of the weak law's axiom picks out its frames ×1
the negation of an open set is open ×1
the new root forces neither disjunct, so it does not force the disjunction ×1
the orders are among point, chain2, chain3, anti2, v, lambda, diamond ×1
the pair is one of em, gd, wem, deep ×1
the refuting algebra has a valuation making (p → q) ∨ (q → p) fall short ×1
the refuting algebra has a valuation making ¬¬p → p fall short ×1
the refuting algebra has a valuation making ¬p ∨ ¬¬p fall short ×1
the refuting algebra has a valuation making p ∨ ¬p fall short ×1
the search has several algebras in it ×1
the search runs over orders on up to 2 to 4 points ×1
the search separates the formulas it refutes from the ones it cannot ×1
the second model refutes the second disjunct at its root ×1
the separating algebras run to 2 to 4 points ×1
the set sits strictly inside the ambient line ×1
the set together with its negation does not fill the line ×1
the union has as many pieces as the two sets between them ×1
the view is one the family draws ×1
the weak law and linearity hold in every chain ×1
three negations are the same as one ×1
three negations collapse in every Heyting algebra ×1
three negations collapse to one ×1
three to five letters ×1
which is not the top, so the formula fails ×1

Where it is called

Every figure on this list is drawn by the same rule, so a change to the rule changes all of them at once. That is why the list is published.

Logic

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

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

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

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

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.

The whole library · What the figures prove