Arithmetic
Arithmetic is treated here as a matter of models rather than of proof rules: a universe of elements laid out in a line, where everything up to a given element is finite in number. The zero, the successor, addition, multiplication and exponentiation are all read off that single layout, so each statement of the chapter is a statement about a structure a reader can picture.
Peano’s postulate, that a zero is the successor of nothing, is what splits the models. Negating it is the same as the universe being finite, which is the chapter’s first result. The models that satisfy it are the natural numbers and nothing else, which is the chapter’s last one. In between, a universe with a maximum counts past the top by wrapping around to the bottom, and that is exactly arithmetic modulo the size of the universe.
Definitions are earned rather than assumed. A property that exactly one element has picks that element out, and recursion is the same idea applied to relations: a specification that speaks of the very relation it defines, answered by exactly one such relation. Addition, multiplication and exponentiation follow from that pattern alone. The finiteness of initial segments is what makes it work, since it makes the order well founded.
The infinite model is reached rather than assumed. A tower of finite models, each an initial segment of the next, glues together into a single universe that is infinite, so Peano’s postulate holds of it. Termination closes the chapter’s toolkit: on a model, a run that never moves upwards stays within finitely many elements, and a measure that strictly shrinks makes every run stop.
- Model
- Difficulty: hard (6 definitions, 0 abbreviations, 4 lemmas, 5 theorems)
- Examples: 0
- Total complexity: 23965
- Definition
- Difficulty: moderate (4 definitions, 0 abbreviations, 4 lemmas, 2 theorems)
- Examples: 0
- Total complexity: 6921
- Recursion
- Difficulty: optional (9 definitions, 0 abbreviations, 1 lemmas, 5 theorems)
- Examples: 0
- Total complexity: 855
- PrimitiveRecursion
- Difficulty: optional (4 definitions, 1 abbreviations, 11 lemmas, 10 theorems)
- Examples: 0
- Total complexity: 35183
- Operation
- Difficulty: easy (3 definitions, 3 abbreviations, 6 lemmas, 0 theorems)
- Examples: 0
- Total complexity: 1098
- Termination
- Difficulty: moderate (3 definitions, 0 abbreviations, 2 lemmas, 5 theorems)
- Examples: 0
- Total complexity: 3458
- Tower
- Difficulty: optional (8 definitions, 0 abbreviations, 20 lemmas, 11 theorems)
- Examples: 0
- Total complexity: 95195
- Categoricity
- Difficulty: moderate (2 definitions, 0 abbreviations, 4 lemmas, 1 theorems)
- Examples: 0
- Total complexity: 3191