GSB 2014 PROCEEDINGS: PAPERS WITH ABSTRACTS

ABSTRACT. We report on a study of intutionistic fragments of classical Lukasiewicz 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, Goedel, Gentzen and Glivenko.

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. One methodology for going beyond1 the expressive power of traditional Gentzen systems for non-classical (e.g. intermediate and modal) logics is (instead of hypersequents or nested sequents) the use of labelled sequent calculi, with rules for analysing implications or modal formulae and a representation of conditions on the accessibility relation(s); this allows a wide range of such logics to be represented. Two ways have been studied of representing the accessibility conditions as inference rules: (1) converts the conditions into CNF, using Skolemisation to reduce quantifier alternation, then generating rules that act on both sides of the sequent (papers by Castellini & Smaill, and by Ciabattoni et al), and (2) is, where the accessibility conditions are coherent (aka geometric) implications, to represent them directly as inference rules (acting only on the antecedent) (as in papers by the authors). These latter rules are natural and transparent, whereas clausification tends to render the conditions rather opaquely.

It has been suggested that the second approach is limited to just those accessibility conditions representable as coherent implications. We show this suggestion to be false, by proving that every first-order theory has a coherent conservative extension, i.e. one in which all the necessary reasoning can be carried out using the (coherent) rule-based approach of the authors. This widens the range of logics that approach (2) can handle to all those based on a first-order Hintikka-Kripke semantics.

Such an extension is easily constructed by adding new predicate symbols (and no Skolemisation). Several approaches can be adopted: we consider them in turn, both from a historical and from a practical perspective.

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. The logical formalisms which have been developed as a result of this interaction have attracted the interest of a wider research community than the logicians, and their theory has been intensively investigated, especially w.r.t.\ their semantics and computational complexity.

However, most of these logics lack a comparable proof-theoretic development. More often than not, 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 (for an expanded discussion of the existing proof systems for dynamic epistemic logics, see [5, section 3]).

The problem of the transfer of results, tools and methodologies has been addressed in the proof-theoretic literature for the families of substructural and modal logics, and has given rise to the development of several generalisations of Gentzen sequent calculi (such as hyper-, higher level-, display- or labelled-sequent calculi).

In this talk we focus on the core technical aspects of a proof-theoretic methodology and set-up closely linked to display logic [2] and basic logic [1]. Instances of this set-up have appeared in [5] and [6] to account for (nonclassical versions of) Baltag-Moss-Solecki's dynamic epistemic logic. In ongoing work, this set-up is being applied to propositional dynamic logic [3], monotone modal logic [4], game logic, and linear logic.

The present set-up, which we refer to as \textit{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 [6, 3]. 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 [4].

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 \textit{separation} property (requiring principal formulas in introduction rules to appear in isolation) to the \textit{visibility} property. Visibility requires \textit{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 [1].

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 [5, 6], 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.

\bigskip {\noindent\large\textbf{References}} \smallskip

{\small \noindent [1] G.~Battilotti, C.~Faggian, G.~Sambin, \emph{Basic logic: Reflection, Symmetry, Visibility}, Journal of Symbolic Logic 65 (2000).

\noindent [2] N.~Belnap, \emph{Display logic}, J. of Philosophical Logic 11 (1982), pp.~375-417.

\noindent [3] S.~Frittella, A.~Kurz, A.~Palmigiano, \emph{Multi-type Display Calculus for Propositional Dynamic Logic}, submitted to JLC - Special Issue on Substructural Logic and Information Dynamics (2014).

\noindent [4] S.~Frittella, G.~Greco, \emph{Display-type Sequent Calculus For Monotone Modal Logic}, submitted to Advances in Modal Logic (2014).

\noindent [5] S.~Frittella, G.~Greco, A.~Kurz, A.~Palmigiano, and V.~Sikimi\'{c}, \emph{A Proof-theoretic Semantic Analysis Of Dynamic Epistemic Logic}, to appear in JLC - Special Issue on Substructural Logic and Information Dynamics (2014).

\noindent [6] S.~Frittella, G.~Greco, A.~Kurz, A.~Palmigiano, and V.~Sikimi\'{c}, \emph{Multi-type Display Calculus For Dynamic Epistemic Logic}, to appear in JLC - Special Issue on Substructural Logic and Information Dynamics (2014).

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.

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 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 for constructing 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 the interpretation of sequent calculi using non-deterministic valuation functions. The proposed framework is useful for developing sequent calculi for sub-classical logics, that are obtained as sets of simple derivable rules of the usual sequent calculus for classical logic. This includes 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. [Gore 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 Goedel Loeb 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. 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 and related to description languages, via hybrid logics, by dePaiva. This article corrects and extends the presentation of iALC appearing in \cite{PHR:2010}. It points out the difference between iALC and the intuitionistic hybrid logic presented in \cite{depaiva2003}. 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. 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 these recent developments and discuss open questions concerning syntactic cut-elimination for modal fixed point logics.