Constructive Modalities with Provability Smack

DOI10.1007/978-94-017-8860-1_8zbMath1350.03020arXiv1708.05607OpenAlexW88360193MaRDI QIDQ5255796

Tadeusz Litak

Publication date: 19 June 2015

Published in: Leo Esakia on Duality in Modal and Intuitionistic Logics (Search for Journal in Brave)

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

zbMATH Keywords

intuitionistic modal logictopos of treesconstructive fixpointspoint-free derivativescattered toposes

Mathematics Subject Classification ID

Modal logic (including the logic of norms) (03B45) Categorical logic, topoi (03G30) Subsystems of classical logic (including intuitionistic logic) (03B20) Provability logics and related algebras (e.g., diagonalizable algebras) (03F45)

Related Items (11)

Interconnection of the lattices of extensions of four logics ⋮ Lewis meets Brouwer: constructive strict implication ⋮ Admissible rules for six intuitionistic modal logics ⋮ The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types ⋮ Mathematical logic: proof theory, constructive mathematics. Abstracts from the workshop held November 8--14, 2020 (hybrid meeting) ⋮ Sequent calculi for intuitionistic Gödel-Löb logic ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Uniform interpolation and the existence of sequent calculi ⋮ Modal Logics that Bound the Circumference of Transitive Frames ⋮ The G4i analogue of a G3i sequent calculus

Cites Work

• 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
• Kripke sheaf completeness of some superintuitionistic predicate logics with a weakened constant domains principle
• Presheaf semantics and independence results for some non-classical first- order logics
• Update to ``A survey of abstract algebraic logic
• On modal \(\mu \)-calculus and Gödel-Löb logic
• On superintuitionistic logics as fragments of proof logic extensions
• Models for normal intuitionistic modal logics
• Models for stronger normal intuitionistic modal logics
• A modal calculus analogous to K4W, based on intuitionistic propositional logic, \(I^0\)
• Topoi. The categorial analysis of logic
• Finite approximability of the \(I^\delta\) calculus and the existence of an extension having no model
• Provability: The emergence of a mathematical modality
• Sheaves in geometry and logic: a first introduction to topos theory
• An algebraic approach to non-classical logics
• Provability interpretations of modal logic
• An effective fixed-point theorem in intuitionistic diagonalizable algebras. (The algebraization of the theories which express Theor. IX.)
• Calculating self-referential statements. I: Explicit calculations
• Propositional lax logic
• A survey of abstract algebraic logic
• Mathematical modal logic: A view of its evolution
• On an intuitionistic modal logic
• Esakia style duality for implicative semilattices
• Scattered toposes
• Modal frame correspondences and fixed-points
• Finite models constructed from canonical formulas
• Beyond Rasiowa's algebraic approach to non-classical logics
• Cut-free tableau calculi for some propositional normal modal logics
• On the admissible rules of intuitionistic propositional logic
• A judgmental reconstruction of modal logic
• The Russell–Prawitz modality
• Access Control in a Core Calculus of Dependency
• Well-Pointed Coalgebras (Extended Abstract)
• Some modal aspects of XPath
• Extending Type Theory with Forcing
• Cover semantics for quantified lax logic
• 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
• The Uses and Abuses of the History of Topos Theory
• SUBFORMULA AND SEPARATION PROPERTIES IN NATURAL DEDUCTION VIA SMALL KRIPKE MODELS
• The modalized Heyting calculus: a conservative modal extension of the Intuitionistic Logic ★
• Logics containing K4. Part II
• Algebraizable logics
• Brouwerian Semilattices
• Grothendieck Topology as Geometric Modality
• Computational types from a logical perspective
• Categories for Types
• Incompleteness Results in Kripke Bundle Semantics
• Priestley duality, a Sahlqvist theorem and a Goldblatt-Thomason theorem for positive modal logic
• A semantic model for graphical user interfaces
• Productive coprogramming with guarded recursion
• On the Blok-Esakia Theorem
• Logic KM: A Biography
• Cantor-Bendixson Properties of the Assembly of a Frame
• Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes
• Foundations of Software Science and Computation Structures
• Applicative programming with effects
• A Modal Deconstruction of Access Control Logics
• The separation theorem of intuitionist propositional calculus
• The elimination theorem when modality is present
• Processes, Terms and Cycles: Steps on the Road to Infinity

This page was built for publication: Constructive Modalities with Provability Smack