Till startsida
To content Read more about how we use cookies on gu.se

The Logic Seminar 2017

The logic seminar takes place on alternate Thursdays between 13:15 and 15:00 at Olof Wijksgatan 6 in room T 307 (unless otherwises stated).

The archive of older seminars (starting 2005) is divided into two web pages: 2005-2013 Logic Seminars and 2014-2017.

Fall 2017 Logic Seminar Schedule

Tuesday 19 Sep: Bartosz Wcisło (Warsaw) NB. room T219

Propositional constructions in compositional truth theories

In our talk, we will describe a construction in propositional logic which proved very useful in the study of models of truth theories.

Many intuitive properties for the classical compositional theory of truth over Peano arithmetic called CT− fail because this theory does not enjoy the properties of disjunctive and conjunctive correctness. I.e., if M |= CT− is a model whose arithmetical part is nonstandard, we cannot typically expect that a disjunction of nonstandard length is true if and only if one of the disjuncts is true.

By a recent result of Pakhomov, compositional truth theory with the disjunctive correctness principle is in fact not conservative over Peano Arithmetic. However, in many applications we only in fact need a disjunctive correctness in a very specific circumstances, where we expect at most one disjunct to be true which is located at some standard syntactic depth of a given nonstandard disjunction. In such a case, the use of disjunctions may be replaced with another propositional construction invented by Smith (and preceded with a similar construction by Lachlan) which behaves in a controllable fashion already in CT−.

We show how this construction may be used to obtain a number of results on models of truth theories including more perspicuous proof of Lachlan’s Theorem on recursive saturation of models of CT−.

21 Sep: Mateusz Łełyk (Warsaw)

Compositional Truth Theories, Bounded Induction and Reflection Principles


One of the most important questions studied within the field of Axiomatic Truth Theories is to determine the arithmetical strength of various axioms for the truth predicate. In this talk we study three main types of such truth principles for the typed truth predicate: various kinds of compositionality, bounded induction and reflection principles, namely, we shall consider three basic compositional truth theories: CT-, in which the internal logic is classical, PT- and WPT-, in which the internal logic is modelled after the Strong and Weak Kleene Logic, respectively.

One of the surprising result explained in our talk is the theorem on multiple axiomatizations of CT- extended with a bounded induction (CT0): putting together the results of Cieśliński, Kotlarski, and myself we show that CT0 is deductively equivalent to extensions of CT- with various reflection principles.

Then we ask whether the above theorem is stable under weakening the compositional axioms: we investigate analogous extensions of PT- and WPT-. It turns out that adding bounded induction to PT- results in one more axiomatization of CT0, and the same is "almost true" for the Weak Kleene case. However differences between "completeness" and "closure" reflection principles become visible. We show that in general the former are much weaker then the latter.

2 Nov: Stergios Chatzikyriakidis (FLoV)

Modern Type Theoretical Semantics and Reasoning with Natural Language


In this talk, I will discuss the use of Modern Type Theories (MTTs), i.e. Type Theories within the tradition of Martin-Löf, to the study of Natural Language (NL) semantics. I will give a short overview of the way MTTs have been used in order to deal with a number of linguistic phenomena and I will argue that MTTs can be used as an alternative to simply type theory and Montague Semantics for NL semantics. I will then discuss the problem of Natural Language Inference (NLI), namely the task of determining of whether an NL sentence follows or not from another one. To this extent, I will argue that one way to deal with at least the NL cases where logical inference is involved, is to use MTT semantics plus proof assistant technology to reason about these semantics. I will exemplify this idea by presenting FraCoq, a system based on the Grammatical Framework (GF) to parse NL sentences and Coq to reason about the output semantics. In effect, FraCoq defines a correspondence between the abstract syntactic structures of GF and semantics in a Type Theoretical language. We show the result of evaluating against the FraCaS test suite. We will show that FraCoq achieves state of the art results (for logical approaches). I will conclude discussing future work, potential extensions of the system, proof-automation, as well as the prospect of using hybrid systems encompassing both logical and Machine/Deep Learning components.


16 Nov: Albert Visser (Utrecht): 2017 Lindström Lectures

Research Lecture: The Second Incompleteness Theorem in a (somewhat) General Setting (13:15–17:00, T307)

Public Lecture: De Interpretatione (18:15–19:15, T307)

For abstracts, see here.


30 Nov: Øystein Linnebo (Oslo)

Generality explained


What explains a true universal generalization? This paper distinguishes two kinds of explanation. While an instance-based explanation proceeds via each instance of the generalization, a generic explanation is independent of each instance, relying instead on completely general facts about the properties or operations involved in the generalization. This distinction is illuminated by means of a truth-maker semantics, which is also used to show that instance-based explanations support classical logic, while generic explanations support only intuitionistic logic.

14 Dec: 

Mailing list

There is a mailing list used for spreading information about the logic seminar. Please use the above link to subscribe to it.


Page Manager: Monica Havström|Last update: 11/10/2017

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?