Citations of:
Proof analysis in intermediate logics
Archive for Mathematical Logic 51 (12):7192 (2012)
Add citations
You must login to add citations.


This paper shows how to derive nested calculi from labelled calculi for propositional intuitionistic logic and firstorder intuitionistic logic with constant domains, thus connecting the general results for labelled calculi with the more refined formalism of nested sequents. The extraction of nested calculi from labelled calculi obtains via considerations pertaining to the elimination of structural rules in labelled derivations. Each aspect of the extraction process is motivated and detailed, showing that each nested calculus inherits favorable prooftheoretic properties from its associated (...) 



We characterise the intermediate logics which admit a cutfree hypersequent calculus of the form \, where \ is the hypersequent counterpart of the sequent calculus \ for propositional intuitionistic logic, and \ is a set of socalled structural hypersequent rules, i.e., rules not involving any logical connectives. The characterisation of this class of intermediate logics is presented both in terms of the algebraic and the relational semantics for intermediate logics. We discuss various—positive as well as negative—consequences of this characterisation. 

This paper contends that Stoic logic (i.e. Stoic analysis) deserves more attention from contemporary logicians. It sets out how, compared with contemporary propositional calculi, Stoic analysis is closest to methods of backward proof search for Gentzeninspired substructural sequent logics, as they have been developed in logic programming and structural proof theory, and produces its proof search calculus in tree form. It shows how multiple similarities to Gentzen sequent systems combine with intriguing dissimilarities that may enrich contemporary discussion. Much of Stoic (...) 

ABSTRACTMonoidal logics were introduced as a foundational framework to analyze the proof theory of logical systems. Inspired by Lambek's seminal work in categorical logic, the objective is to defin... 

Monoidal logics were introduced as a foundational framework to analyse the proof theory of deontic logic. Building on Lambek’s work in categorical logic, logical systems are defined as deductive systems, that is, as collections of equivalence classes of proofs satisfying specific rules and axiom schemata. This approach enables the classification of deductive systems with respect to their categorical structure. When looking at their proof theory, however, one can see that there are similarities between monoidal and substructural logics. The purpose of (...) 

Antirealist epistemic conceptions of truth imply what is called the knowability principle: All truths are possibly known. The principle can be formalized in a bimodal propositional logic, with an alethic modality ${\diamondsuit}$ and an epistemic modality ${\mathcal{K}}$, by the axiom scheme ${A \supset \diamondsuit \mathcal{K} A}$. The use of classical logic and minimal assumptions about the two modalities lead to the paradoxical conclusion that all truths are known, ${A \supset \mathcal{K} A}$. A Gentzenstyle reconstruction of the Church–Fitch paradox is presented (...) 

The paper settles an open question concerning Negristyle labeled sequent calculi for modal logics and also, indirectly, other proof systems which make (more or less) explicit use of semantic parameters in the syntax and are thus subsumed by labeled calculi, like Brünnler’s deep sequent calculi, Poggiolesi’s treehypersequent calculi and Fitting’s prefixed tableau systems. Specifically, the main result we prove (through a semantic argument) is that labeled calculi for the modal logics K and D remain complete w.r.t. valid sequents whose relational (...) 

The logic of Conditional Beliefs has been introduced by Board, Baltag, and Smets to reason about knowledge and revisable beliefs in a multiagent setting. In this article both the semantics and the proof theory for this logic are studied. First, a natural semantics forCDLis defined in terms of neighbourhood models, a multiagent generalisation of Lewis’ spheres models, and it is shown that the axiomatization ofCDLis sound and complete with respect to this semantics. Second, it is shown that the neighbourhood semantics (...) 

That every firstorder theory has a coherent conservative extension is regarded by some as obvious, even trivial, and by others as not at all obvious, but instead remarkable and valuable; the result is in any case neither sufficiently wellknown nor easily found in the literature. Various approaches to the result are presented and discussed in detail, including one inspired by a problem in the proof theory of intermediate logics that led us to the proof of the present paper. It can (...) 



Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal the Ecumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that (...) 

The work is concerned with the so called display property of display logic. The motivation behind it is discussed and challenged. It is shown using one display calculus for intuitionistic logic as an example that the display property can be abandoned without losing subformula, cut elimination and completeness properties in such a way that results in additional expressive power of the system. This is done by disentangling structural connectives so that they are no longer contextsensitive. A recipe for characterizing structural (...) 

A comparison is given between two conditions used to define logical constants: Belnap's uniqueness and Hacking's deducibility of identicals. It is shown that, in spite of some surface similarities, there is a deep difference between them. On the one hand, deducibility of identicals turns out to be a weaker and less demanding condition than uniqueness. On the other hand, deducibility of identicals is shown to be more faithful to the inferentialist perspective, permitting definition of genuinely prooftheoretical concepts. This kind of (...) 

Proofs and countermodels are the two sides of completeness proofs, but, in general, failure to find one does not automatically give the other. The limitation is encountered also for decidable nonclassical logics in traditional completeness proofs based on Henkin’s method of maximal consistent sets of formulas. A method is presented that makes it possible to establish completeness in a direct way: For any given sequent either a proof in the given logical system or a countermodel in the corresponding frame class (...) 

Justification logics are modallike logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modaljustification logics. Using a method due to Sara Negri, we internalize the Kripkestyle semantics of justification and modaljustification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the (...) 