A complete derivation in first-order Peano arithmetic, with independent mechanical verification at the moment of rendering
Communications in Settled Matters 1 (2026), pp. 32–32.
Abstract. Working in first-order Peano arithmetic, we prove that the set S ≔ {n ∈ ℕ : 260 < n < 293} has cardinality exactly 32. The derivation proceeds from the axioms P1–P7 and the definition of order through eleven lemmas, of which the principal are the digitwise identity 260+33=293 (L7) and the enumeration lemma Cₐ(a+Sk)=k (L11). The result is then confirmed by independent means: thirty-two unary witnesses embedded in the present document direct any conforming layout engine to reconstruct S and to recompute both its extension and its cardinality at the moment of rendering, so that the theorem is re-established on every reading. The count is further determined under all rival interpretations of the question: 34 (endpoints included), 33 (either half-open reading), 2ℵ₀ (real numbers), ℵ₀ (rational numbers); over ℂ the question is shown to be ill-posed.
2020 Mathematics Subject Classification. Primary 03F30; Secondary 68U15. Key words and phrases. Successor function, cardinality, unary numeration, automatic counters.
The vernacular question “how many numbers are between 260 and 293” is ill-typed until both of its nouns are fixed. We fix them by fiat.
I1. Number ≔ element of ℕ = {0, S0, SS0, …}, the standard model of §1.
I2. Between ≔ strictly between: the set at issue is S ≔ {n ∈ ℕ : 260 < n < 293}. An endpoint is not between itself and anything. This is a definition, not a moral position.
I3. 0 ∈ ℕ. (Irrelevant below; declared to preempt correspondence.)
Dissenters are provided for in §4.
We work in classical first-order logic with equality, over L = {0, S, +, ·, <}, with axioms (after [1], lightly modernized):
P1: ∀x Sx≠0. P2: ∀x∀y (Sx=Sy → x=y). P3: ∀x x+0=x. P4: ∀x∀y x+Sy=S(x+y). P5: ∀x x·0=0. P6: ∀x∀y x·Sy=x·y+x. P7 (induction): φ(0) ∧ ∀x(φ(x)→φ(Sx)) → ∀x φ(x), one instance per formula φ. (A schema. We use finitely many instances, as must everyone.)
D<: x<y ≔ ∃z x+Sz=y. The axioms of equality are used silently and without apology. ≔ introduces a definition; within a chain of equations, ≔ and ≕ mark steps that hold by definition alone.
Numerals: 1≔S0, 2≔S1, 3≔S2, 4≔S3, 5≔S4, 6≔S5, 7≔S6, 8≔S7, 9≔S8, X≔S9. Decimal notation is a definitional scheme (⌜du⌝ ≔ ⌜d⌝·X+⌜u⌝, positionally); the instances of record: 260 ≔ (2·X+6)·X+0, 293 ≔ (2·X+9)·X+3, 32 ≔ 3·X+2, 33 ≔ 3·X+3, 34 ≔ 3·X+4; the upper bound of record is b ≔ 293. That these definitions agree with the numerals of the reader's childhood is Lemma 0; it is discharged by the reader's childhood [5].
L1. ∀x 0+x=x. Pf. P7 on x. Base: P3. Step: 0+Sx =P4 S(0+x) =IH Sx. ∎
L2. ∀x∀y Sx+y=S(x+y). Pf. P7 on y. Base: P3 twice. Step: Sx+Sy =P4 S(Sx+y) =IH SS(x+y) =P4 S(x+Sy). ∎
L3. ∀x∀y x+y=y+x. Pf. P7 on y. Base: P3, L1. Step: x+Sy =P4 S(x+y) =IH S(y+x) =L2 Sy+x. ∎
L4. ∀x∀y∀z (x+y)+z=x+(y+z). Pf. P7 on z. Base: P3 twice. Step: (x+y)+Sz =P4 S((x+y)+z) =IH S(x+(y+z)) =P4 x+S(y+z) =P4 x+(y+Sz). ∎
L5. ∀x∀y∀z (x+y)·z=x·z+y·z. Pf. P7 on z. Base: P5 thrice, P3. Step: (x+y)·Sz =P6 (x+y)·z+(x+y) =IH (x·z+y·z)+(x+y) =L3,L4 (x·z+x)+(y·z+y) =P6 x·Sz+y·Sz. ∎
L6. 6+3=9. Pf. 6+3 ≔ 6+S2 =P4 S(6+2) ≔ S(6+S1) =P4 SS(6+1) ≔ SS(6+S0) =P4 SSS(6+0) =P3 SSS6 ≕ SS7 ≕ S8 ≕ 9. ∎ (The one proof in this paper given in full, so that the reader may calibrate what is being spared elsewhere.)
L7. 260+33=293. Pf. ((2·X+6)·X+0)+(3·X+3) =P3 (2·X+6)·X+(3·X+3) =L5 ((2·X)·X+6·X)+(3·X+3) =L4 (2·X)·X+(6·X+(3·X+3)) =L4 (2·X)·X+((6·X+3·X)+3) =L5 (2·X)·X+((6+3)·X+3) =L6 (2·X)·X+(9·X+3) =L4 ((2·X)·X+9·X)+3 =L5 (2·X+9)·X+3 ≕ 293. Associativity of · is never used, which is fortunate, for we never proved it. ∎
L8. 33=S(32). Pf. 3·X+3 ≔ 3·X+S2 =P4 S(3·X+2) ≕ S(32). ∎
L9. ∀x∀z x+Sz≠x; hence ∀x ¬(x<x). Pf. P7 on x. Base: 0+Sz =L1 Sz ≠ 0, by P1. Step: were Sx+Sz=Sx, then S(x+Sz)=Sx by L2, so x+Sz=x by P2, against IH. The “hence” is D<, one quantifier negation, and modus tollens. ∎
D#. Fix a. Let χₐ(n) ≔ 1 if a<n and χₐ(n) ≔ 0 otherwise — a definition by cases, licit because a<n ∨ ¬(a<n) (immediate; the logic is classical; intuitionists may instead prove the decidability of < by double induction, and are warmly encouraged to). Let Cₐ(0) ≔ 0 and Cₐ(Sn) ≔ Cₐ(n)+χₐ(n) — a definition by primitive recursion, available inside PA by Gödel's β-function [2]; the coding is suppressed here, as it is everywhere, always. Cₐ(u) thus counts exactly the n with a<n and n<u, so that |S| = C₂₆₀(293). (For the fastidious: “counts exactly” abbreviates the PA-definable bijection between {n : a<n<u} and {m : m<Cₐ(u)}, built by the same recursion. The fastidious know who they are.)
L10. ∀a∀j (∃w j+w=a → Cₐ(j)=0); in particular Cₐ(a)=0, and moreover Cₐ(Sa)=0. Pf. P7 on j. Base: the definition of Cₐ(0). Step: given Sj+w=a, first j+Sw =P4 S(j+w) =L2 Sj+w = a, so Cₐ(j)=0 by IH; second ¬(a<j), for a+Su=j would give a = Sj+w =L2 S(j+w) = S((a+Su)+w) =L4 S(a+(Su+w)) =P4 a+S(Su+w), against L9; so χₐ(j)=0, whence Cₐ(Sj) =D# Cₐ(j)+χₐ(j) = 0+0 =P3 0. The particular is the instance j≔a, w≔0 with P3; the moreover is Cₐ(Sa) =D# Cₐ(a)+χₐ(a) = 0+0 =P3 0, the second summand vanishing by L9. ∎
L11. ∀a∀k Cₐ(a+Sk)=k. Pf. P7 on k. Base: a+S0 =P4 S(a+0) =P3 Sa, and Cₐ(Sa)=0 by L10. Step: Cₐ(a+SSk) =P4 Cₐ(S(a+Sk)) =D# Cₐ(a+Sk)+χₐ(a+Sk) =IH k+χₐ(a+Sk); now a<a+Sk by D< with witness k, so χₐ(a+Sk)=1, and k+1 ≔ k+S0 =P4 S(k+0) =P3 Sk. ∎
Theorem. |{n ∈ ℕ : 260 < n < 293}| = 32.
Pf. 293 =L7 260+33 =L8 260+S(32). Hence |S| =D# C₂₆₀(293) = C₂₆₀(260+S(32)) =L11 32, taking a ≔ 260 and k ≔ 32. ∎
In the proper idiom: PA ⊢ C₂₆₀(293)=32, every numeral read as its §1 definition. The standard model concurs; the reader, inhabiting it, has no standing to differ.
R1 (inclusive endpoints). If “between” admits its endpoints, the count is |{n : 260≤n≤293}| = SS(32) = 34: the two endpoints are appended to S by hand, and 34 = S(33) = SS(32), each equality proved exactly as L8 was. (Alternatively L11 with a≔259, k≔34; but that route requires 259+35=294, whose digitwise proof contains a carry, and we decline to perform a carry.)
R2 (half-open readings). Either half-open reading yields 33 = S(32): one by L11 with a≔260, k≔33 via the carryless 260+34=294; the other by appending its endpoint by hand as in R1, its own L11 route costing the carry 9+4, which we decline as before. Thirty-three pleases nobody, and is therefore the compromise.
R3 (real numbers). If “number” denotes a real number, the answer is 2ℵ₀: x ↦ (x−260)/33 is an order isomorphism from (260,293) onto (0,1), and |(0,1)| = |ℝ| = 2ℵ₀ [3]. This is not 32; it is not even a number in the sense of I1. Askers intending this reading are invited to sit quietly with what they have done.
R4 (rational numbers). ℵ₀, by the map of R3 and the countability of ℚ [3]. Still not 32.
R5 (complex numbers). Ill-posed: no linear order on ℂ is compatible with its field operations — in an ordered field every square is ≥ 0, and i·i is not. Nothing there is “between”. Returned to sender.
Under every admissible reading the question has an exact answer; under the intended one, that answer is 32.
This document referees itself. Inside the frame below, the source of this file contains exactly thirty-two empty p elements: the set S in unary, unary being the only numeral system whose adequacy requires no lemma. Two counters (CSS 2.1, §12.4 [4]) direct the reader's layout engine to set n ≔ 260 and c ≔ 0; to apply S to both once per witness, typesetting n each time, so that the elements of S are enumerated by the reader's machine rather than by us; to apply S to n once more at the frame's end and typeset the result, which the reader will observe equals b — the engine has performed thirty-three successor applications upon 260 and arrived at 293, an independent check of L7 and L8; and to typeset c last, an independent check of the Theorem.
Of the thirty-five numerals typeset within the frame, exactly one is read from this file: the basepoint 260, the counter's initialization — it plays the axiom. The other thirty-four are computed at render time by a party with no stake in the outcome. That the thirty-third successor of the basepoint coincides, glyph for glyph, with the b of §1 may be confirmed by the reader in three character comparisons; these are the reader's share of the work.
The derivations of §3 and §5 proceed from disjoint trust bases — the axioms of Peano and the specifications of the web platform, two bodies not known to collude — and they agree. Should some user agent typeset a total other than 32, the theorem stands and the user agent does not. Nothing here executes: there is no script; the computation above is declarative layout, which cannot be deceived, bribed, or reasoned with.
∎ ∎
(once analytically; once mechanically)
Remarks for the reader of source. The witnesses are unclosed: each p element is closed by the birth of its successor, and the last by its ancestor's end tag (WHATWG HTML, §13.2.6 [4]); the exhibit, like ℕ itself, is generated by succession and closed from above. Within the frame, the inner S names the set and the outer S the successor; the collision is regretted but not repaired, and max means what max means. The document likewise omits html, head and body, whose existence the same section infers; we do not write what can be derived. Every “<” in the mathematics is escaped, since an unescaped one before a letter opens a tag: in this genre even the less-than sign must be handled rigorously.