「‍」 Lingenic

README

(⤓.txt ◇.txt); γ ≜ [2026-07-17T120407.600, 2026-07-17T135416.643] ∧ |γ| = 3

STRUCTURE THEORIES

Axiomatizations of order, algebra, and geometry: theories whose signature governs a structure rather than a foundation. Dense linear orders, algebraically closed fields, real closed fields, Tarski's elementary geometry, and the theories of groups, rings, and fields are first-order theories in the same sense Peano arithmetic is — a signature, axioms, classical first-order consequence — and they are the theories the model theory in Metatheory is about.

The division's other four groups axiomatize what mathematics is built from: number, set, truth, part. This group axiomatizes what mathematics is built into. That is a different motive and it produces different theories: where the foundational entries are individuated by strength and measured by what they cannot prove, these are individuated by their models and measured by what they decide. Quantifier elimination, categoricity, o-minimality, and stability are properties of theories in this group, and they are stated in Metatheory/Model-Theory with these theories as their instances. The instances belong here.

The group is also where the collection's decidability results live. Presburger and Skolem arithmetic decide fragments of number by removing an operation; DLO, ACF, RCF, and Tarski's geometry are decidable outright, and their decidability is not a weakness but the reason Tarski could prove that elementary geometry is complete. Reading them against the arithmetic entries is the point: the same first-order logic, the same kind of axioms, and the incompleteness phenomenon absent — because the signature does not code sequences. The theories of groups and rings sit on the other side of that line, undecidable by interpreting Q, and are here to mark it.

Entries are cross-listed with Metatheory/Model-Theory, which holds the general results, and with Applications/Spatial for the geometric material. The bare axiomatization belongs here; the technique belongs there.