ABSTRACT. A useful modular semantics is an important property of any proof system: it can be used to characterize important syntactic properties of the system, provide insights into its underlying logic, and in many cases induce a decision procedure for it. Recent developments in the field of paraconsistent logics are an interesting case which exemplifies the cross-fertilization between semantic explorations and proof theoretical developments. In this talk I will survey the framework of non-deterministic semantics and its proof-theoretical applications, and demonstrate how non-deterministic semantics pushed forward the development of analytic Gentzen-type calculi for the large family of Logics of Formal Inconsistency.

ABSTRACT. We study the question of when a given set of derivable rules in some basic analytic propositional sequent calculus forms itself an analytic calculus. First, a general syntactic criterion for analyticity in the family of pure sequent calculi is presented. Next, given a basic calculus admitting this criterion, we provide a method to construct weaker pure calculi by collecting simple derivable rules of the basic calculus. The obtained calculi are analytic-by-construction. While the criterion and the method are completely syntactic, our proofs are semantic, based on interpretation of sequent calculi via non-deterministic valuation functions. In particular, this method captures calculi for a wide variety of paraconsistent logics, as well as some extensions of Gurevich and Neeman's primal infon logic.

ABSTRACT. In this talk I will consider the question of how to compare and evaluate the expressive strength of different formats of Gentzen-style systems. More precisely, the general question is which logics can be captured in the different frameworks. Of course some results are clear: e.g. since every standard sequent can be seen as a hypersequent with only one component or as a nested sequent without the nesting, every logic which can be captured in the framework of standard sequent calculus can be captured in the framework of hypersequent or nested sequent calculi as well. Other results are given by explicitly translating one framework into another, see e.g. [Goré and Ramanayake:2012].

While such results certainly establish important connections between the different frameworks, they only provide information on the expressive strength of one Gentzen-style framework relative to another one. Yet we are also interested in the absolute expressive strength and in particular the limits of what can be expressed in the different frameworks in a meaningful way. The qualification "in a meaningful way'' here is important, since of course given any set A of formulae the sequent calculus with groundsequents =>a for every a in A will serve to derive exactly the formulae in A, even in a cut-free way. Thus to make this question non-trivial we also need to restrict the format of the rules in the different frameworks.

Comparing the different frameworks and formats of rules finally can be done by identifying characterisations for them in a single common framework. Since we would like to compare extensions of sequent calculus, this should be a framework outside the class of Gentzen-style frameworks, and ideally the characterisations should provide a way of quickly determining which Gentzen-style framework is suitable for a particular logic. For this purpose here we choose the framework of Hilbert-style axiom systems. This gives a high degree of flexibility and allows in particular to capture non-normal modal logics and logics based on other than classical propositional logic. A characterisation of a specific Gentzen-style framework together with a specific format of rules then is given by an ideally purely syntactically defined class of axioms together with translations from rules of the considered format and framework into axioms of this class and vice versa. The prime example for this method is Kracht's result characterising those modal temporal logics which can be captured by structural rules in a display calculus satisfying Belnap's conditions for cut elimination as exactly the logics axiomatisable by primitive axioms [Kracht:1996]. Another example is the characterisation of structural rules in a sequent or hypersequent calculus for substructural logics by certain levels of the substructural hierarchy from [Ciabattoni et al:2008]. Apart from providing a first step for the construction of analytic calculi from Hilbert axioms, this method also yields a way to show limitative results: By showing that a certain logic cannot be axiomatised by axioms of a specific (syntactically given) form we can show that the logic cannot be captured by the framework and format of rules corresponding to this class of axioms.

In this talk I will discuss some recent results in this spirit concerning logical rules of different formats in the frameworks of standard sequent calculi and hypersequent calculi. The logics under consideration are propositional modal logics such as Gödel Löb logic GL or the logic of 2-transitive Kripke frames, and more generally, extensions of classical or intuitionistic propositional logic with additional not necessarily unary connectives.

ABSTRACT. This paper develops sequent calculi for several classical modal logics. Utilizing a polymodal translation of the standard modal language, we are able to establish a base system for the minimal classical modal logic from which we generate extensions in a modular, and uniform, manner. We also briefly suggest potential applications to epistemic logic.

ABSTRACT. We prove Lyndon interpolation for the modal mu-calculus by applying so-called circular proofs. One of the proof systems for the modal mu-calculus is based on non-well-founded derivation trees with a global condition which roughly says that in each infinite branch, there must be an outermost greatest fixed point unfolded infinitely many often. We analyse regular proof trees (so-called circular proofs) in this proof system and obtain the Lyndon interpolation for the modal mu-calculus.

ABSTRACT. We present recent developments and discuss open questions concerning syntactic cut-elimination for modal fixed point logics.

ABSTRACT. The range of non-classical logics has been rapidly expanding, driven by influences from other fields which have opened up new opportunities for applications. However, the hurdles preventing a standard proof-theoretic development for these logics are due precisely to some of their defining features which make them suitable for applications, such as e.g. their not being closed under uniform substitution, or the fact that (the semantic interpretations of) key connectives are not adjoints.

These difficulties caused the existing proposals in literature to be often ad hoc, not easily generalisable, and more in general lacking a smooth proof-theoretic behaviour. In particular, the difficulty in smoothly transferring results from one logic to another is a problem in itself, since these logics typically come in large families (consider for instance the family of dynamic logics), and hence proof-theoretic approaches which uniformly apply to each logic in a given family are in high demand.

In this talk we focus on the core technical aspects of a proof-theoretic methodology and set-up closely linked to Belnap's display logic and Sambin's basic logic. The present set-up, which we refer to as display-type calculi, generalizes display calculi in two aspects: by allowing multi-type languages, and by dropping the full display property. The generalisation to a multi-type environment makes it possible to introduce specific tools enhancing expressivity, which have proved useful e.g. for a smooth proof-theoretic treatment of multi-modal and dynamic logics. The generalisation to a setting in which full display property is not required makes it possible to account for logics which admit connectives which are neither adjoints nor residuals.

One technical aspect which guarantees the cut elimination meta-theorem to go through for display-type calculi, even in the absence of the full display property, concerns the strengthening of the separation property (requiring principal formulas in introduction rules to appear in isolation) to the visibility property. Visibility requires all active formulas in introduction rules to occur in isolation. This property was recognized to be crucial for the cut elimination theorem of basic logic. However, in the present set-up of display-type calculi, visibility is also weakened, in the sense that, in order to account for logics that are not closed under uniform substitution, principal formulas in axioms are not required to occur in isolation.

In the proposed talk, we will illustrate the basic principles of the multi-type environment, and also how the above combination of weakenings, strengthenings of the separation property concurs to guaranteeing the cut elimination meta-theorem for display-type calculi. Time permitting, we will also discuss some difficulties that still arise in the case of PDL and some ideas towards treating predicative logics.

ABSTRACT. I will talk about ongoing work with Matteo Mio (University of Cambridge) to build useful proof systems for quantitative fixed-point logics. Our approach adapts cyclic-proof-based sequent calculi to the quantitative setting. Several technical issues arise, not all of which have been resolved. The overall aim of the programme is to develop machinery for reasoning about probabilistic concurrent systems. But the talk will focus on proof-theoretic issues, in a purely logical setting.

ABSTRACT. In this talk we show for each of the modal axioms d, t, b, 4, and 5 an equivalent set of inference rules in a nested sequent system, such that, when added to the basic system for the intuitionistic modal logic IK, the resulting system admits cut elimination. The result is similar to the one presented at "Gentzen Systems and Beyond 2011" about classical modal logics. We use a combination of structural and logical rules to achieve modularity.

ABSTRACT. This article presents iALC, an intuitionistic version of the classical description logic ALC, based on the framework for constructive modal logics presented by Simpson (1994) and related to description languages, via hybrid logics, by de Paiva (2006). This article corrects and extends the presentation of iALC appearing in de Paiva et al (2010). It points out the difference between iALC and the intuitionistic hybrid logic presented in de Paiva (2006). Completeness and soundness proofs are provided. A Sequent Calculus for iALC and a discussion on the computational complexity is taken. It is worth mentioning that iALC is used to formalize legal knowledge, and in fact, was specifically designed to this goal.

ABSTRACT. Two well-known implication fragments of substructural logics are BCI (fragment of logic without contraction and weakening) and BCK (fragment of logic without contraction). The technique of link formulas was developed by the present author first for BCI, as a tool to solve an open problem. Then, a modification of the technique turned out to work for BCK and delivered a proof of its structural incompleteness. The technique can be used to obtain relatively easy proofs of admissibility of certain rules in BCK and BCI, yielding structural incompleteness proofs of several logics in the vicinity.

I will present the technique in a uniform way, applicable to BCI and BCK, as well as to the implication fragments of the relevant logic R and the intuitionistic logic. Some applications (old and new) will be presented to illustrate the technique.

ABSTRACT. We show extensions of the proof theoretic approach to standard completeness, based on the elimination of the density rule in suitable hypersequent calculi.

ABSTRACT. We report on a study of intutionistic fragments of Łukasiewicz logic. We present, in a structured human readable form, syntactic proofs of a number of important formulas originally found with the assistance of the Prover9 automated theorem prover. The identities include homomorphism properties that we put to work in an analysis of the double negation translations of Kolmogorov, Gödel, Gentzen and Glivenko.

ABSTRACT. Girard formulated an approach to proof net quantifiers over a series of three papers. Since the approach uses explicit witnesses for existential quantifiers, it suffers from two problems: limited proof identification and non-local cut elimination. This paper introduces a more abstract approach, unification nets, which solves these problems by leaving existential witnesses implicit: a unification net is merely an axiom linking.