INCLUSION CRITERIA
An entry belongs in this division if and only if it is a theory: a non-logical signature together with axioms, whose consequence relation is inherited from a base logic rather than defined by the entry.
Required: Both of the following:
- A non-logical signature (constants, functions, relations) that the axioms govern
- Axioms that are not valid in the base logic — they say something, and dropping them changes the theorems
Not sufficient: Having axioms, since every system in the collection has them. This division is for systems whose individuation is the signature and the axioms, with the logic taken as given. If the entry changes what follows from what — the variety, the accessibility relation, the structural rules, the typing judgment, the object of evaluation — it belongs in the apparatus division that names the change, not here.
Boundary: An axiomatization of an order, algebraic, or geometric structure is a theory by this criterion and belongs in the Structure subdivision, which states its own criteria; the model-theoretic properties such theories have—quantifier elimination, categoricity, o-minimality, stability—are Metatheory/Model-Theory, and the theories that have them are here. A theory that also modifies its logic is placed by the modification, not by the signature: constructive set theory is classified here because CZF's departure is its axioms over an intuitionistic base already catalogued in Algebraic/Heyting, whereas a system whose novelty is the base logic belongs there. Results about theories—incompleteness, forcing, reverse mathematics, ordinal analysis—belong in Metatheory and are cross-listed from here. A theory used to model an application domain belongs in Applications; the bare axiomatization belongs here.