Related papers: Intuitionistic G\"odel-L\"ob logic, \`a la Simpson…
A focused proof system provides a normal form to cut-free proofs that structures the application of invertible and non-invertible inference rules. The focused proof system of Andreoli for linear logic has been applied to both the proof…
We prove a topological completeness theorem for the modal logic GLP containing operators $\langle\lambda\rangle$ for $\lambda \in$ Ord intended to capture progressively stronger notions of consistency in mathematical theories. We show that,…
Recent work on loglinear models in probabilistic constraint logic programming is applied to first-order probabilistic reasoning. Probabilities are defined directly on the proofs of atomic formulae, and by marginalisation on the atomic…
The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite model property holds for each of these logics have been long-standing open problems. It was…
We extend the meet-implication fragment of propositional intuitionistic logic with a meet-preserving modality. We give semantics based on semilattices and a duality result with a suitable notion of descriptive frame. As a consequence we…
We introduce a monotone modal analogue of the intuitionistic (normal) modal logic IK using a translation into a suitable (intuitionistic) first-order logic. We axiomatise the logic and give a semantics by means of intuitionistic…
Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality $!_r$ captures how many times a…
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…
We examine cyclic, non-well-founded and well-founded derivations in the provability logic $\mathsf{GLP}$. While allowing cyclic derivations does not change the system, the non-well-founded and well-founded derivations we consider define the…
This reports introduces a novel sound and complete semantics for first order intuitionistic logic, in the framework of category theory and by the computational interpretation of the logic based on the so-called Curry-Howard isomorphism.…
We present constructive provability logic, an intuitionstic modal logic that validates the L\"ob rule of G\"odel and L\"ob's provability logic by permitting logical reflection over provability. Two distinct variants of this logic, CPL and…
Well-known principles of induction include monotone induction and different sorts of non-monotone induction such as inflationary induction, induction over well-founded sets and iterated induction. In this work, we define a logic formalizing…
We report on the mechanization of (preference-based) conditional normative reasoning. Our focus is on Aqvist's system E for conditional obligation, and its extensions. Our mechanization is achieved via a shallow semantical embedding in…
We show that intuitionistic logic is deductively equivalent to Connexive Heyting Logic (CHL), hereby introduced as an example of a strong connexive logic with intuitive semantics. We use the reverse algebraisation paradigm: CHL is presented…
G\"odel's Incompleteness Theorems suggest that no single formal system can capture the entirety of one's mathematical beliefs, while pointing at a hierarchy of systems of increasing logical strength that make progressively more explicit…
Non-wellfounded proof systems impose a global condition called the global trace condition (GTC) on a derivation tree to ensure soundness. Providing a categorical characterisation of the GTC that guarantees soundness remains challenging due…
Full first order linear logic can be presented as an abstract logic programming language in Miller's system Forum, which yields a sensible operational interpretation in the 'proof search as computation' paradigm. However, Forum still has to…
Inquisitive modal logic, InqML, in its epistemic incarnation, extends standard epistemic logic to capture not just the information that agents have, but also the questions that they are interested in. We use the natural notion of…
Gottfried Leibniz embarked on a research program to prove all the Aristotelic categorical syllogisms by diagrammatic and algebraic methods. He succeeded in proving them by means of Euler diagrams, but didn't produce a manuscript with their…
An Isabelle/HOL formalisation of G\"odel's two incompleteness theorems is presented. The work follows \'Swierczkowski's detailed proof of the theorems using hereditarily finite (HF) set theory. Avoiding the usual arithmetical encodings of…