Related papers: Topological interpretations of provability logic
The system of intuitionistic modal logic ${\bf IEL}^{-}$ was proposed by S. Artemov and T. Protopopescu as the intuitionistic version of belief logic \cite{Artemov}. We construct the modal lambda calculus which is Curry-Howard isomorphic to…
We study two notions of definability for classes of relational structures based on modal extensions of {\L}ukasiewicz finitely valued-logics. The main results of the paper are the equivalent of the Goldblatt - Thomason theorem for these…
We provide the first (non-labelled) sequent calculi for bimodal provability logics with "usual" provability predicates. In particular, we introduce calculi for the logics CS, CSM and ER. Additionally, we present non-wellfounded versions of…
This paper investigates the contingency of logic within the framework of possible world semantics. Possible world semantics captures the meaning of necessitation, i.e., a statement is necessarily true if it holds in all possible worlds.…
In a seminal paper from 1985, Sistla and Clarke showed that satisfiability for Linear Temporal Logic (LTL) is either NP-complete or PSPACE-complete, depending on the set of temporal operators used. If, in contrast, the set of propositional…
In arXiv:1604.08705 we introduced the propositional modal logic $\textbf{TSC}$ (which stands for Turing Schmerl Calculus) which adequately describes the provable interrelations between different kinds of Turing progressions. In…
Logic $L$ was introduced by Lewitzka [7] as a modal system that combines intuitionistic and classical logic: $L$ is a conservative extension of CPC and it contains a copy of IPC via the embedding $\varphi\mapsto\square\varphi$. In this…
The Alexandrov topology affords a well-known semantics of modal necessity and possibility. This paper develops an Alexandrov topological semantics of intuitionistic propositional modal logic internally in any elementary topos. This is done…
In this paper we investigate the complexity-theoretical aspects of cyclic and non-wellfounded proofs in the context of parsimonious logic, a variant of linear logic where the exponential modality ! is interpreted as a constructor for…
In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between…
We introduce and develop a topological semantics of conservativity logics and interpretability logics. We prove the topological compactness theorem of consistent normal extensions of the conservativity logic $\mathbf{CL}$ by extending…
A semantics is given to possibilistic logic, a logic that handles weighted classical logic formulae, and where weights are interpreted as lower bounds on degrees of certainty or possibility, in the sense of Zadeh's possibility theory. The…
Intuitionistic modal logics (IMLs) extend intuitionistic propositional logic with modalities such as the box and diamond connectives. Advances in the study of IMLs have inspired several applications in programming languages via the…
Topological metals are special conducting materials with gapless band structures and nontrivial edge-localized resonances, whose discovery has proved elusive because the traditional topological classification methods do not apply in this…
We study the logic FO(~), the extension of first-order logic with team semantics by unrestricted Boolean negation. It was recently shown axiomatizable, but otherwise has not yet received much attention in questions of computational…
In 1994 Jech gave a model theoretic proof of G\"odel's second incompleteness theorem for Zermelo-Fraenkel set theory in the following form: ZF does not prove that ZF has a model. Kotlarski showed that Jech's proof can be adapted to Peano…
We propose a nonmonotonic Description Logic of typicality able to account for the phenomenon of concept combination of prototypical concepts. The proposed logic relies on the logic of typicality ALC TR, whose semantics is based on the…
A co-valuation is, essentially, a minimal finite cover. We introduce a logic based on co-valuations, which play the role of valuations of free variables in classical first-order logic, and show that the fundamental tools of model theory --…
The topological interpretation of modal logics provides descriptive languages and proof systems for reasoning about points of topological spaces. Recent work has been devoted to model checking of spatial logics on discrete spatial…
In arXiv:1604.08705 the authors introduced the propositional modal logic $\textbf{TSC}$ (which stands for Turing Schmerl Calculus) which adequately describes the provable interrelations between different kinds of Turing progressions. The…