Cartesian theory ($\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.

In the positive finite-limit convention, a Horn theory uses atomic finite-conjunction sequents; uniquely witnessed existential extensions remain Cartesian. Its models are the finite-limit-preserving functors out of its Cartesian syntactic category. This convention does not insert arbitrary existential witnesses or falsity as Cartesian constructors. Its classifier is the presheaf classifier of a Horn theory.

Internal Horn models are finite-limit-preserving functors out of the Cartesian syntactic category. Since that category has finite limits, these are exactly flat functors; the presheaf Diaconescu equivalence for geometric morphisms proves the classifying property. Equivalently the classifier is the covariant functor category on finitely presented set-based models.

Objects are Cartesian formulas-in-context modulo provable equivalence, and arrows are provably total single-valued Cartesian relations. Composition quantifies the unique intermediate tuple. Context concatenation, conjunction and equality give finite limits. Its canonical model interprets a formula as its own context subobject, so factorization of antecedent through consequent is exactly sequent derivability.

If a Cartesian sequent fails to factor its antecedent subobject $A\hookrightarrow C$ through its consequent, the covariant representable functor ${\mathcal{C}}_{\mathbb{T}}(A,-)$ is a set-valued countermodel. It preserves finite limits, and the element named by the antecedent inclusion belongs to the antecedent but cannot belong to the consequent. Hence validity in every set model implies Cartesian derivability.

A Cartesian formula is built from atoms and equality using truth, finite conjunction and uniquely witnessed existential quantification. Uniqueness is proved relative to the theory before admitting the quantifier. In a finite-limit category, such a quantified relation projects monomorphically into the remaining context, so its semantics needs no arbitrary image operation.