Nicola Olivetti: Proof systems for Conditional logics

Conditional logics are a generalisation of modal logics and have a long history . They have been studied to formalise several kinds of reasoning such as : counterfactuals, causality, belief change, plausible/non-monotonic inferences, and strategic reasoning in games. However proof systems for these logics are still underdeveloped, in comparison for instance to modal logics. After recalling the logic themselves, we present the state of the art on some proof systems for conditional logics, open problems and new perspectives.

Paolo Maffezioli: Labelled sequent systems for Dynamic Epistemic Logics

In the first part of the talk,  I will provide a general background on labelled sequent calculi for modal and non-classical logics, and I will discuss the complexity of cut-elimination methods: a numerical bound on cut-free derivations is calculated following the proof of cut-elimination theorem for first-order logic. However, I will argue that a better result can be achieved by a suitable modification of modal rules. In the second part, I will apply the approach to both multi-modal epistemic logic and dynamic logics of knowledge. In particular, I will present a labelled cut-free system for the logic of communications and announcements, which is equivalent to the axiomatic system, and complete with respect to the standard semantics. To conclude, I will suggest new directions for further research.

Richard McKinley: Sequent Calculus in Natural Deduction Style

We explore the possibilities of adding to the sequent calculus abstraction over open branches of derivations.  We consider first a calculus for second-order propositional classical logic in which the axiom is replaced by this abstraction mechanism, and then a higher-order sequent calculus with linear connectives and abstraction, which can simulate the sequent calculi for intuitionistic, classical and multiplicative-exponential linear logic.

Christoph Röthlisberger: Unification in Finite-Valued Logics

The admissible rules of a logic are those rules that can be added to the logic without producing any new theorems. Deciding admissibility for a given rule is theoretically always possible for a finite algebraizable logic, since this is equivalent to checking derivability in a corresponding finite free algebra. However, since free algebras tend to be huge, it is often not at all easy to check if a rule is derivable, even with the help of a computer. In this talk I will describe a general procedure to check admissibility with the help of smaller algebras.

Roman Kuznets: Modal Interpolation via Nested Sequents

Craig interpolation is known to hold for many modal logics. The proof-theoretic way of demonstrating it is by using induction on a cut-free derivation in a suitable sequent calculus. But for several modal logics cut-free sequent systems are not known. It is natural then to consider generalizations of sequent calculi that capture more modal logics in a cut-free way, such as labelled sequents and/or nested sequents. While it is not clear how to perform induction interpolation proof for the former, nested sequents seem well suited for the task due to the absence of semantical elements in the calculus. Despite this, the only use of nested sequents to prove interpolation we are aware of is due to Marta Bílková. Her method deals only with uniform interpolation and only for the basic normal logic K. We present a general framework for proving interpolation by induction on a nested-sequent derivation. The method, a joint work with Melvin Fitting, is inspired by prefixed sequent calculi that he recently introduced as a formalism, intermediate between nested sequents and prefixed tableaus. We discuss how our method applies to normal modal logics axiomatized using axioms d, t, b, 4, and 5 in various combinations.

Jose Gil Ferez: Category Theory as a Tool for (Abstract) Algebraic Logic

Two different contributions of Category Theory to Abstract Algebraic Logic will be explained: The first one, how categories of modules over quantales can help to understand the Problem of the Isomorphism, that is, when the syntactic and lattice-theoretic equivalences of two “general” deductive systems coincide. The second one, how a simple characterization of an algebraic property as a functorial property can help to prove connexions between interpolation and amalgamation.

Leonardo Cabrer: Admissibility through Duality

Dualities of various types have been used by different authors to describe free and projective objects in a large number of classes of algebras. In this paper we go one step further and use dualities to obtain characterizations of subalgebras of free objects. Using these characterizations we provide axiomatizations for single and multiple conclusion admissible rules for the varieties of Kleene algebras, De Morgan algebras, Stone algebras, Kleene lattices and De Morgan lattices.

George Metcalfe: Admissible Rules and Beyond

The admissible rules of a logic (understood as a consequence relation) are often described, equivalently, (1) as rules that can be added to the logic without producing any new theorems, and (2) as rules such that any substitution making the premises into theorems, also makes the conclusion into a theorem. However, this equivalence collapses once multiple-conclusion or other, more exotic, admissible rules are considered. The aim of this talk will be to explain how such distinctions can be characterized and exploited.

Jiri Velebil: Distributive substructural logics are coalgebraic

We define the category of “distributive substructural frames” as certain progroupoids on preorders. We prove that these frames can be considered as a class of coalgebras for a locally monotone endofunctor of preorders. In fact, the above class of frames is modally definable, the modal algebras being precisely the residuated distributive lattices.

Rostislav Horcik: Finite consequence relation in FLc is undecidable

Using results from combinatorics on words, we are going to show that the finite consequence relation in Full Lambek Calculus with contraction (FLc) is undecidable. The key idea is based on a translation of a Minsky machine into a theory and a formula in the language of FLc by means of square-free words. The proof itself uses residuated frames in order to avoid tedious techniques from proof theory.

Anna Zamansky: Non-deterministic semantics and their applications in proof theory

Non-deterministic Matrices (Nmatrices) are a generalization of standard many-valued logics based on
incorporating non-deterministic computations into logical truth-tables. In this talk we present the framework of
Nmatrices and discuss their proof-theoretical applications for a natural class of sequent systems called
canonical calculi. These are systems which have all the standard structural rules, and their logical rules
introduce exactly one occurrence of a connective. We provide modular non-deterministic semantics for such
systems, and use them to characterize important syntactic properties, which are sometimes hard to capture by
other means. This includes various notions of cut-elimination, analyticity, invertibility of logical rules,
axiom-expansion, etc.

Karel Chvalovsky: Notes on Condensed Detachment

We study some basic properties of Hilbert-style propositional calculi with the rule of condensed detachment instead of modus pones and substitution. The rule of condensed detachment, proposed by Carew A. Meredith, can be seen as a version of modus ponens with the “minimal” amount of substitution.

Sebastian Krinninger: Validity in logics that combine supervaluation and fuzzy logic

Fuzzy logics based on t-norms are a degree-based and truth-functional approach for reasoning with vague information. Supervaluationism, one of the theories of vagueness studied by analytic philosophy, follows a different idea: A vague statement should be considered true if it is true in all admissible precisifications, i.e., in a set of completely precise, classical models. In this talk, we present a natural way of combining supervaluation and t-norm based logics. Basically, we measure the amount of truth of atomic formulas in a precisification space and evaluate compound formulas according to the truth functions given by a continuous t-norm. We consider two natural restrictions on precisification spaces. The first one is to require that every precisification has a strictly positive measure. The second one is to enforce that all precisifications have a uniform measure. We investigate the effects of these restrictions on the validity of formulas. It turns out that the ukasiewicz t-norm is special because these restrictions do not affect the set of valid formulas. For other t-norms a more subtle picture emerges.

Oliver Fasching: Modal Gödel operators as Gödel homomorphisms

We extend Gödel logic by a unary operator o and consider several interpretations with a real-semantics. If interpretations are given by I_r(o(A)):= min{1,r+I(A)}, for fixed r \in [0,1], the resulting propositional fragment is nicely axiomatisable but the first-order fragment is surprisingly is Π₂-hard due to variant of Scarpellini’s proof for Łukasiewicz logic. Another class of interpretations is given by Gödel homomorphisms, i.e. functions that where o distributes over the binary connectives; we present a simple proof-system for LK. We also give axiomatisations for the case where o runs through a class of certain monotone functions.

Martin Vita: A Uniform Approach to Special Types of (Fuzzy) Filters

The recent years witnessed a proliferation of not-so-deep papers on special types of (fuzzy) filters (fantastic, implicative, etc.) on algebras of fuzzy logics. While the community have always suspected that these papers have a very little ‘added value’ none took the effort to ‘formalize and prove’ this suspicion. In our previous work we have done exactly this for ‘crisp’ filters by providing a simple theory of R-L-filters based on Abstract Algebraic Logic. In this contribution we review this theory and develop its straightforward ‘fuzzyfication’ to deal with ‘fuzzy filters’ and show how it can be simply generate the results existing in the ‘literature’.

Matthias Baaz: Sequents of relation calculus: standard and witnessed first order Gödel logics (joint work with Agata Ciabattoni)

The natural extension of the sequent of relation calculus is sound for the witnessed, but not sound for the standard first order Gödel logic. However, the sequent of relation calculus is not cut-free complete for the witnessed first order Gödel logic. (No analytic calculus exists for this logic.) We show, that the prenex formulas cut-free provable in the sequent of relation calculus are exactly the prenex formulas valid in standard first order Gödel logic.

Felix Bou: Thinking on the Monadic Predicate Lukasiewicz Logic

The aim of the talk is explaining how the interpretability (in the context of predicate Lukasiewicz logic) of classical linear orders can be used to get new results for the monadic predicate Lukasiewicz logic. We will explain the method, and we will show two applications: building standard tautologies that are not general tautologies, and proving undecidability of monadic predicate Lukasiewicz logic.

Zuzana Hanikova: Complexity in Basic Logic

We look at fragments of the theory of some (standard) BL-algebras: those imposed by restricting the language, and those imposed by conditions on the first-order algebraic formulas.

Tomas Kroupa: Probabilities in Finitely-valued  Lukasiewicz Logic and the Binomial Sampling Models

States on MV-algebras are usually interpreted as probabilities over many-valued events. Every many-valued event is identified with the equivalence class of a formula in the Lukasiewicz logic. This model is justified by a betting-style argument based on a vague description of bets together with the generalization of the de Finetti’s theorem. We will present an alternative interpretation of states on the free MV-algebra of Lukasiewicz logic over one propositional variable. Specifically, every state is identified with an expected value operator on an algebra of random variables describing certain binomial sampling models (such as independent trials in a series of many coin tossing experiments).  The basic properties of this model are derived and its consequences for modelling uncertainty in Lukasiewicz logic are discussed.

Tommaso Flaminio: Geometrical aspects of possibility measures on finite domain MV-clans

We will present a study on generalized possibility and necessity measures on MV-algebras of [0, 1]-valued functions (MV-clans) in the framework of the so-called idempotent mathematics, where the usual field of reals R is replaced by  the max-plus semiring R_\max. We present results about extendability of partial assessments  to possibility and necessity measures, and we characterize the geometrical properties of the space of homogeneous possibility measures. Not secondarily, we show how idempotent mathematics is the natural framework where to develop possibility and necessity theory, in the same way classical mathematics serve as a natural setting for probability theory.

Thomas Vetterlein: Logics between approximate reasoning and fuzzy logic

Truth degrees can be interpreted as similarities; this way to interpret fuzzy sets has been proposed very soon after Zadeh’s seminal paper appeared. We propose a logic based on this approach. The logic is an improved version of the calculus presented at Eusflat 2011.
The logic is characterised by the fact that it is conceptually very close both to (mathematical) fuzzy logic and to approximate reasoning. However, since its semantics cannot be based on chains, it cannot be called a fuzzy logic; and since connectives are, roughly speaking, treated in a truth-functional way, it is not exactly what is at present called approximate reasoning.
The benefit of our logic is its clear conceptual framework. Moreover, the calculus is strong enough to be applicable, for instance, in the field of if-then rule based fuzzy expert systems.

Lluis Godo: On the expansion of t-norm fuzzy logics with hedges

Hajek and Vychodil proposed the axiomatization of truth-stressing and depressing hedges as expansions of \BL\ by new unary connectives. They show that their logics are chain-complete, but standard completeness is only proved for the expansions over Gödel logic.  We propose  weaker axiomatizations that have as main advantages to preserve the standard completeness properties of the original logic and that any subdiagonal (resp. superdiagonal) non-decreasing function on [0,1] preserving 0 and 1 is a sound interpretation of the truth stresser (resp. depresser) connectives.