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

The Logic Seminar 2019

The logic seminar takes place on alternate Fridays between 10:15 and 12:00 at Olof Wijksgatan 6 in room T340 (unless otherwise stated).

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

Autumn 2019 Logic Seminar Schedule

6 September (Room T340)
Ali Enayat (FloV)
Some recent news about truth theories
Abstract: This talk is an expanded version of the talk I recently presented at the Logic Colloquium 2019 (Prague). I will report on the following two recent developments in the axiomatic study of truth theories. Item (1) resulted from my collaboration with Fedor Pakhomov (Steklov Institute, Moscow); while item (2) arose from my joint work with Mateusz Łełyk and Bartosz Wcisło (both from the University of Warsaw).
(1) The nonconservativity of CT^-[PA] + DC over PA, where CT^-[PA] is the extension of PA (Peano arithmetic) with CT^- (compositional theory of truth without extra induction), and DC is the axiom stating that a finite disjunction is true iff one of its disjuncts is true.
(2) Feasible reducibility of certain truth theories (including CT^-[PA]) to PA. A corollary of this result is that such truth theories exhibit at most polynomial speed-up over PA.

4 October (T340)
Moa Johansson (Chalmers)
Theory Exploration and Automated Induction
Abstract: Theorem provers typically work by reasoning from a given set of facts, searching for a proof of a given conjecture. But what about situations where there are missing lemmas? This can be the case if we're trying to automating proofs by induction, as we don't necessarily have cut elimination. Theory exploration is a technique for inventing new and interesting mathematical conjectures, given a set of functions, constants and datatypes. I will show a demo of a system called Hipster, which not only automatically generates new conjectures (using testing), but also tries to prove them automatically, and finally assesses if the proof was interesting enough to motivate showing it to the human user.

18 October (T340)
Colin Zwanziger (Carnegie Mellon University)
3 Myths about Predicate Modal Logic
Abstract: Predicate modal logic has been controversial at least since the criticisms of Quine. While predicate modal logic is now accepted, questions remain about its formulation, which has been hampered by several myths. Among these are:
1. In the context of a modal operator, substitution of equals for equals fails.
2. In the context of a modal operator, ordinary quantifier rules such as existential generalization fail.
3. De re is the result of a modal operator occurring inside the scope of a quantifier or other scope-taking operator.
Applying lessons from modal type theory (Bierman and de Paiva 2000, Pfenning and Davies 2001, etc.), I argue for the following countervailing principle:
A. In the context of a modal operator, all free variables will receive de re interpretation, and should be marked as such.
Where this is implemented (e.g. Zwanziger 2017), the rules for equality and quantifiers finally become unproblematic (as demanded by Quine), and de re is more evidently decoupled from scope taking operators. Further refinements should avoid Myths 1-3 by adhering to Principle A, roughly speaking.

1 November (T340)
Daichi Hayashi (Hokkaido)
On complete cut-elimination of several axiomatic theories of truth
Abstract: In this talk, I give cut-elimination arguments for compositional theories of truth, to obtain other proofs of their proof-theoretic strengths. Firstly, following Leigh and Rathen's cut-elimination arguments, I discuss Friedman-Sheard theory (FS) and then apply the method to the analysis of typed theories. Secondly, I consider Kripke-Feferman theory (KF) with the consistency axiom (Cons); however, there is room for improvement in that my proof basically depends on Cantini’s original argument and thus it (partially) requires a model-theoretic procedure.

15 November (T340)
Anton Broberg (FLoV)
Friedman-Sheard and Co-Necessitation
Abstract: The axiomatic theory of truth commonly known as FS (for Friedman-Sheard) has two rules, NEC and CONEC (originally called T-Intro and T-Elim), that allows you to conclude Tr(A) if you have proven A, respectively allows you to conclude A if you have proven Tr(A).

In this talk we will outline a proof of that CONEC is an admissible rule in FS. First, we show that we can put some restrictions on the proofs of FS without limiting the strength of FS. This makes it possible to reformulate the original problem (is CONEC admissible in FS?) to an equivalent, slightly more manageable problem: can FS without CONEC prove anything that FS without NEC can?

We take on this reduced problem by taking a detour into an infinitary system of truth. We show a partial cut-elimination result for this system and we show that within ”reasonable" proof lengths we can embed FS without NEC in this (almost) cut-free, system. Eventually, with a formalised soundness argument for the infinitary system, within the theory FS without CONEC, we show that FS without CONEC can indeed show everything FS without NEC can, and the main result follows.

This is joint work with Graham Leigh.

29 November (T340)
Ana Maria Mora Marquez (FLoV)
What Is Formal In Aristotle’s Syllogistics?
Abstract Using Dutilh-Novaes' and MacFarlane’s taxonomies of the formal in relation to logic, and an additional one by myself, I intend to assess the ways, if any, in which Aristotle’s syllogistic in his Prior Analytics can be said to be ‘formal’. I conclude that it can be said to be formal primarily in relation to a mechanistic intention.

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/21/2019
Share:

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?