Lewis meets Brouwer: constructive strict implication

DOI10.1016/j.indag.2017.10.003zbMath1436.03137arXiv1708.02143OpenAlexW3101546648MaRDI QIDQ1688950

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) First-order arithmetic and fragments (03F30) Subsystems of classical logic (including intuitionistic logic) (03B20)

Related Items

Monotone subintuitionistic logic: duality and transfer results, Implication via spacetime, Lewis meets Brouwer: constructive strict implication, The G4i analogue of a G3i sequent calculus

Uses Software

• ModuRes

Cites Work

• Strict implication, deducibility and the deduction theorem
• The deduction theorem in a functional calculus of first order based on strict implication
• Rules and arithmetics
• Substitutions of \(\Sigma_1^0\)-sentences: Explorations between intuitionistic propositional logic and intuitionistic arithmetic
• A model of guarded recursion with clock synchronisation
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Linear logic
• Intermediate logics and the de Jongh property
• Computational interpretations of linear logic
• Intuitionistic epistemic logic, Kripke models and Fitch's paradox
• The \(\Sigma_1\)-provability logic of \(\mathsf{HA}\)
• The logic of \(\Pi_ 1\)-conservativity
• Notions of computation and monads
• Lectures on the Curry-Howard isomorphism
• Self-reference and modal logic
• Analytic implication
• Models for normal intuitionistic modal logics
• Provability: The emergence of a mathematical modality
• Incompleteness in intuitionistic metamathematics
• On intuitionistic modal epistemic logic
• Constructivism in mathematics. An introduction. Volume I
• The first axiomatization of relevant logic
• Provability interpretations of modal logic
• Shavrukov's theorem on the subalgebras of diagonalizable algebras for theories containing \(I\Delta_ 0 + \exp\)
• A smart child of Peano's
• Propositional lax logic
• Monad as modality
• A closer look at some subintuitionistic logics
• Generalising monads to arrows
• Lewis meets Brouwer: constructive strict implication
• Possible worlds and resources: The semantics of \(\mathbf{BI}\)
• Esakia style duality for implicative semilattices
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• The semantics and proof theory of the logic of bunched implications
• In memoriam: Clarence Irving Lewis (1883--1964)
• A modification of Parry's analytic implication
• Cut-free tableau calculi for some propositional normal modal logics
• On the limit existence principles in elementary arithmetic and \(\varSigma_{n}^{0}\)-consequences of theories
• A Formalized Proof of Strong Normalization for Guarded Recursive Types
• Guarded Dependent Type Theory with Coinductive Types
• Iris
• Epistemic Updates on Algebras
• Higher-order functional reactive programming in bounded space
• ModuRes: A Coq Library for Modular Reasoning About Concurrent Higher-Order Imperative Programming Languages
• Sequent Calculus in the Topos of Trees
• Programming and Reasoning with Guarded Recursion for Coinductive Types
• A Light Modality for Recursion
• First steps in synthetic guarded domain theory: step-indexing in the topos of trees
• A very modal model of a modern, major, general type system
• Solution of a problem of Leon Henkin
• Properties of Intuitionistic Provability and Preservativity Logics
• Predicate Logics of Constructive Arithmetical Theories
• The Henkin Sentence
• Lifschitz' realizability
• Interpolation in fragments of intuitionistic propositional logic
• A Survey of Propositional Realizability Logic
• Closed Fragments of Provability Logics of Constructive Theories
• Weak Logics with Strict Implication
• Brouwerian Semilattices
• Grothendieck Topology as Geometric Modality
• The nonderivability in intuitionistic formal systems of theorems on the continuity of effective operations
• Computational types from a logical perspective
• The Logic of Bunched Implications
• Provability logic—a short introduction
• Biological Perspectives Irreversible Lithium-Induced Neuropathy: Two Cases
• Guard Your Daggers and Traces: Properties of Guarded (Co-)recursion
• A type theory for productive coprogramming via guarded recursion
• Bounded distributive lattices with strict implication
• On the completenes principle: A study of provability in heyting's arithmetic and extensions
• Preservativity logic: An analogue of interpretability logic for constructive theories
• TRANSITIVE PRIMAL INFON LOGIC
• Editor's Introduction to C.I. Lewis and C.H. Langford ‘A Note on Strict Implication’
• A Note on Strict Implication (1935)
• Idioms are Oblivious, Arrows are Meticulous, Monads are Promiscuous
• A Model of Countable Nondeterminism in Guarded Type Theory
• A semantic model for graphical user interfaces
• Constructive validity is nonarithmetic
• The interpretability logic of Peano arithmetic
• Productive coprogramming with guarded recursion
• Constructive Modalities with Provability Smack
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• Impredicative Concurrent Abstract Predicates
• Applicative programming with effects
• MacNeille completions and canonical extensions
• INTUITIONISTIC EPISTEMIC LOGIC