PhDs in Logic IX

PhDs in Logic IX

2nd-4th May 2017, Ruhr-University Bochum, Germany


Download programme

Abstracts and Slides

Book of abstracts of all talks.

Petr Cintula

A Gentle Introduction to Abstract Algebraic Logic (2x45 minutes)

Slides 1

Slides 2

Algebraic logic is the branch of mathematical logic that studies logical systems by giving them algebraic semantics. It mainly capitalizes on the standard Linbenbaum–Tarski proof of completeness of classical logic w.r.t. the two-element Boolean algebra, which can be analogously repeated in other logical systems yielding completeness w.r.t. other kinds of algebras. Abstract algebraic logic (AAL) determines what are the essential elements in these proofs and develops an abstract theory of the possible ways in which logical systems can be related to an algebraic counterpart. The usefulness of these methods is witnessed by the fact that the study of many logics, relevant for mathematics, computer science, linguistics or philosophical purposes, has greatly benefited from the algebraic approach, that allows to understand their properties in terms of equivalent algebraic properties of their semantics.

This course is a self-contained introduction to AAL. We start from the very basics of AAL, develop its general and systematic theory and illustrate the results with applications to particular examples of propositional logics.

Maria Manzano

Leon Henkin on Completeness (1x45 min.)


The Completeness of Formal Systems is the title of the thesis that Henkin presented at Princenton in 1947, and his director was Alonzo Church. His renowned results on completeness for both type theory and first order logic are part of his thesis. It is interesting to note that he obtained the proof of completeness of first order logic readapting the argument found for the theory of types.
In 1963 Henkin published a completeness proof for propositional type theory, A Theory of Propositional Types, where he devised yet another method not directly based on his completeness proof for the whole theory of types. It is surprising that the first-order proof of completeness that Henkin explained in class was not his own but was developed by using Herbrand's theorem and the completeness of propositional logic.
In the book The Life and Work of Leon Henkin, recently published, there is a complete chapter devoted to this issue, Henkin on Completeness.

Abstract as PDF including references.

Identity, Equality, Nameability and Completeness (1x45 min.)


This contribution is divided into two parts. The first one is devoted to the concepts of identity and equality in a variety of logical systems that motivates the definition of our system of Equational Hybrid Propositional Type Theory (EHPTT). The language we have chosen contains a propositional type theory based on lambda and equality. It also contains hybrid resources as well as algebraic ones.
The second part concentrates on the relevant role played by names on the three completeness theorems Leon Henkin published last century. Our completeness proof for EHPTT owes much to the three and we will point out the more important debts we have undertaken.

Abstract as PDF including references.

João Marcos

Classic-like Analytic Tableaux for Non-Classical Logics


This tutorial will show how a single uniform classic-like proof-theoretical mechanism may be constructively applied to a very wide class of logics, exploiting the bivalence that show up in their meta-theory and at the same time making it easier to compare different non-classical systems. Tableaux with two labels are perfectly adequate for expressing such mechanism, and we will show how they may be obtained by a number of axiom-extraction procedures that operate over suitable semantic presentations for non-classical logics.

Gabriella Pigozzi

The logic of group decision: An introduction to judgment aggregation (2x45 min.)

The aggregation of individual judgments on logically interconnected propositions into one collective judgment has drawn attention in economics, law, philosophy, logic and computer science. Classical social choice theoretic models focus on the aggregation of individual preferences into collective outcomes. Such models focus primarily on collective choices between alternative outcomes such as candidates, policies or actions. However, they do not capture decision problems in which a group has to form collectively endorsed beliefs or judgments on logically interconnected propositions. Such decision problems arise in expert panels, decision making bodies (and artificial agents!) seeking to aggregate diverse individual beliefs, judgments or viewpoints into a coherent collective opinion. Judgment aggregation fills this gap by extending earlier approaches of social choice theory. Despite the apparent simplicity of the problem, seemingly reasonable aggregation procedures cannot ensure a consistent collective judgment as result of the aggregation. This is the so-called discursive dilemma.
The bottom line is that it has been shown that no aggregation function can satisfy a number of desirable properties at the same time. Moreover, the aggregation problem has been generalized in a number of ways and several impossibility and possibility results have been proved.
Computer scientists also face the problem of combining different and potentially conflicting sources of information. Recently, methods that originated in computer science have been applied to judgment aggregation and, on the other hand, judgment aggregation has obtained attention from computer scientists as a fruitful paradigm for framing problems stemming from, in particular, distributed artificial intelligence.

Christian Straßer

Nonmonotonic logic


Nonmonotonic logics are attempts to understand defeasible reasoning in a formally precise way. A conclusion obtained by a strictly deductive inference is warranted to be true if it is derived from true premises. Not so for defeasible inferences: they are prone to exceptions. For instance, birds typically fly while penguins don't, or: there is a good reason to infer that it rained when seeing a wet street, but it may have been cleaned just a moment ago, etc.
In this tutorial I will introduce students to nonmonotonic logics. Some central techniques and concepts will be explained. At least one family of nonmonotonic logics will be introduced in some depth.

Heinrich Wansing

Bi-Connexive Variants of Heyting-Brouwer Logic (joint work with Norihiro Kamide)


In this talk I will introduce connexive Heyting-Brouwer logic or bi-intuitionistic connexive logic, BCL. The system BCL is presented as a Gentzen-type sequent calculus, and some theorems are shown for embedding BCL into a Gentzen-type sequent calculus BL for bi-intuitionistic logic, BiInt. The completeness theorem with respect to a Kripke semantics for BCL is proved using these embedding theorems. The cut-elimination theorem and a certain duality principle are also shown for some subsystems of BCL. Moreover, a sound and complete triply-signed tableau calculus for BCL is presented.

Contributed Talks - Slides

Julian Bitterlich: Acyclicity, Simple Connectivity and Covers of Hypergraphs

Carolina Blasio: Through Many-Valent Semantics

Felix Canavoi: A Modal Characterisation Theorem for Common Knowledge Logic

Jérémie Dauphin: ASPIC-END: A Structured Argumentation Framework to Model Explanations of the Liar Paradox

Jonathan Dittrich: Nontransitive Approaches to Paradox and Compositional Principles of Truth

Diego P. Fernandes: Translational Expressiveness between Logics: Giving Adequacy Criteria

Stef Frijters: Formula Feeding: Reasoning about Deontic Conflicts with a Contingent Basis

Daniela Glavaničová: A Realistic View on Normative Conflicts

Gernot Gellwitz: Three-and-a-half Semantics for Epsilon Terms

Balthasar Grabmayr: Invariance of Metamathematical Theorems with regard to Gödel Numberings

Arthur Zito Guerriero: Classical Inferences in the Meta-Theory of Non-Classical Logics

Maciej Kleczek: Variable as a Non-Rigidly Designating Modal Constant

Angeliki Koutsoukou-Argyraki: Proof Mining for Nonexpansive Semigroups

Hermógenes Oliveira: A Decision Procedure for Intuitionistic Propositional Logic Based Solely, notes

Edi Pavlovic: Proof-Theoretic Analysis of the Quantifed Argument Calculus

Yaroslav Petrukhin: Completeness via Correspondence for Extensions of First Degree Entailment supplied with Classical Negation

Jakob Piribauer and Joannes B. Campell: Might and Must in Questions

Adam Přenosil: Extensions of the Four-Valued Belnap-Dunn Logic

Andrei Sipoş: Proof Mining in Convex Optimization

Hanna van Lee: Formalising Theories in Micro-Economics with Dynamic Epistemic Logic

Other events

Note, that there's another logic conference in Bochum following PhDs in Logic: Logic in Bochum III