Welcome

This Jupyter Book turns the core ideas from source.tex into a runnable, experiment-first guide. The focus is: use lambda calculus as a programming language for logic, then reconstruct a core fragment of propositional logic via the Curry–Howard correspondence, and finally build the foundations of Peano arithmetic with hands-on proofs.

How to use this book

• Each chapter is a Jupyter notebook you can run in VS Code.

• Mathematical definitions, lemmas, and examples appear in colored boxes.

• Python code mirrors lambda-calculus constructions so you can test and explore.

• Selected chapters include Bussproofs-style proof-tree diagrams in HTML.

• Reduction and substitution sections include animated visual traces.

• A right-side glossary widget gives quick definitions of alpha/beta/eta/normal form.

• For recursion and conditionals, see the note on eager evaluation in execution_notes.md.

• All exercises have hidden, linked solutions in notebooks/99_exercise_solutions.ipynb.

Prerequisites

• Comfort with functions and basic proofs.

• No advanced type theory is assumed.

Notation

• \lambda x. t is written as λx. t in math cells.

• We use Church encodings for booleans and numerals.

Tip

If you run these notebooks in VS Code, you can edit and re-run any lambda term or Python function to see how the proof or computation changes.

Remark (Python Evaluation Strategy)

Python is eager. With Church booleans, IF behaves lazily under normal-order (call-by-name style) reduction, but not under eager evaluation. In the recursion and Peano arithmetic chapters we use IF_THUNK to delay branch evaluation in Python. See execution_notes.md for details.