Propositional geometric theory
= Propositional geometric theory
A geometric theory with only nullary relation symbols has formulas built from primitive propositions by finite conjunctions and set-indexed disjunctions. Its sequents present a <frame>; its <locale> carries a canonical model in its <sheaf topos>, where a proposition is interpreted as the corresponding open subterminal sheaf.