Geometric syntactic topology
= Geometric syntactic topology
{title2=$J_{\mathbb T}$}
A family of definable arrows covers a formula when the theory proves that their images jointly exhaust that formula. Such covers encode disjunction and existential quantification. The resulting <site> presents the <classifying topos> of the <geometric theory>. Adding geometric axioms adds covering sieves, yielding the <duality between geometric quotients and subtoposes>.