INCLUSION CRITERIA
An entry belongs in this subdivision if and only if its subject is a proof calculus or a metatheorem about the structure, transformation, or strength of formal derivations.
Required: At least one of the following:
- A proof format with explicit inference rules (sequent, natural deduction, tableaux, resolution, display, proof nets)
- A structural result about proofs (cut elimination, normalization, ordinal analysis, proof mining)
- An algorithmic proof procedure or a limitative theorem about provability (unification, SAT, incompleteness)
- A meaning explanation giving the connectives by their proof conditions (BHK, proof-theoretic semantics)
Not sufficient: A result about models or definability (Model-Theory). A categorical semantics of proofs (Categorical). A theory of computability (Computability).
Boundary: Gödel's incompleteness (about provability) lives here; Tarski's undefinability (about truth) lives in Model-Theory. Reverse mathematics is cross-listed with Model-Theory. The historical logic entries concern proof and consequence as formal practice; rhetorical and dialectical practice belongs in Argumentation and Rhetoric.