 When the details of the formalism are not important, from now on we follow Troelstra and van Dalen [1988] in letting “\(\mathbf{IQC}\)” or “\(\mathbf{IPC}\)” refer to any formal system for intuitionistic predicate or propositional logic respectively, and similarly “\(\mathbf{CQC}\)” and “\(\mathbf{CPC}\)” for classical predicate and propositional logic.