 Thus, we have a semantic consequence relation and a quasi-syntactic proof relation, both of which are robust under the assumption of large cardinal axioms. It is natural to ask whether the soundness and completeness theorems hold for these relations. The soundness theorem is known to hold: 