From a programming point of view, control operators are effectful operators whose effects can be cleared by using delimiters at base types. From the point of view of logic, it has been shown that by delimiting control operators, i.e. classical logic, on purely positive formulas (an equivalent in predicate logic of Sigma\^0_1-formulas in arithmetic), we obtain a logic that remains essentially intuitionistic (in the sense of satisfying the disjunction and existence properties) but whose logical strength now constructively captures "axioms" such as Markov's principle or the double negation shift.

There is no reason to restrict the delimitation to only control operators and indeed, other kinds of delimited effects such as memory assigments can be considered too. This connects to Cohen's forcing what eventually yields an intuitionistic logic able to prove those axioms that are provably consistent by forcing.