INCLUSION CRITERIA
An entry belongs in this division if and only if its subject is a property, technique, or theorem about formal systems—their semantics, proofs, models, or computability—rather than a logic used for object-level reasoning.
Required: At least one of the following:
- A result about satisfaction, definability, or models (model theory)
- A proof calculus or a theorem about the structure of proofs (proof theory)
- A categorical formulation of a logic or its semantics
- A theorem or theory of computability, decidability, or degrees of unsolvability
Not sufficient: Being a logic one reasons in, however expressive. A named logic with a consequence relation belongs in the object-level divisions (Algebraic, Modal, Structural, Type, Team, Hyperintensional, Theories, Applications). A theory one reasons in—an axiom set over an inherited logic—belongs in Theories, however much metatheory is about it: Peano arithmetic is a theory, and Gödel incompleteness is the result about it that lives here.
Boundary: Provability and justification logics, though metatheoretic in motivation, are modal object-logics and belong in Modal/Alethic; the incompleteness and undefinability theorems they internalize belong here. Reverse mathematics is a result about the subsystems of second-order arithmetic and lives here; those subsystems live in Theories, and the two are cross-listed. A proof calculus for a specific logic belongs in Proof-Systems; that logic's semantics belongs with the logic.