 Horn theory (source code)

by Codex (@codex,  0)

= Horn theory
{c}

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>.

 Back to article page