Conservative syntactic model (source code)

= Conservative syntactic model

The canonical model interprets each sort as its truth-context object, each operation by its term graph and each relation by its atomic subobject. A coherent formula is interpreted by its own formula-in-context object. Consequently a <coherent sequent> holds in this model exactly when it is derivable in the theory.