logic_induction

A Lean 4 formalization of the exercises in "Induction: Well-founded relations and generalized induction", lecture notes by Prof. Mohamed Amer for a logic course at Cairo University.

The project has no dependencies, not even Mathlib. It defines its own Set and the few operations it needs, so that the statements stay close to the notes.

Contents

• LogicInduction/Set.lean: sets as predicates, membership, subset, intersection, difference, univ, range, and predR, which is the notes' ρ[x].
• LogicInduction/IndN.lean: Section 1. Peano-like structures and the equivalence of the two induction principles.
• LogicInduction/Relations.lean: relative product, transitivity, powers ρⁿ, the closures ρ⁺ and ρ*, and their properties.
• LogicInduction/WellFounded.lean: well-founded relations, the principle of ρ,A-induction, and the equivalence theorem.
• LogicInduction/SuccWF.lean: the successor relation is well founded.
• LogicInduction/WfClosure.lean: ρ is well founded iff ρ⁺ is.
• LogicInduction/NatOrder.lean: ≤ = S*, < = S⁺, and course of values induction on ℕ.
• LogicInduction/WellOrder.lean: well orderings and well-foundedness.
• docs/Logic_Induction.pdf: my written proofs, which the Lean code follows (not updated).

Each theorem carries a comment with its number in the notes where it has one.

Progress

• Peano-like structures and Theorem 1.5 (the two forms of induction are equivalent)
• Well-founded relations and the principle of ρ,A-induction
• Equivalence of well-foundedness, ρ,A-induction, and no infinite descending sequence
• ρ is well founded iff it is well founded on Rρ
• ρ,A-induction holds for every A iff it holds for Rρ
• The successor relation is well founded
• If σ ⊆ ρ and ρ is well founded, then σ is well founded
• Relative product: transitivity, functions, associativity, failure of commutativity
• Powers of a relation, including ρ^(m+n) = ρ^m | ρ^n
• TC(ρ) = ρ⁺ and RTC(ρ) = ρ*
• ρ*|ρ = ρ⁺ = ρ|ρ*
• ρ is well founded iff ρ⁺ is
• ≤ = S*, < = S⁺, < is well founded, course of values induction
• Well orderings: a strict linear order is a well ordering iff it is well founded, with a counterexample when linearity is dropped
• Remarks 1 to 3 on domains, ranges, and powers
• Uniqueness in the recursion theorem
• Other proof of Claim (⋆)

Building

Install Lean through elan. The toolchain version is pinned in lean-toolchain.

lake build

No network access is needed after elan has fetched the toolchain.

Proof Atlas

atlas/ contains an interactive companion site that presents every declaration three ways: its informal pen-and-paper proof (transcribed from docs/Logic_Induction.pdf [which is not upated; I know]), the exact machine-checked Lean source, and its position in the proof dependency tree. It is a static Next.js site generated from the Lean sources; see atlas/README.md to run it locally or just access it from https://MinaBasilious.github.io/logic_induction/.

Authorship

• The Lean formalization (all definitions, theorems and proofs) is entirely human work, designed and written by me (Mina Basilious) and only checked by the machine (lake build, plus an axiom audit with #print axioms: every declaration depends solely on the standard axioms).
• The Proof Atlas website was built with AI assistance; parsing, informal proof transcriptions, and UI. It is a presentation layer over the human-written mathematics; no mathematical statement or proof originates from AI.

Source

The statements follow the notes by Prof. Mohamed Amer, which are not included in this repository. The proofs and any mistakes in them are mine.

License

See MIT License.