= Classical completeness of coherent theories
A coherent sequent true in all set models of a coherent theory is coherently derivable. A generic underivable sequent remains false after the <Boolean cover by a generic quasi-closed subtopos>. Slice over its nonzero Boolean counterexample to show classical consistency of the theory with a named tuple satisfying the antecedent and negated consequent. The <Henkin construction> then gives a set-valued countermodel. This argument does not assume that every Boolean topos has points.
Back to article page
