Generator

tree

A generator in the logic library, called 16 times across 3 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.

tree 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

A tableau for (p → q) → (¬q → ¬p)A branching tree of formulas, each branch ending in a contradiction or in a description of a counterexample.¬((p → q) → (¬q → ¬p))p → q¬(¬q → ¬p)¬p¬q¬¬pp×q¬q¬¬p×assume the formula false, then take it apart: (p → q) → (¬q → ¬p)every branch closes, so the assumption is impossible — the formula is valid

show: "konig"

A tree branching at most 3 ways, to depth 4, and the path through itA tree drawn level by level, with the nodes that die out faint and a highlighted path that always steps to a node with descendants at the bottom.every node has at most 3 children and the tree reaches level 416 nodes on the bottom row; the marked walk takes a surviving child at every step

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.

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.

The whole library · What the figures prove