Logic — page 2

The numbers to 18 in hereditary base 2, and their ordinals. A table of small whole numbers written in hereditary base notation beside the ordinal obtained by replacing the base with omega.

Every ordinal in base omega

Every ordinal below a certain point is a descending sum of powers of ω, in exactly one way. That notation makes comparison mechanical, it is what hereditary base notation becomes when the base is replaced, and it stops at the first ordinal it cannot name.

Limit ordinals and the sequences that approach them. Several ordinals with the first terms of their fundamental sequences, and the successors marked as having a predecessor instead.

Reached from below, or not at all

Every limit ordinal anybody meets is the end of an increasing sequence — ω, ω·2, ω^ω, all of them approached one step at a time. The first uncountable ordinal is not, and the reason it is not constrains the size of the continuum.

The fast-growing hierarchy at its first few ordinals. A table of the fast-growing hierarchy: one row per ordinal index, one column per argument, with the cells too large to evaluate marked as such.

An ordinal as a growth rate

Index a family of functions by the ordinals, each one iterating the last, and the index becomes a measure of how fast a function grows. The point where the index leaves what arithmetic can prove is exactly where the Goodstein sequence became unprovable.

Two diagrams the language cannot tell apart

A modal formula sees a diagram of worlds and arrows through a very narrow window. Exactly how narrow is settled by a game: where one player can answer every move, no formula whatever separates the two starting worlds, however different the diagrams look.

Worlds built out of sentences

A Kripke model needs worlds, and nothing so far has said where worlds come from. They can be made of the syntax: a world is a set of formulas it commits to, one world sees another when the boxed commitments line up, and in the model that results every formula is true exactly where it was assumed.

Axioms, the conditions on the arrows they answer to, and the one that answers to none. A table of modal axioms with the property of the accessibility relation each corresponds to, every row decided by sweeping all relations on up to four worlds.

The axiom with no property of the arrows

Each axiom of modal logic can be matched by hand to a condition on the arrows between worlds. There is a recipe that does it for a whole class of axioms, and there is an axiom the recipe cannot reach — not because nobody has looked, but because no condition on the arrows defines it at all.

The frames on which provability makes sense, and the two that are refused. Six small frames marked by whether Löb's axiom is valid on them: transitive frames with no cycles accept it, and any frame in which a world can reach itself does not.

Necessity that means provable

Read the box as "the theory proves" and one modal logic stops being a proposal about what necessity might mean. It becomes a complete description of what a formal system can prove about its own proofs — and its frames run forward, compose, and stop.

How many worlds a formula can need

A modal formula can be true in a model with infinitely many worlds. It can also be true in a small one — and the small one is built from the large one by throwing away every distinction the formula was never able to make.

Nearly always, or nearly never

Toss a coin for every pair of points and ask whether the graph that results has some property. For a property a first-order sentence can state, the answer in the limit is never a genuine probability — it is zero or it is one, and the game is what proves it.

What a sentence of depth 2 can reach. Two rings of points, of 14 and 19 points, each with a run of 9 consecutive points marked as the neighbourhood a sentence of depth 2 can inspect.

The distance a sentence can see

A first-order sentence with three quantifiers cannot notice anything about a graph beyond a fixed distance from the points it names. That single limitation is why it cannot say connected, and why the failure survives every attempt to add more quantifiers.

A 6-cycle and two 3-cycles: refinement cannot tell them apart. Two graphs side by side — one cycle and two smaller cycles — with the same number of points, the same number of edges and every point of the same degree.

The game the algorithm was playing

Change what Duplicator has to offer — a whole bijection instead of one element — and the game stops measuring first-order logic and starts measuring colour refinement, the algorithm every practical graph-isomorphism test begins with. Two subjects that grew apart are one game with the moves relabelled.

Where a word of m letters stops being distinguishable from one of m + 1. A row for each quantifier depth and a cell for each length, shaded where Duplicator survives the game between words of that length and one longer.

A language that can name a set

Allow a sentence to quantify over sets of positions as well as positions, and on words the answer changes completely: the sets buy exactly the languages a finite automaton recognises. Whether the number of letters is even is the smallest example of what the sets are for.

7 steps and 3 withdrawn assumptions. A natural-deduction derivation of (p → q) → (¬q → ¬p). Each horizontal bar is one inference, named on its right; the bracketed formulas are assumptions, and each is withdrawn at the step that names it.

The assumption a proof pays back

A tableau assumes the opposite once and takes it apart. Natural deduction assumes things freely, uses them, and then withdraws them — and the withdrawal is what turns a derivation of a consequence into a proof of an implication.

A lemma, and the proof that never mentions one

Proving something by first proving a lemma is what makes mathematics readable, and it is exactly what makes a proof system impossible to search — because the lemma can be any formula at all. Gentzen proved the step can always be removed, and the removal is not free.

Closed after 3 uses of the universal. The Herbrand expansion of a first-order question at 5 stages, with the number of remaining models at each. It reaches nought after 3 instantiations.

The instance that has to be guessed

Every rule of a propositional tableau replaces a formula by shorter ones, which is why it stops. The rule for a universal claim does not replace it — it keeps it and adds an instance — and one word changing turns a decision procedure into a search that may run forever.

A derivation of ((p → q) ∧ (q → r)) → (p → r), and the term it is. A natural-deduction derivation of ((p → q) ∧ (q → r)) → (p → r) with a lambda term written under each formula. The whole derivation is the term λh₁. λh₂. (π₂ h₁) ((π₁ h₁) h₂), and at every node the type of the term is the formula the derivation proves there.

Every derivation is a term

Write a variable for each assumption, an abstraction where one is discharged, and an application where an implication is used, and a natural-deduction derivation becomes a term. The formula it proves is the term's type, and checking the one is checking the other. A detour in the proof — a lemma introduced and at once used — is a term that simplifies, and simplifying it is removing the detour.

A implies B, and r ∨ s sits between them. A = ((p ∨ q) ∧ (p → r)) ∧ (q → s) implies B = (r ∨ s) ∨ t. A resolution refutation of A with the negation of B yields the interpolant r ∨ s. It uses only the shared atoms r, s, follows from A and implies B, and lies between the strongest and weakest interpolants.

The sentence between a premise and its consequence

When one formula implies another, something sits between them written only in the words the two have in common: a sentence the first implies and that implies the second. A refutation of the first together with the denial of the second hands such a sentence over, and every possible one lies between a strongest and a weakest that can be computed outright.

Two literals make an arrow

A clause of two literals, p ∨ q, says that if p is false then q is true, and if q is false then p is true — two arrows. A set of such clauses is a directed graph on the literals, and it is unsatisfiable exactly when some variable and its negation reach each other. Each of those two paths is a chain of resolution steps, and finding them takes time proportional to the size of the input.

A failed search is a proof

Search for an assignment by branching on variables and backing up whenever a clause turns false. If every branch fails, the tree the search leaves behind is itself a resolution refutation: write at each branch point the resolvent of the clauses below it, and the top of the tree is the empty clause. So every limit on short refutations is a limit on every such search — and the pigeonhole clauses, whose refutations are long, defeat them all.

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.

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.

Two graphs every count agrees on, and one question that does not. Two sixteen-point graphs drawn on a four-by-four grid, with one point marked and its six neighbours highlighted in each, the neighbours forming two triangles in one and a six-cycle in the other.

One gadget defeats every refinement

Colour refinement fails on two triangles against a hexagon; its two-dimensional version fixes that and fails on a pair of strongly regular graphs. For every k there are two graphs the k-dimensional version cannot separate, and they are built from one local piece whose only symmetry is a parity.

Who survives with two pebbles and who with three, over 4 rounds. A table of three pairs of graphs with, for each, whether the duplicating player survives a two-pebble game and a three-pebble game played to a fixed depth.

The boundary at three variables

Restrict a sentence to two variable names and it can still be arbitrarily long, because the names are reused. What it cannot be is deep: every satisfiable two-variable sentence has a small model, so asking whether one is satisfiable is a bounded search. Allow a third name and the question becomes undecidable.

The order type of a nonstandard model of arithmetic. The ordinary numbers as a run of dots, followed by 9 galaxies — copies of the integers — at the positions of c/2 up to 2c, ordered densely like the rationals, with c² beyond. Infinitely many more galaxies lie between those drawn.

A number larger than every number

Ask for a number bigger than 0, bigger than 1, bigger than 2, and so on for ever. Every finite piece of that request is granted by an ordinary number, so compactness grants all of it at once — in a structure that satisfies every sentence true of the whole numbers and still contains something beyond all of them. Nothing in first-order logic can say 'and nothing else'.