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