= Cartesian theory
{c}
{title2=$\mathbb T$}
A Cartesian theory uses a many-sorted <first-order signature> and sequents between <Cartesian formulas>. The fragment contains equality, atomic relations, truth, finite conjunction and existential quantification with provably unique witnesses. It has a <Cartesian syntactic category> with finite limits, whose <finite-limit-preserving functors> classify its internal models. Arbitrary existential quantification, disjunction and falsity are not added as finite-limit constructors.
Back to article page
