 Ideally, a logic \(\mathfrak L\) has a sound and complete proof theory, that is, an accompanying deductive system whose theorems—the formulas provable in the system—are exactly the logical truths of \(\mathfrak  L\).[36]  There is such a system for SQML—for convenience, we’ll refer to it by setting “SQML” in italics: SQML. (We will follow this convention for logics generally.)