Generator
A set, its negation, and its double negation
A generator in the logic library, called 5 times across 1 essays. Below: what it draws at its defaults 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.
At its defaults
show: "algebra"
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.
- a set is contained in its double negation ×1
- and here it is strictly contained — the punched-out points come back ×1
- and so does double-negation elimination ×1
- between one and four points are punched out ×1
- every element sits below its double negation ×1
- every punched-out point is inside the set ×1
- excluded middle fails somewhere in this algebra ×1
- no open set larger than the implication satisfies the condition ×1
- the implication really does meet the antecedent inside the consequent ×1
- the negation of an open set is open ×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
- three negations are the same as one ×1
- three negations collapse to one ×1
Where it is called
Changing this generator changes every figure on this list. That is what makes the list worth publishing rather than keeping in a check script.