Syntax of proofs, derivability, normal forms, consistency proofs, proof length, and proof complexity.
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 for proofs are studied next, showing how proofs can often be transformed into more regular shapes that make their structure easier to analyze.
Consistency proofs are then discussed, where one shows that a formal system cannot derive a contradiction, usually by assigning meanings to formulas or by analyzing the structure of derivations.
The final part of the chapter studies proof length and complexity, asking not only whether a statement has a proof, but how long or difficult such a proof must be inside a given formal system.