Formal Systems and Axiomatics

1900. Paris. David Hilbert publishes 23 problems for 20th-century mathematics. Problem two: prove the consistency of arithmetic. 1931: Kurt Godel proves it is impossible from within the system itself. Hilbert's program collapses. But from the ruins grows something unexpected: CompCert - a formally verified C compiler used in aviation and nuclear engineering. Formal systems turned out to be more powerful than Hilbert imagined.

• **CompCert (Xavier Leroy, INRIA)**: formally verified C compiler - every translation step proved in Coq. Used in aviation and nuclear industry where a compiler bug is a catastrophe
• **TLA+ at Amazon**: formal specification of distributed systems S3, DynamoDB, EBS. Before adoption: one bug in distributed consensus could cost billions. After: 17 critical bugs caught before deployment
• **Z3 SMT solver (Microsoft Research)**: formal program verification through automated contradiction search. Used in GitHub Copilot safety layers and AWS infrastructure
• **seL4**: operating system with machine-proven security via Isabelle/HOL. Used in military drones - the first OS kernel with a machine-checked correctness proof

Axioms and the Axiomatic Method

A formal system consists of three components: an alphabet (symbols), a grammar (rules for forming well-formed formulas), and axioms together with inference rules. A proof is a finite sequence of formulas where each formula is either an axiom or derived from previous formulas by an inference rule. The key word is finite. A proof must be mechanically checkable - this is exactly what Coq, Lean4, and Isabelle do.

Syntax (formal derivability |-) and semantics (logical consequence |=) are different worlds. Godel's completeness theorem states they coincide for first-order logic: |- phi if and only if |= phi. This is a substantive result - proving that two independently defined notions match requires real work.

Euclidean geometry: 5 axioms generate all of school geometry. Kolmogorov's 3 axioms define all of probability theory. The axiomatic method is a game: choose the rules, then everything follows. CompCert (Xavier Leroy, INRIA) is a C compiler with every translation step proved correct in Coq. Used in aviation and nuclear industry where a compiler bug equals a catastrophe.

**TLA+ at Amazon:** formal specification of distributed systems S3, DynamoDB, EBS. Before adoption: one bug in distributed consensus could cost billions. After: 17 critical bugs caught before deployment. Formal logic is not academia. It is an insurance policy on hundreds of billions of dollars of infrastructure.

Deduction and the Deduction Theorem

Deduction is the derivation of consequences from premises according to the system's rules. The Deduction Theorem is a meta-theorem linking conditional and unconditional derivation: Gamma, phi |- psi if and only if Gamma |- phi -> psi. Instead of proving "given hypothesis phi we derive psi", one can directly prove the implication "phi -> psi" as an object inside the formal system.

The Deduction Theorem holds in most propositional and predicate systems, but requires care: in predicate logic it does not apply to formulas containing free variables that were bound by generalization rules. This is not a bug - it is a fundamental constraint that surfaces when working with quantifiers.

The Deduction Theorem is a meta-theorem: a statement about a formal system, not inside it. Most such meta-theorems are proved by induction on the length of a derivation - a classic application of mathematical induction to syntactic objects.

Consistency and Completeness

A system is consistent if it cannot simultaneously derive both phi and not-phi. It is complete if every formula true in it is provable. These two properties were the goal of Hilbert's program. Godel in 1931 showed: a system rich enough to express arithmetic is either inconsistent or incomplete. No choice. This is not a bug in formal systems - it is a fundamental limit.

Hilbert Systems and the Curry-Howard Correspondence

A Hilbert system is a style of formal system with a minimal set of inference rules (typically just modus ponens) and a rich set of axiom schemas. Alternatives include Gentzen's natural deduction (more convenient for reasoning) and sequent calculus (more powerful for metatheory and automated theorem proving). Sequent calculus underlies the Z3 SMT solver - the one that verifies programs in GitHub Copilot's safety layer.

The Curry-Howard correspondence is one of the deepest discoveries of the 20th century. Logic and type theory are the same thing described in different languages. Agda, Coq, and Lean4 use this for machine-verified mathematical proofs. When Lean4 compiles a correctly typed term, it verifies a proof. seL4 - operating system with machine-proven security via Isabelle/HOL. Used in military drones - the first OS kernel with a machine-checked correctness proof.

Hilbert's program collapsed in 1931. But the collapse produced an unexpected fruit: the realization that formal systems are not just mathematics. They are computation. Curry-Howard made this precise: proof equals program, type equals formula. Lean4 holds over 100,000 machine-verified theorems. Behind each one sits some variant of the structure this lesson covers.

Key Takeaways

• Formal system = alphabet + grammar + axioms + inference rules. A proof is a finite sequence of formulas, mechanically checkable
• Consistency: cannot derive both phi and not-phi simultaneously. Otherwise explosion - everything becomes derivable
• Deduction Theorem: Gamma, phi |- psi if and only if Gamma |- phi -> psi
• Godel's first incompleteness theorem: sufficiently rich consistent theories are incomplete - they contain true but unprovable statements
• Curry-Howard correspondence: proof = program, type = formula. CompCert, seL4, Lean4 are this in action

Toward Godel's Theorems

Hilbert's program collapsed in 1931 when Godel proved two fundamental limitations. The next lesson covers the completeness theorem - the positive result that preceded that collapse.

• Godel's Incompleteness Theorems — Direct consequence of analyzing formal systems - impossibility of completeness for rich theories
• Undecidability and Completeness — Algorithmic consequences of Godel's theorems - connection to the halting problem

Вопросы для размышления

• Why did mathematicians before the 20th century get along without formal systems? What changed with the discovery of set-theoretic paradoxes?
• If a proof is a program, what is a 'bug' from a logical standpoint?
• Amazon uses TLA+ and finds bugs in DynamoDB before deployment. Is this formal verification or just testing? What is the difference?

Связанные уроки

• ml-03 — Predicate logic is the language formal systems are built in
• ml-05 — Godel completeness theorem - the next result after formal systems
• dm-04 — Proof methods are the practice of what formal systems describe in theory
• dm-03 — Predicate logic as a live example of an axiomatic system
• fl-18-turing-machine