PROOF SYSTEMS
Proof calculi and the metatheory of derivation: the formats in which proofs are built and the theorems about their structure, normalization, and strength. Where a model-theoretic entry studies what a logic's formulas describe, an entry here studies how its proofs are constructed and what they cost.
Entries include the calculus formats (sequent calculus, natural deduction, tableaux, resolution, Gentzen systems, hypersequents, nested sequents, display calculus and display logic, deep inference, focusing and polarized systems, proof nets, uniform and circular proofs), the structural metatheory (normalization, cut elimination, ordinal analysis, proof mining, reverse mathematics, bounded arithmetic), the algorithmic proof methods (unification, DPLL and SAT solving), the limitative results (Gödel's incompleteness theorems), the proofs-as-programs correspondence (Curry-Howard, cross-listed with Type/Simple), and the historical practice of proof and consequence (Stoic logic, medieval consequentiae, sophismata, terminist logic; Navya-Nyaya).