• README ⤓ .txt 2026-07-17T121634.146 000000000000672
  Formal systems studied as objects, rather than reasoning conducted within any one of them. Its entries are the theories, techniques, and theorems by which logics are given semantics, their proofs analyzed, their models constructed, and the limits of computation and provability established.
• Categorical
  Logics formulated or given semantics inside category theory: systems whose connectives, quantifiers, and proofs are read as universal constructions, functors, and natural transformations.
• Combination
  The methods by which logics, theories, and structures are built out of others, and the theorems that say what survives the construction.
• Computability
  The metatheory of computation: what functions and sets are effectively computable, decidable, or enumerable, and how the undecidable problems are stratified by degree and hierarchy.
• Duality
  The correspondences between algebraic and relational semantics, and the machinery that transports structure across them.
• Model-Theory
  The metatheory of the satisfaction relation: results and techniques about the models of a logic, their construction, classification, and the definability of properties within them.
• 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.
• CRITERIA ⤓ .txt 2026-07-17T121634.146 000000000000688
  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.