Delimited control operators prove double-negation shift

DOI10.1016/J.APAL.2011.12.008zbMATH Open1251.03033arXiv1012.0929OpenAlexW1491272572MaRDI QIDQ450950FDOQ450950

Danko Ilik

Publication date: 26 September 2012

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

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.

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

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

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)

Cites Work

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

Cited In (6)

• Title not available (Why is that?)
• An intuitionistic formula hierarchy based on high‐school identities
• Title not available (Why is that?)
• Delimited control operators prove double-negation shift
• Minimum classical extensions of constructive theories
• On the unification of classical, intuitionistic and affine logics

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)