Related papers: Calibrating the negative interpretation
Earlier, the authors introduced the logic IntGC, which is an extension of intuitionistic propositional logic by two rules of inference mimicking the performance of Galois connections (Logic J. of the IGPL, 18:837-858, 2010). In this paper,…
We provide a characterization of those nonmonotonic inference operations C for which C(X) may be described as the set of all logical consequences of X together with some set of additional assumptions S(X) that depends anti-monotonically on…
We introduce the notions of triviality and order-triviality for global invariant types in an arbitrary first-order theory and show that they are well behaved in the NIP context. We show that these two notions agree for invariant global…
We develop a correspondence between the theory of sequential algorithms and classical reasoning, via Kreisel's no-counterexample interpretation. Our framework views realizers of the no-counterexample interpretation as dynamic processes…
The field of proof-theoretic semantics (P-tS) offers an alternative approach to meaning in logic that is based on inference and argument (rather than truth in a model). It has been successfully developed for various logics; in particular,…
A prototypical example of categorial grammars are those based on Lambek calculus, i.e. noncommutative intuitionistic linear logic. However, it has been noted that purely noncommutative operations are often not sufficient for modeling even…
Many semantical aspects of programming languages, such as their operational semantics and their type assignment calculi, are specified by describing appropriate proof systems. Recent research has identified two proof-theoretic features that…
We propose an extension of minimal intuitionistic predicate logic, based on delimited control operators, that can derive the predicate-logic version of the Double-negation Shift schema, while preserving the disjunction and existence…
We consider extensions of the language of Peano arithmetic by transfinitely iterated truth definitions satisfying uniform Tarskian biconditionals. Without further axioms, such theories are known to be conservative extensions of the original…
We construct an internal language for cartesian closed bicategories. Precisely, we introduce a type theory modelling the structure of a cartesian closed bicategory and show that its syntactic model satisfies an appropriate universal…
The paper treats 4 different fragments of first-order logic induced by their respective versions of Kripke style semantics for modal intuitionistic logic. In order to capture these fragments, the notion of asimulation is modified and…
We first recall some basic notions on minimalist grammars and on categorial grammars. Next we shortly introduce partially commutative linear logic, and our representation of minimalist grammars within this categorial system, the so-called…
In proof-theoretic semantics, meaning is based on inference. It may seen as the mathematical expression of the inferentialist interpretation of logic. Much recent work has focused on base-extension semantics, in which the validity of…
We combine the concepts of modal logics and many-valued logics in a general and comprehensive way. Namely, given any finite linearly ordered set of truth values and any set of propositional connectives defined by truth tables, we define the…
The proof theory and semantics of intuitionistic modal logics have been studied by Simpson in terms of Prawitz-style labelled natural deduction systems and Kripke models. An alternative to model-theoretic semantics is provided by…
An elementary rheory of concatenation is introduced and used to establish mutual interpretability of Robinson arithmetic, Minimal Predicative Set Theory, the quantifier-free part of Kirby's finitary set theory, and Adjunctive Set Theory,…
Short-circuit evaluation denotes the semantics of propositional connectives in which the second argument is evaluated only if the first argument does not suffice to determine the value of the expression. Short-circuit evaluation is widely…
This work contributes to the theory of judgment aggregation by discussing a number of significant non-classical logics. After adapting the standard framework of judgment aggregation to cope with non-classical logics, we discuss in…
In a recent paper, Herbelin developed a calculus dPA$^\omega$ in which constructive proofs for the axioms of countable and dependent choices could be derived via the encoding of a proof of countable universal quantification as a stream of…
Intuitionistic belief has been axiomatized by Artemov and Protopopescu as an extension of intuitionistic propositional logic by means of the distributivity scheme K, and of co-reflection $A\rightarrow\Box A$. This way, belief is interpreted…