Chapter 15. Ordinal Analysis
Proof theoretic ordinals, transfinite induction, strength of theories, applications to arithmetic, and limits of formal strength.
Tag
Proof-Theory
39 notes
14.5 Extensions and Refinements
Stronger forms of incompleteness, Rosser’s improvement, Löb’s theorem, and connections to computability.
14.2 First Incompleteness Theorem
Construction of a true but unprovable statement using diagonalization and self-reference.
Chapter 14. Godel Theorems
Arithmetization of syntax, the first and second incompleteness theorems, implications for formal systems, and refinements.
13.5 Proof Length and Complexity
Quantitative study of proofs, including proof size, efficiency, and connections to computational complexity.
13.4 Consistency Proofs
Methods for proving consistency of formal systems, including syntactic and semantic approaches.
13.3 Normal Forms
Normalization of proofs, elimination of detours, and structural simplification of derivations.
13.2 Derivability
Formal notion of deriving formulas from assumptions, including structural properties and inference behavior.
13.1 Syntax of Proofs
Formal structure of proofs, including derivations, inference rules, axioms, and proof representations.
Chapter 13. Formal Proof Systems
Syntax of proofs, derivability, normal forms, consistency proofs, proof length, and proof complexity.
3.4 Proof Transformations
Transformations of proofs, normalization, and structural properties of derivations.
Chapter 3. Proof Systems
Formal systems for deriving logical conclusions including natural deduction, sequent calculus, Hilbert systems, and proof transformations.
2.25 Common Proof Mistakes and Debugging
Lean proofs fail in predictable ways.
2.24 Simplification and Automation
Lean provides automation to reduce routine proof steps.
2.23 Rewriting Strategies
Rewriting with equality is one of the most frequent operations in Lean.
2.22 Backward Reasoning
Backward reasoning starts from the goal and reduces it to simpler subgoals.
2.21 Forward Reasoning
Forward reasoning starts from the assumptions in the local context and derives new facts until the goal becomes immediate.
2.20 Using Assumptions Effectively
An assumption is a local term that Lean may use to solve the current goal or produce another proof.
2.19 Local Context Management
The local context is the list of variables, hypotheses, instances, and intermediate facts available at a point in a proof.
2.18 Naming Conventions
Names in Lean carry meaning.
2.17 Proof Structuring Patterns
A Lean proof should expose the shape of the argument.
2.16 Introduction and Elimination Rules
Every logical connective in Lean has two sides.
2.15 Case Analysis
Case analysis is the proof pattern for using data that has more than one possible constructor.
2.14 Proof by Contradiction
Proof by contradiction is a classical proof pattern.
2.13 Classical vs Constructive Logic
Lean is constructive by default.
2.12 Universal Quantifiers
A universal statement asserts that a property holds for every element of a type.
2.11 Existential Quantifiers
An existential statement says that some object exists with a given property.
2.10 Symmetry and Transitivity
Equality supports two structural operations: reversing direction (symmetry) and chaining steps (transitivity).
2.9 Rewriting with Equality
Rewriting is the main way to use equality in Lean.
2.8 Equality Basics
Equality expresses that two terms are identical.
2.7 True and Trivial Proofs
`True` is the proposition that always has a proof.
2.6 False and Contradiction
`False` is the proposition with no constructors.
2.5 Negation
Negation represents "not".
2.4 Disjunction
Disjunction represents "or".
2.3 Conjunction
Conjunction represents "and".
2.2 Implication and Functions
Implication is the first logical connective to understand in Lean because it is also the ordinary function type.
2.1 Propositions as Types
Lean identifies propositions with types and proofs with terms.
1.5 Soundness and Completeness
Soundness, completeness, and the relationship between semantic validity and formal provability.
03. Logic and Foundations
Formal logic, set theory, computability, and the foundations of mathematics treated as a formal system.