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.

For a commutative ring $R$, this locale is presented by basic opens $U_r$ recording membership in a multiplicatively closed prime filter. Products give intersections. A ring map induces a locale map in the opposite direction. The basic opens satisfy $U_r\vee U_s=1$ exactly when $(r,s)=R$, making unit-ideal calculations a substitute for choosing prime ideals.