3.3 Hilbert Systems
Hilbert systems provide a very compact and minimalistic approach to formal proofs, where almost all logical reasoning is encoded in a fixed collection of axiom schemes, and only a small number of inference rules are used to derive new formulas. In contrast with natural deduction and the sequent calculus, where many rules correspond directly to logical connectives, Hilbert systems concentrate the logical content in axioms and rely heavily on repeated...