Generator
kripke
A generator in the logic library, called 3 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.
kripke 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: "stages"
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.
- □p at a world is p at every world it can reach ×1
- ◇p at a world is p at some world it can reach ×1
- a world that reaches nowhere makes every necessity true and every possibility false ×1
- excluded middle at a stage is exactly p there or ¬p there ×1
- no stage forces both p and its negation ×1
- some stage forces neither p nor its negation, so p ∨ ¬p fails there ×1
- the frame is one this figure knows ×1
- the valuation, as a bitmask over the stages is a whole number between 0 and 31 ×1
- what is established at a stage stays established later ×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.