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

The Logic Seminar 2018

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

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

Autumn 2018 Logic Seminar Schedule

27 Sep: Volker Halbach (Oxford). Room T340!
Classical and determinate truth (joint work with Kentaro Fujimoto)
Abstract. We present an axiomatic theory of truth over PA formulated in the language of arithmetic with two new unary predicate symbols D and T. The axioms for truth state that truth commutes with connectives and quantifiers for the entire language. Moreover we have an axiom schema stating the T-sentences for all determinate sentences. Determinacy is expressed by the symbol D, which is also axiomatized. The axioms allow for serious interaction between truth and determinacy.

We argue that this system satisfies several requirements that make the theory very useful. In particular, we argue that it can alleviate some worries Kreisel had about the model-theoretic definition of logical consequence.

A proof-theoretic analysis of system shows that it is slightly stronger than the Kripke-Feferman theory of truth or ramified analysis up to ε0.

11 Oct: Bahareh Afshari (FLoV & CS). Room: T340!
Nested sequents for the modal mu-calculus
Abstract. Modal logic provides an effective language for expressing properties of state-based systems. When equipped with operators that can test for infinite behaviour like looping and reachability, the logic becomes a powerful tool for specifying correctness of nonterminating reactive processes such as communication protocols and control systems. An elegant example of such a logic is the modal mu-calculus which extends basic modal logic by two quantifiers for defining inductive and co-inductive operators.

In this talk I will introduce the modal mu-calculus and present a complete proof system for it based on nested sequents. We will see how the proof system can be used to obtain both old and new results for the mu-calculus and its extensions.

25 Oct: Sven-Ove Hansson (KTH)
Choosing the objects of (epistemic) choice
Abstract. In traditional belief revision theory, the epistemic agent is assumed to make choices either among possible worlds or among maximally consistent subsets (“remainders”) of logically closed sets representing the belief state. This is cognitively unrealistic, and some of the problematic properties of the traditional models are directly connected with these constructions of choice. An alternative model, in which choices are made among potential belief states, is shown to avoid most of the problems associated with the traditional models.

8 Nov: Jakub Szymanik (Amsterdam)
Ease of learning explains semantic universals
Abstract: Despite extraordinary differences between natural languages, linguists have identified many semantic universals – shared properties of meaning – that are yet to receive a unified explanation. We analyze universals in a domain of content words (color terms) and a domain of function words (quantifiers). Using tools from machine learning, we show that meanings satisfying attested universals are easier to learn than those that are not. Thus, ease of learning can explain the presence of semantic universals in many different linguistic domains.

22 Nov: Andrea Vezzosi (Chalmers)
Cubical Agda and its Implementation
Abstract. Cubical Type Theory (CTT) [1] gives a computational interpretation to the univalence axiom [2]. It also supports function extensionality and higher inductive types and can be extended with other extensionality principles, like bisimulation as equality for coinductive types.

Cubical Agda is the extension of the proof assistant Agda with the features from Cubical Type Theory. Agda is a feature rich language and interactive editing environment, whose implementation spans around 100k lines of Haskell code. In this talk I will present how CTT has been adapted to better fit the language and implementation of Agda, while still maintaining soundness with regard to the denotational model.

[1] Cubical Type Theory: a constructive interpretation of the univalence axiom. https://arxiv.org/abs/1611.02108
[2] Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book

6 Dec: Gothenburg–Warsaw Seminar on Truth
Details to follow.

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/13/2018

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?