13. Formal Proof Systems
Formal proof systems study proofs as mathematical objects, with explicit syntax, fixed rules, and precisely defined notions of derivation. The chapter begins with the syntax of proofs, where a proof is treated as a finite formal object built from formulas, assumptions, axioms, and inference rules. Derivability is then introduced to express when a formula can be obtained from a given collection of assumptions inside a chosen proof system. Normal forms...