Delimited control operators prove double-negation shift

DOI10.1016/J.APAL.2011.12.008MaRDI QIDQ450950zbMATHOpenAlexFDO

Authors Danko Ilik

Publication date 26 September 2012

Published in Annals of Pure and Applied Logic (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1012.0929

zbMATH Keywords

intermediate logicdisjunction propertydelimited control operatorsdouble-negation shiftexistence propertyextension of minimal intuitionistic predicate logic

Mathematics Subject Classification ID

Subsystems of classical logic (including intuitionistic logic) (03B20) Intermediate logics (03B55) Logic in computer science (03B70) Metamathematics of constructive systems (03F50)

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.

Recommendations

• A direct version of Veldman's proof of open induction on Cantor space via delimited control operators
• The bounded functional interpretation of the double negation shift
• THEORETICAL PEARL: A simple proof of a folklore theorem about delimited control
• The Peirce translation and the double negation shift
• On subexponentials, synthetic connectives, and multi-level delimited control

Cites work

• scientific article; zbMATH DE number 5204708 (Why is no real title available?)
• scientific article; zbMATH DE number 3222098 (Why is no real title available?)
• scientific article; zbMATH DE number 3231083 (Why is no real title available?)
• scientific article; zbMATH DE number 3259893 (Why is no real title available?)
• scientific article; zbMATH DE number 2222013 (Why is no real title available?)
• A Constructive Proof of Dependent Choice, Compatible with Classical Logic
• A Functional calculus of first order based on strict implication
• A Substructural Type System for Delimited Continuations
• A generalization of jumps and labels
• A type-theoretic foundation of delimited continuations
• An introduction to Landin's ``A generalization of jumps and labels
• Applied Proof Theory: Proof Interpretations and Their Use in Mathematics
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• Constructivism in mathematics. An introduction. Volume I
• Delimited control operators prove double-negation shift
• Extensional Gödel functional interpretation. A consistency proof of classical analysis
• Intuitionistic logic and the creative subject
• Intuitionistische Untersuchungen der formalistischen Logik
• Lectures on the Curry-Howard isomorphism
• Logical Approaches to Computational Barriers
• On the concepts of completeness and interpretation of formal systems
• On the unity of duality
• Polymorphic Delimited Continuations
• Realizability algebras. II: New models of \(\mathrm{ZF} + \mathrm{DC}\)
• Realizability algebras: a program to well order \(\mathbb R\)
• Representing Control: a Study of the CPS Transformation
• The deduction theorem in a functional calculus of first order based on strict implication
• Typed lambda-calculus in classical Zermelo-Fraenkel set theory

Cited in

(8)

• scientific article; zbMATH DE number 7649968 (Why is no real title available?)
• An intuitionistic formula hierarchy based on high‐school identities
• Interrelation between weak fragments of double negation shift and related principles
• Type directed partial evaluation for level-1 shift and reset
• On the unification of classical, intuitionistic and affine logics
• Delimited control operators prove double-negation shift
• Minimum classical extensions of constructive theories
• A direct version of Veldman's proof of open induction on Cantor space via delimited control operators

This page was built for publication: Delimited control operators prove double-negation shift

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q450950)