Lewis meets Brouwer: constructive strict implication

DOI10.1016/J.INDAG.2017.10.003MaRDI QIDQ1688950zbMATH OpenOpenAlexFDO

Authors Tadeusz Litak, Albert Visser

Publication date 12 January 2018

Published in Indagationes Mathematicae. New Series (Search for Journal in Brave)

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

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Subsystems of classical logic (including intuitionistic logic) (03B20) First-order arithmetic and fragments (03F30)

Abstract: C. I. Lewis invented modern modal logic as a theory of "strict implication". Over the classical propositional calculus one can as well work with the unary box connective. Intuitionistically, however, the strict implication has greater expressive power than the box and allows to make distinctions invisible in the ordinary syntax. In particular, the logic determined by the most popular semantics of intuitionistic K becomes a proper extension of the minimal normal logic of the binary connective. Even an extension of this minimal logic with the "strength" axiom, classically near-trivial, preserves the distinction between the binary and the unary setting. In fact, this distinction and the strong constructive strict implication itself has been also discovered by the functional programming community in their study of "arrows" as contrasted with "idioms". Our particular focus is on arithmetical interpretations of the intuitionistic strict implication in terms of preservativity in extensions of Heyting's Arithmetic.

Recommendations

• scientific article; zbMATH DE number 1778908
• scientific article; zbMATH DE number 2170850
• Weak Logics with Strict Implication
• Begründung einer strengen Implikation
• From intuitionism to Brouwer's modal logic

Cites work

• scientific article; zbMATH DE number 3950473 (Why is no real title available?)
• scientific article; zbMATH DE number 956473 (Why is no real title available?)
• scientific article; zbMATH DE number 47777 (Why is no real title available?)
• scientific article; zbMATH DE number 192927 (Why is no real title available?)
• scientific article; zbMATH DE number 3494368 (Why is no real title available?)
• scientific article; zbMATH DE number 1215477 (Why is no real title available?)
• scientific article; zbMATH DE number 1215499 (Why is no real title available?)
• scientific article; zbMATH DE number 1303434 (Why is no real title available?)
• scientific article; zbMATH DE number 1735881 (Why is no real title available?)
• scientific article; zbMATH DE number 1170091 (Why is no real title available?)
• scientific article; zbMATH DE number 1489627 (Why is no real title available?)
• scientific article; zbMATH DE number 218496 (Why is no real title available?)
• scientific article; zbMATH DE number 218514 (Why is no real title available?)
• scientific article; zbMATH DE number 219032 (Why is no real title available?)
• scientific article; zbMATH DE number 757639 (Why is no real title available?)
• scientific article; zbMATH DE number 1431908 (Why is no real title available?)
• scientific article; zbMATH DE number 4195937 (Why is no real title available?)
• scientific article; zbMATH DE number 5066367 (Why is no real title available?)
• scientific article; zbMATH DE number 2242586 (Why is no real title available?)
• A Survey of Propositional Realizability Logic
• A closer look at some subintuitionistic logics
• A formalized proof of strong normalization for guarded recursive types
• A model of countable nondeterminism in guarded type theory
• A model of guarded recursion with clock synchronisation
• A modification of Parry's analytic implication
• A note on strict implication (1935)
• A semantic model for graphical user interfaces
• A smart child of Peano's
• A type theory for productive coprogramming via guarded recursion
• A very modal model of a modern, major, general type system
• Analytic implication
• Applicative programming with effects
• Biological Perspectives Irreversible Lithium-Induced Neuropathy: Two Cases
• Bounded distributive lattices with strict implication
• Brouwerian Semilattices
• Closed Fragments of Provability Logics of Constructive Theories
• Computational interpretations of linear logic
• Computational types from a logical perspective
• Constructive modalities with provability smack
• Constructive validity is nonarithmetic
• Constructivism in mathematics. An introduction. Volume I
• Cut-free tableau calculi for some propositional normal modal logics
• Editor's introduction to C. I. Lewis and C. H. Langford `A note on strict implication'
• Epistemic updates on algebras
• Esakia style duality for implicative semilattices
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• Generalising monads to arrows
• Grothendieck Topology as Geometric Modality
• Guard your daggers and traces: properties of guarded (co-)recursion
• Guarded dependent type theory with coinductive types
• Higher-order functional reactive programming in bounded space
• INTUITIONISTIC EPISTEMIC LOGIC
• Idioms are oblivious, arrows are meticulous, monads are promiscuous
• Impredicative concurrent abstract predicates
• In memoriam: Clarence Irving Lewis (1883--1964)
• Incompleteness in intuitionistic metamathematics
• Intensional type theory with guarded recursive types qua fixed points on universes
• Intermediate logics and the de Jongh property
• Interpolation in fragments of intuitionistic propositional logic
• Intuitionistic epistemic logic, Kripke models and Fitch's paradox
• Iris: monoids and invariants as an orthogonal basis for concurrent reasoning
• Lectures on the Curry-Howard isomorphism
• Lewis meets Brouwer: constructive strict implication
• Lifschitz' realizability
• Linear logic
• MacNeille completions and canonical extensions
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Models for normal intuitionistic modal logics
• ModuRes: a Coq library for modular reasoning about concurrent higher-order imperative programming languages
• Monad as modality
• Notions of computation and monads
• On intuitionistic modal epistemic logic
• On the completenes principle: A study of provability in heyting's arithmetic and extensions
• On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Predicate Logics of Constructive Arithmetical Theories
• Preservativity logic: An analogue of interpretability logic for constructive theories
• Productive coprogramming with guarded recursion
• Programming and reasoning with guarded recursion for coinductive types
• Properties of Intuitionistic Provability and Preservativity Logics
• Propositional lax logic
• Provability interpretations of modal logic
• Provability logic—a short introduction
• Provability: The emergence of a mathematical modality
• Rules and arithmetics
• Self-reference and modal logic
• Sequent Calculus in the Topos of Trees
• Shavrukov's theorem on the subalgebras of diagonalizable algebras for theories containing \(I\Delta_ 0 + \exp\)
• Solution of a problem of Leon Henkin
• Strict implication, deducibility and the deduction theorem
• Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
• The Henkin sentence
• The Logic of Bunched Implications
• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
• The deduction theorem in a functional calculus of first order based on strict implication
• The first axiomatization of relevant logic
• The interpretability logic of Peano arithmetic
• The logic of \(\Pi_ 1\)-conservativity
• The non-reflexive counterpart of Grz
• The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations
• The semantics and proof theory of the logic of bunched implications
• Transitive primal infon logic
• Weak Logics with Strict Implication
• Why the theory R is special

Cited in

(14)

• On weak Lewis distributive lattices
• On a generalization of Heyting algebras. I
• The G4i analogue of a G3i sequent calculus
• Intuitionistic sets and numbers: small set theory and Heyting arithmetic
• On geometric implications
• Stable canonical rules for intuitionistic modal logics
• An overview of Verbrugge semantics, a.k.a. generalised Veltman semantics
• Lewisian fixed points. I: Two incomparable constructions
• Proof theory for Lax Logic
• Monotone subintuitionistic logic: duality and transfer results
• Implication via spacetime
• Intuitionistic -calculus with the Lewis arrow
• Lewis meets Brouwer: constructive strict implication
• Editor's introduction to C. I. Lewis and C. H. Langford `A note on strict implication'

Describes a project that uses

Uses Software

• ModuRes

This page was built for publication: Lewis meets Brouwer: constructive strict implication

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