Source and edition

Tim Button and the Open Logic Project contributors, The Open Logic Text, Arithmetization chapter. Open Logic Project.

The teaching unit is dedicated to the public domain under CC0 1.0. Its cut definition, order and union argument, and the square-root cut calculation follow the Open Logic source in the unit’s own words; the Cauchy-sequence approach also informs the unit. GPT-6 Astra (OpenAI), Ultra, in Codex wrote it, including the detailed field and order verification, bisection estimates, comparison and uniqueness proofs, and worked solutions, and self-checked it.

Editable teaching unit · Read the lesson

Sources

• Tim Button and Open Logic contributors: cuts.tex
• Tim Button and Open Logic contributors: cauchy.tex
• Tim Button and Open Logic contributors: checking-details.tex

Edition and prerequisites

Open Logic source revision 1e960beff9ed7835bf3e3f1335e21af3439cd107. The teaching proofs are fully supplied in the editable lesson. The unit starts with rational arithmetic, induction, recursion and elementary set constructions; it does not claim to prove those starting inputs.