Delimited control operators prove Double-negation Shift

TL;DR

This paper introduces an extension to minimal intuitionistic predicate logic using delimited control operators, enabling derivation of the Double-negation Shift schema while maintaining key logical properties.

Contribution

It presents a novel logical extension that incorporates delimited control operators to derive Double-negation Shift without losing disjunction and existence properties.

Findings

Successfully derives Double-negation Shift in extended logic

Preserves disjunction and existence properties in the extension

Demonstrates the utility of control operators in logical systems

Abstract

We propose an extension of minimal intuitionistic predicate logic, based on delimited control operators, that can derive the predicate-logic version of the Double-negation Shift schema, while preserving the disjunction and existence properties.