# Seminari Cuc, Seminar on Proof Theory and Foundations of Mathematics

Organization

In principle, we meet on a bi-weekly basis on Wednesday from 12:15 -- 14:00 at the Ramon Llull Seminar Room (Room 4047, formerly called the Logic Seminar Room) at the fourth floor of the Philosophy department at Carrer Montalegre 6. This seminar was formerly called Seminari Cuc, Seminar on Proof Theory and Modal Logic. Related presentations of a more informal nature are allocated at the PhD Seminar on Mathematical Logic informally referred to as the Seminari Alterne.

 Luka Mikec 13-11-2019 Luka Mikec 30-10-2019 Joost J. Joosten 16-10-2019 Joost J. Joosten 10-10-2019 Joost J. Joosten 09-10-2019 Joost J. Joosten 02-10-2019 Joost J. Joosten 27-06-2019 Joost J. Joosten 18-06-2019 David Fernández Duque 20-05-2019 Ana Borges 06-05-2019 Ana Borges 29-04-2019 Joost J. Joosten 24-04-2019 Tuomas Hakoniemi 18-03-2019 David Fernández Duque 14-03-2019 Joost J. Joosten 25-02-2019 Joost J. Joosten 18-02-2019 Amanda Vidal 13-02-2019 Cyril Cohen 30-01-2019 David Fernández Duque 23-01-2019 Joost J. Joosten 16-01-2019 Joost J. Joosten 09-01-2019 Ana Borges 05-12-2018 Joost J. Joosten 14-11-2018 Joost J. Joosten 07-11-2018 Joost J. Joosten 31-10-2018 Joost J. Joosten 26-09-2018 Mireia González Bedmar 27-06-2018 David Fernández Duque 19-06-2018 Bjørn Jespersen 14-06-2018 Ana Borges 06-06-2018 Ana Borges 23-05-2018 Daniel Sousa 16-05-2018 Fabian Romero 09-05-2018 Joost J. Joosten 25-04-2018 Joost J. Joosten 18-04-2018 Joost J. Joosten 14-03-2018 Eduardo Hermo Reyes 07-03-2018 Eduardo Hermo Reyes 21-02-2018 Eduardo Hermo Reyes 14-02-2018 Joost J. Joosten 07-02-2018 Joost J. Joosten 31-01-2018 Joost J. Joosten 17-01-2018 Fabian Romero Jimenez 28-11-2017 Joost J. Joosten 22-11-2017 Eduardo Hermo Reyes 15-11-2017 Ana Borges 02-11-2017 Ana Borges 25-10-2017 Ana Borges 04-10-2017 Andrea Condoluci 15-06-2017 Luka Mikec 19-04-2017 Joost J. Joosten 22-03-2017 Joost J. Joosten 15-03-2017 Joost J. Joosten 09-03-2017 Antonio Montalban 01-03-2017 David Fernández Duque 25-01-2017 Joost J. Joosten 09-11-2016 Joost J. Joosten 26-10-2016 Pawel Pawlowski 19-10-2016 Pawel Pawlowski 05-10-2016 Juan Pablo Aguilera 21-09-2016 Hector Zenil 20-09-2016 Joost J. Joosten 25-05-2016 Joost J. Joosten 04-05-2016 Tuomas A. Hakoniemi 07-04-2016 Joost J. Joosten 03-02-2016 Joost J. Joosten 14-01-2016 David Fernández Duque 02-12-2015 Joost J. Joosten 18-03-2015 Joost J. Joosten 04-03-2015 Joost J. Joosten 28-01-2015 Joost J. Joosten 14-01-2015 Joost J. Joosten 17-12-2014 Joost J. Joosten 29-10-2014 Joost J. Joosten 22-10-2014 Eduardo Hermo Reyes 28-05-2014 Joost J. Joosten 02-04-2014 Joost J. Joosten 19-03-2014 Joost J. Joosten 22-01-2014 Joost J. Joosten 08-01-2014 Cory Knapp 18-12-2013 Cory Knapp 27-11-2013 Joost J. Joosten 20-11-2013 Cory Knapp 13-11-2013 Joost J. Joosten 06-11-2013 Cory Knapp 16-10-2013 Paul Erdös 23-10-2013 Cory Knapp 16-10-2013 Joost J. Joosten 02-10-2013 Joost J. Joosten 15-05-2013 Joost J. Joosten 08-05-2013 Joan Bagaria 24-04-2013 David Fernández Duque 17-04-2013 Joan Bagaria 03-04-2013 Joost J. Joosten 20-03-2013 Joost J. Joosten 13-03-2013 Joost J. Joosten 06-03-2013 Joost J. Joosten 27-02-2013 Joost J. Joosten 20-02-2013 Joost J. Joosten 13-02-2013 Joost J. Joosten 23-01-2013 Joost J. Joosten 19-12-2012 Joost J. Joosten 21-11-2012 Joost J. Joosten 07-11-2012 Joost J. Joosten 24-10-2012 Joost J. Joosten 16-05-2012 Joost J. Joosten 02-05-2012 Joost J. Joosten 28-03-2012 Joost J. Joosten 21-03-2012 Joost J. Joosten 07-03-2012 Joost J. Joosten 22-02-2012 Joost J. Joosten 08-02-2012 Joost J. Joosten 25-01-2012 Joost J. Joosten 11-01-2012 Joost J. Joosten 14-12-2011 Joost J. Joosten 30-11-2011 Joost J. Joosten 28-9-2011 Joost J. Joosten 15-6-2011 Joost J. Joosten 1-6-2011 Joan Bagaria 18-5-2011 Joan Bagaria 17-5-2011 Joost J. Joosten 13-4-2011 Joost J. Joosten 6-4-2011 Joost J. Joosten 16-03-2011

Speaker: Luka Mikec
Title: Completeness w.r.t. generalised Veltman semantics, Part II
Date: Wednesday, November 13, 2019
Time: 13:00 - 14:00
Location: Ramon Llull

Two similar but different semantics for interpretability logics are used today for various purposes, ordinary and generalised Veltman semantics. Completeness of a given system w.r.t. the ordinary semantics implies completeness w.r.t. the generalised semantics. Recently we have shown that certain logics are complete w.r.t. the generalised semantics, and these logics are not known to be, or even are known not to be, complete w.r.t. ordinary semantics. Although the fact that some logic is complete w.r.t. generalised semantics is in principle a strictly weaker result than the analogous result for ordinary semantics, it's not necessarily less useful. For example, there is a relatively straightforward method of establishing finite model property for logics that are complete w.r.t. generalised semantics, while no such method is known for ordinary semantics. Thus at least in some cases completeness w.r.t. generalised semantics suffices. We will give a few examples of why is using generalised semantics helpful, and sketch proofs of some of the key results.

Speaker: Luka Mikec
Title: Completeness w.r.t. generalised Veltman semantics
Date: Wednesday, October 30, 2019
Time: 12:30 - 14:00
Location: Ramon Llull

Two similar but different semantics for interpretability logics are used today for various purposes, ordinary and generalised Veltman semantics. Completeness of a given system w.r.t. the ordinary semantics implies completeness w.r.t. the generalised semantics. Recently we have shown that certain logics are complete w.r.t. the generalised semantics, and these logics are not known to be, or even are known not to be, complete w.r.t. ordinary semantics. Although the fact that some logic is complete w.r.t. generalised semantics is in principle a strictly weaker result than the analogous result for ordinary semantics, it's not necessarily less useful. For example, there is a relatively straightforward method of establishing finite model property for logics that are complete w.r.t. generalised semantics, while no such method is known for ordinary semantics. Thus at least in some cases completeness w.r.t. generalised semantics suffices. We will give a few examples of why is using generalised semantics helpful, and sketch proofs of some of the key results.

Speaker: Joost J. Joosten
Title: Two series of interpretability principles for weak arithmetics
Date: Wednesday, October 16, 2019
Time: 12:30 - 14:00
Location: Ramon Llull

In this talk we will discuss various aspects of the paper Two series of formalized interpretability principles for weak systems of arithmetic.

In that paper, a collection of new interpretability principles is presented. For any arithmetical theory extending bounded arithmetic the principles can be proven to be arithmetically valid. The main techniques used here are based on definable cuts and observations by Pudlák.

In the talk, as in the paper, we shall be mostly interested in frame correspondences and arithmetical soundness proofs. Rather than looking at the recursively defined series as in the paper, we shall in the talk look at representative examples instead.

This is joint work with Evan Goris.

Speaker: Joost J. Joosten
Title: Control funcional y control cualitativo de los algoritmos en la administración pública
Date: Thursday, October 10, 2019
Time: 12:00 - 12:45
Location: Valencia

This talk was given at

Segundo Seminario Internacional DAIA de Derecho público. “Datos e inteligencia artificial en el sector público: la importancia de las garantías jurídicas” and slides of the talk can be found here.

Speaker: Joost J. Joosten
Title: Two semantics for interpretability logics: relational and arithmetical
Date: Wednesday, October 9, 2019
Time: 12:00 - 12:45
Location: Ramon Llull

In this talk we discuss relational semantics for interpretability logics, the so-called Veltman semantics. We discuss completeness and incompleteness results. Further, we also consider arithmetic semantics from last week. Where Montagna's principle used full induction, in general we can only get an approximation of it by replacing non-available induction with shortening definable cuts: Pudlák's principle. We use this principle to see the arithmetical soundness of various principles of interpretability.

Speaker: Joost J. Joosten
Title: The interpretability logic of Peano arithmetic
Date: Wednesday, October 2, 2019
Time: 12:00 - 13:30
Location: Ramon Llull

We introduce interpretability as a meta-mathematical concept and see how this gives rise to formalisation and to logics much in the spirit of Gödel-Löb's logic for formalised provability. Next, we present the logic ILM which is known to be sound and complete for Peano arithmetic. As a heuristics for soundness proofs we see how interpretations as uniform model constructions help us a lot. In particular, when we have full induction we see that any internally defined model will be an end-extension of the original thereby preserving existential formulas.

Speaker: Joost J. Joosten
Title: Turing progressions versus worms
Date: Thursday, June 27, 2019
Time: 11:10 - 12:10
Location: Maria Zambrano

In this talk we will see how each Turing progression can be approximated by adding (the arithmetical interpretation of) a single worm to the base theory. We present the proof for first order arithmetic and see which parts have to be changed and how to go beyond first order.

Speaker: Joost J. Joosten
Title: Released from the swamp
Date: Tuesday, June 18, 2019
Time: 10:00 - 11:15
Location: Maria Zambrano

When the baron of Münchhausen got trapped with his horse in a swamp he was able to free himself and his horse by pulling himself up by his hair. In analogy to this heroic deed we coined our Münchhausen provability: a provability predicate that uses oracles which are provability predicates. For the past two years I have been talking every now and then about various aspects of Münchhausen provability: soundness, completeness, provable completeness, uniqueness, etc. But never did we really dwell on the question if there really exists (usable) Münchhausen predicates. In this presentation we will show they don’t. Of course, that is a joke and we will see that indeed good Münchhausen predicates can be defined in rather weak fragments of second order arithmetic. In principle this should close the lecture series on our barony.

Speaker: David Fernández Duque
Title: Predicatively unprovable termination of the Ackermannian Goodstein principle
Date: Monday, May 20, 2019
Time: 10:30 - 12:00
Location: Ramon Llull Seminar

Joint work with Toshiyasu Arai, Stanley Wainer and Andreas Weiermann.

The classical Goodstein process gives rise to long but finite sequences of natural numbers whose termination is not provable in Peano arithmetic. In this talk we consider a variant based on the Ackermann function. We show that Ackermannian Goodstein sequences eventually terminate, but this fact is not provable using predicative means.

Speaker: Ana de Almeida Borges
Title: Artemov's Theorem
Date: Monday, May 6, 2019
Time: 10:30 - 12:00
Location: Ramon Llull Seminar

We continue the last seminar where we left of, giving the proof of Artemov's Theorem and of the main Lemma it is based on.

Speaker: Ana de Almeida Borges
Title: Artemov's Theorem
Date: Monday, April 29, 2019
Time: 10:30 - 12:00
Location: Ramon Llull Seminar

We can talk about first-order arithmetic by using provability logic enriched with quantifiers. This new language is the language of quantified modal logic, or QML. Artemov's Theorem states that the class of always true sentences of QML is not arithmetical, i.e., that there is no sentence True of arithmetic such that for every formula φ of arithmetic, True(φ) ↔ φ holds. We talk about the idea behind the proof of this statement, and give some preliminary notions and results towards a full proof. This talk is based on Chapter 17 of Boolos' The Logic of Provability.

Speaker: Joost J. Joosten
Title: The Logic Road to Software Homologation.
Date: Wednesday, April 24, 2019
Time: 15:00 - 16:30
Location: Salon de grados, Facultad de derecho, UB

This talk was given in the context of the Second UB International PhD in Law Conference.

Software always contains mistakes. Most of them are small and innocuous since they passed expert scrutiny and dynamic testing. However, the mistakes are there and from time to time they can have disastrous consequences: exploding rockets, planes or erroneous legal verdicts. These days we are getting increasingly dependent on algorithmic legal processes. But how are we to trust them knowing that software always contains errors. In the face of this, what is the value of a DNA sequencing run, the reading of a tachograph, the measurement and interpretation of a speeding device? In this talk with we will see how proof assistants can help to significantly reduce operational risk. As such, software will be proven to comply the specification. Of course humans can still err in claiming that the formal specification faithfully describes a situation. But, in our solution, at least the errors in the software are reduced to zero. Slides of this talk can be found here.

Speaker: Tuomas Hakoniemi
Title: Lower bounds on size of Sums-of-Squares refutations.
Date: Monday, March 18, 2019
Time: 10:30 - 12:00
Location: Logic Seminar/Ramon Llull

We discuss a size-degree trade-off for Sums-of-Squares proofs and show how to obtain strong lower bounds on the monomial size of refutations from the trade-off and the existing degree lower bounds. This talk is based on joint work with Albert Atserias. Here is the paper.

Speaker: David Fernández Duque
Title: Intuitionistic linear temporal logics.
Date: Thursday, March 14, 2019
Time: 10:15 - 11:45
Location: Maria Zambrano Seminar

Dynamical topological systems are pairs (X,S) where X is a topological space and S: X->X is continuous. These systems provide a natural semantics for the language of linear temporal logic by interpreting temporal modalities using the function S and interpreting implication according to the topological semantics for intuitionistic logic, giving rise to a family of natural intuitionistic temporal logics. In this talk we will give an overview of known results regarding such logics, including decidability and completeness theorems, and state some open problems. This is joint work with Joseph Boudou and Martín Diéguez.

Speaker: Joost J. Joosten
Title: Provable completeness for Münchhausen provability, reflection, induction and collection.
Date: Monday, February 25, 2019
Time: 10:30 - 11:30
Location: Logic Seminar/Ramon Llull

In this talk we focus on provable completeness for our provability predicates and study the formula classes for which we have provable completeness. Using a Rosser-style fixpoint, we can show that sometimes we can import universal quantifiers from outside the box to inside the box. However, if all the technical machinery works depends on the amount of collection available which in turn can be related to reflection and induction.

The provable completeness results shall be key in proving that the [a] modality is, in a sense Sigma_{1+a}^0-definable.

Speaker: Joost J. Joosten
Title: Completeness for our Barony
Date: Monday, February 18, 2019
Time: 10:30 - 11:30
Location: Logic Seminar/Ramon Llull

In previous sessions we have spoken mainly on soundness for Münchhausen provability. In this talk we fix on various completeness phenomena for Münchhausen provability.

In this talk we shall see how arithmetical completeness can be easily obtained under some fairly general conditions. We revisit Solovay's completeness proof and comment on the changes to adopt to our setting.

Speaker: Amanda Vidal
Title: On non RE logics: some well-known cases and some new ones
Date: Wednesday, February 13, 2019
Time: 12:30 - 14:00
Location: Logic Seminar/Ramon Llull

In this talk we will do an overview of some non Recursively Enumerable logics, and then move to modal many-valued logics, where we can exhibit several new examples of non RE logics arising from a very natural semantical definition. Computability results for this logics naturally play a crucial role in proving so. Slides of this talk can be found here.

Speaker: Cyril Cohen
Date: Wednesday, January 30, 2019
Time: 12:30 - 14:00
Location: Logic Seminar

Formal verification of algorithms often requires a choice between definitions that are easy to reason about and definitions that are computationally efficient. One way to reconcile both consists in adopting a high-level view when proving correctness and then refining stepwise down to an efficient low-level implementation. We present a refinement methodology for developing formally verified computer algebra algorithms that can be run inside Coq. The methodology allows us to prove the correctness of algorithms on a proof oriented description taking advantage of the Mathematical Components library, and then refine it to an efficient computation-oriented version. The proofs are transported mostly automatically using ideas found in the proof of the parametricity theorem for functional programming languages. We give various examples of applications, ranging from code extraction to large scale reflection.
We present various joint works, which involved the collaboration of Simon Boulier, Maxime Dénès, Anders Mörtberg, Damien Rouhling and Enrico Tassi. Slides can be found here.

Speaker: David Fernánuez-Duque
Title: Goodstein sequences for the Bachmann-Howard ordinal
Date: Wednesday, January 23, 2019
Time: 12:30-13:30
Location: Logic Seminar/Ramon Llull

The classical Goodstein process is defined by writing numbers in base k for increasing values of k and successively subtracting one. By mapping the numbers obtained into \epsilon_0, it becomes clear that the process must terminate in finite time, although the sequences are typically too long for this termination to be observed empirically. In this talk we will consider an alternate Goodstein-like process based on subrecursive hierarchies. Namely, one uses a form of fast-growing hierarchy based on ordinals below \epsilon_0 to provide a notation system for natural numbers relative to some base number k. With this one can produce an analogue to the classical Goodstein process which can also be guaranteed to terminate, although in this setting one must map natural numbers into the Bachmann-Howard ordinal, producing a proof of termination not formalizable in ID_1.

Speaker: Joost J. Joosten
Title: Tweaking the oracles
Date: Wednesday, January 16, 2019
Time: 12:30-13:30
Location: Logic Seminar

This talk is a continuation of last week's talk. As such, we revisit Münchhausen provability and consider consider predicates using one oracle call, multiple oracle calls of fixed tier and multiple oracle calls of multiple tiers. We will see under what circumstances these notions relate to each other and how.

Speaker: Joost J. Joosten
Title: Münchhausen provability revisited: the devil is in the detail
Date: Wednesday, January 9, 2019
Time: 12:30-13:30
Location: Logic Seminar

We revisit Münchhausen provability and consider how slight changes in the recursive definition lead to mayor possible diversions. In particular, we consider predicates using one oracle call, multiple oracle calls of fixed tier and multiple oracle calls of multiple tiers. The latter turns out to be the better option.

Speaker: Ana Borges
Title: Worms in Coq
Date: Wednesday, December 5, 2018
Time: 12:30-13:30
Location: Logic Seminar

The Reflection Calculus (RC) is the strictly positive fragment of GLP, a polymodal provability logic. This fragment is interesting because it is known to be decidable in polynomial time through Kripke frames, while still being expressive enough to perform ordinal analysis of theories such as PA. Joost Joosten and the speaker have developed the Worm Calculus (WC), a calculus exactly as expressive as RC, but with a language constrained to worms (iterated consistency statements). In this talk, we will take a look at a journey to formalize RC, WC, and the proof of their equivalence in Coq. As a bonus, we will see purely syntactical algorithms to decide both calculi.

Speaker: Joost J. Joosten
Title: Set theoretical aspects of proof theory via Turing progressions
Date: Wednesday, November 14, 2018
Time: 12:30-13:30
Location: Ramon Llull

Abstract: In this talk we will exhibit the basics of proof-theoretical analysis via iterated reflection as introduced by Ulf Schmerl and streamlined by Lev Beklemishev. The objective of this method is to measure the strength of some target theory U relative to some weak base theory T. Thus, a proof theoretical ordinal will measure how often' one should iterate adding consistency to T as to maximally approximate the target theory U. We will try to keep the proof theoretical content of the talk self-contained highlighting interactions with and applications to set theory. Slides of this talk can be found here.

Speaker: Joost J. Joosten
Title: Münchhausen sound without induction
Date: Wednesday, November 7, 2018
Time: 12:30-13:30
Location: Ramon Llull

Abstract: This talk is a continuation of last week's talk and as such considers some aspects of Münchhausen provability of transfinite polymodal provability logic. We have seen how a straight-forward soundness proof does not allow for the separation of meta from object theory. In this talk we continue our approach from our previous presentation and put forward a rather simple solution using bounded quantification to replace conjunctions of arbitrary length but of bounded complexity. We can now finish our soundness proof without having any need for transfinite nor reflexive induction. This is good since it allows for a small `unit of consistency" base theory when applying the logic to ordinal analyses.

Speaker: Joost J. Joosten
Title: Ordinal analyses via Münchhausen provability predicates
Date: Wednesday, October 30, 2018
Time: 12:10-13:00
Location: Ramon Llull

Abstract: This talk considers some aspects of the Turing Jump Interpretation (also called Münchhausen provability) of transfinite polymodal provability logic. We have seen how a straight-forward soundness proof does not allow for the separation of meta from object theory. In this talk we continue our approach from our previous presentation and put forward a rather simple solution using bounded quantification to replace conjunctions of arbitrary length but of bounded complexity. This gives rise to two different natural notions of natural provability predicates. We shall finish the soundness proof (without transfinite induction!) and comment on how these two provability notions are related to each other.
Next we shall briefly discuss how such predicates are to be employed in a Pi_zero-one ordinal analysis.

Speaker: Joost J. Joosten
Title: Strict Münchhausen versus Münchhausen provability
Date: Wednesday, September 26, 2018
Time: 12:15-13:15
Location: Aula 402 (different from our regular place)

Abstract: This talk considers some aspects of the Turing Jump Interpretation (also called Münchhausen provability) of transfinite polymodal provability logic. We have seen how a straight-forward soundness proof does not allow for the separation of meta from object theory. In this talk we put forward a rather simple solution using bounded quantification to replace conjunctions of arbitrary length but of bounded complexity. This gives rise to two different natural notions of natural provability predicates. We shall comment on how these are related to each other.

Speaker: Mireia González-Bedmar
Title: On the Dialectica interpretation and a game-theoretic extension to analysis
Date: Wednesday, June 27, 2018
Time: 17:00-18:00
Location: Ramon Llull seminar

The Dialectica interpretation, combined with the negative translation, provides a way of extracting constructive content from classical proofs in arithmetic. Its usual extension to analysis via Spector's bar recursion can be replaced with an extension via an equivalent game-theoretic recursion computing optimal strategies. In this talk we present and motivate the Dialectica interpretation, we introduce the notion of sequential game and selection function, and we work out a simple case study: the interpretation of the infinite pigeon-hole principle.

Speaker: David Fernánuez-Duque
Title: Baire resolvability on metric spaces
Date: Tuesday, June 19, 2018
Time: 12:00-13:00
Location: IMUB Seminar room

Abstract: This is a talk in the Barcelona Logic Seminar Series of which the recent talk has a separate page and the past talks have another page.

A topological space is resolvable if it can be partitioned into two dense sets. Hewitt showed that any crowded metric space is resolvable. One may then ask if the two sets may be chosen so that they are not only dense, but everywhere "large" in some sense; speci cally, we consider largeness in the sense of Baire. Recall that a set is meager if it can be written as a countable union of nowhere- dense sets. Let us say that a set is 'Baire-dense' if its intersection with any non- empty open set is non-meager, and a topological space is Baire-resolvable if it can be partitioned into two Baire-dense sets. We show that, under some natural conditions, Hewitt's result can be strengthened to obtain Baire-resolvability of crowded spaces. Finally, we discuss how this result can be seen within the more general context of Kuratowski algebras, which are Boolean algebras equipped with a closure-like operation.

Speaker: Bjørn Jespersen
Title: Foundations and Applications of Transparent Intensional Logic
Date: Thursday, June 14, 2018
Time: 10:00-11:00
Location: Logic Seminar

Abstract: This talk presents the key formal foundations of Transparent Intensional Logic, explains their philosophical motivation, and demonstrates how the theory can offer a logical analysis of a wide range of terms and sentences primarily from natural language.

Speaker: Ana Borges
Title: Smooth Turing progressions II
Date: Wednesday, June 06, 2018
Time: 12:30-14:00
Location: Logic Seminar

Abstract: This talk is a continuation of May 23. As such we will show that PA + Con(PA) has the same Π1-consequences as the (ε0 + ε0)-th smooth Turing jump of EA+ by using our knowledge about the amount of "jumps" necessary to go from EA+ to an intermediate theory T and from T to PA + Con(PA). We shall see how Schmerl's Thoerem provides an alternative and easier proof of this fact and we will see some generalizations.

Speaker: Ana Borges
Title: Smooth Turing progressions
Date: Wednesday, May 23, 2018
Time: 12:30-14:00
Location: Logic Seminar

Abstract: We will show that PA + Con(PA) has the same Π1-consequences as the (ε0 + ε0)-th smooth Turing jump of EA+ by using our knowledge about the amount of "jumps" necessary to go from EA+ to an intermediate theory T and from T to PA + Con(PA).

Speaker: Daniel Ribeiro Sousa
Title: Formal epistemology: a primer and a surprising application
Date: Wednesday, May 16, 2018
Time: 12:15-13:15
Location: Logic Seminar

Abstract: We will see how to formalise the idea of "scientific knowledge" through an infinite game between a scientist and the devil. This means talking about what it means for an hypothesis to be decidable with a deadline, with certainty, in the limit and gradually. We will then apply this knowledge to talk about Regulation (EC) No 561/2006. If time permits, we will see the connections between the concepts introduced earlier with the Borel hierarchy.

Speaker: Fabian Romero
Title: Topological semantics for intuituionistic logic
Date: Wednesday, May 09, 2018
Time: 12:15-14:00
Location: Logic Seminar

Abstract: Intuitionistic logic is a natural framework to model several dynamic semantics. In this talk we will see a couple of topological interpretations: the classic one, and an alternative interpretation for the 'henceforth' modality which validates the Fisher Servi Axioms.

Speaker: Joost J. Joosten
Title: On conjunctions of bounded hyper arithmetical complexity but arbitrary length
Date: Wednesday, April 25, 2018
Time: 12:30-13:45
Location: Logic Seminar

Abstract: This talk is a continuation of previous week and as considers some aspects of the Turing Jump Interpretation (also called Münchhausen provability) of transfinite polymodal provability logic. Last week we saw how a straight-forward soundness proof does not allow for the separation of meta from object theory. If we had an artifact to express arbitrary long conjunctions of formulas of some (transfinitely) bounded complexity, then we can prove soundness with the object theory different from the meta-theory. However, the canonical way of writing such arbitrary long conjunctions makes use of a generalization of the Friedman-Goldfarb-Harrington theorem and as such requires quite heavy artillery from the object theory. We see how partial truth predicates can play an important role here.

Speaker: Joost J. Joosten
Title: Separating object-theory from meta-theory for Münchhausen provability
Date: Wednesday, April 18, 2018
Time: 12:15-13:45
Location: Logic Seminar

Abstract: This talk considers some aspects of the Turing Jump Interpretation (also called Münchhausen provability) of transfinite polymodal provability logic. In particular, we revisit how a straight-forward soundness proof does not allow for the separation of meta from object theory. If we had an artifact to express arbitrary long conjunctions of formulas of some (transfinitely) bounded complexity, then we can prove soundness with the object theory different from the meta-theory. However, the canonical way of writing such arbitrary long conjunctions makes use of a generalization of the Friedman-Goldfarb-Harrington theorem and as such requires quite heavy artillery from the object theory. We see how partial truth predicates can play an important role here.

Speaker: Joost J. Joosten
Title: On universal models of WC and RC
Date: Wednesday, March 14, 2018
Time: 12:15-13:45
Location: Logic Seminar

Abstract: We write RC for the reflection calculus and WC for the worm calculus. Both RC and WC are known to have the finite model property. We prove however that any universal model U of them is in essence infinite and inherits some complexity from Ignatiev's universal model I for the closed fragment of GLP. In particular, we show that for each point x on the main axis of I, there is a point y in U so that x and y have the same modal theory. However, in some sense, simplifications can be present. For example, we can restrict the order types of the accessibility relations to omega. This is joint work with Ana de Almeida Borges.

Speaker: Eduardo Hermo Reyes
Title: Relational semantics for TSC, Part III
Date: Wednesday, March 7, 2018
Time: 12:15-13:30
Location: Logic Seminar

Abstract: This talk is a continuation of previous week. As such, we study relational semantics for the system TSC_omega^\Lambda by considering a small variation on Ignatiev's frame. This is joint work with Joost J. Joosten.

Speaker: Eduardo Hermo Reyes
Title: Relational semantics for TSC, Part II
Date: Wednesday, February 21, 2018
Time: 12:15-13:30
Location: Logic Seminar

Abstract: This talk is a continuation of previous week. As such, we introduce relational semantics for the system TSC_omega^\Lambda by considering a small variation on Ignatiev's frame. This is joint work with Joost J. Joosten.

Speaker: Eduardo Hermo Reyes
Title: Relational semantics for TSC
Date: Wednesday, February 14, 2018
Time: 12:15-13:30
Location: Logic Seminar

Abstract: We introduce relational semantics for the system TSC_omega^\Lambda by considering a small variation on Ignatiev's frame. This is joint work with Joost J. Joosten.

Speaker: Joost J. Joosten
Title: Formalized conjunctions of arbitrary length
Date: Wednesday, February 07, 2018
Time: 12:15-13:30
Location: Logic Seminar

Abstract: In this session, we revisit the soundness proof of transfinite provability logic under the Turing jump interpretation. In the previous talks we saw how formalized reflexive transfinite induction helped us prove the arithmetical soundness of GLP_Lambda. In this talk, we finish this proof and observe that the proof disallows us to make a difference between the object and the meta theory which is undesirable. Thus, we will present an alternative proof by formalizing conjunctions of arbitrary length. In principle this requires much arithmetic but we will see that for our purposes we will only need to consider conjunctions of arbitrary length for formulas that shall be seen can be bound by some complexity measure. These bounds will take care that under some mild assumptions --that are needed anyway for the soundness proof-- we can mimic conjunctions of arbitrary length. This allows for a soundness proof where object and meta theory can be chosen differently.

Speaker: Joost J. Joosten
Title: Induction: internal, external, transfinite, reflexive, formalized and combinations thereof
Date: Wednesday, January 31, 2018
Time: 12:15-13:30
Location: Logic Seminar

Abstract: This session is a continuation of our session of two weeks ago. A such, we study a recursive equation for what we coined the Turing jump interpretation of transfinite polymodal provability logic. A theory that can express and prove this recursion up to some ordinal Lambda is called a GLP_Lambda amenable theory (GAT). We will show that for GATs, we can obtain soundness of the GLP axioms without many further assumptions on the base theory. However, we will need a form of transfinite induction since external transfinite induction does not suffice. At first sight the amount of induction seems huge but we shall see that things don't come that bad after all and ACA_0 will work. In this session we dwell on the subtleties between the various kinds of induction. In particular, we shall look at what is called reflexive transfinite induction.

Speaker: Joost J. Joosten
Title: The Turing Jump interpretation of modal logic revisited
Date: Wednesday, January 17, 2018
Time: 12:30-13:45
Location: Logic Seminar

Abstract: We study a recursive equation for what we coined the Turing jump interpretation of transfinite polymodal provability logic. A theory that can express and prove this recursion up to some ordinal Lambda is called a GLP_Lambda amenable theory (GAT). We will show that for GATs, we can obtain soundness of the GLP axioms without many further assumptions on the base theory. However, we will need a form of transfinite induction since external transfinite induction does not suffice. At first sight the amount of induction seems huge but we shall see that things don't come that bad after all and ACA_0 will work.

Speaker: Fabian Romero Jimenez
Title: Current trends in industry applications of software verification tools
Date: Tuesday, November 28, 2017
Time: 12:30-14:00
Location: Logic Seminar

Abstract:Software bugs have a combined cost of hundreds of millions of dollars and many human casualties. They disrupt essential services and cause uncountable other lesser damages.

Formal verification has made significant strides over the last years and has proven to be is a great way to reduce these risks. Today it is completely feasible to create verified software within sensible effort. Moreover, in mission-critical software, it is only reasonable and responsible to do so.

But even when feasible, it is still much harder to build verified software than "regular" software. Building software is still hard enough, for the "software crisis" is still well and alive.

Slides are available.

Speaker: Joost J. Joosten
Title: Soundness of GLP axioms from a recursive equation
Date: Wednesday, November 22, 2017
Time: 12:30-14:00
Location: Logic Seminar

Abstract: We define a recursive equation for what we coined the Turing jump interpretation of transfinite polymodal provability logic. A theory that can express and prove this recursion up to some ordinal Lambda is called a GLP_Lambda amenable theory (GAT). We will show that for GATs, we can obtain soundness of the GLP axioms without many further assumptions on the base theory.

Speaker: Eduardo Hermo Reyes
Title: Turing-Schmerl Calculus beyond \varepsilon_0
Date: Wednesday, November 15, 2017
Time: 12:30-14:00
Location: Logic Seminar

Abstract: We shall present the system TSC (Turing-Schmerl Calculus) tailored to express all principles that hold between different Turing progressions given a particular set of natural consistency notions and a recursive ordinal \Lambda. The system is proven to be arithmetically sound and complete for a natural interpretation, named the Formalized Turing Progressions Interpretation.

Joint work with Joost Joosten.

Speaker: Ana Borges
Title: Systems for nonstandard Heyting arithmetic
Date: Thursday, November 2, 2017
Time: 12:30-14:00
Location: Logic Seminar

Abstract: Our goal is to extend Gödel's dialectica interpretation to the nonstandard setting. In order to accomplish that, we start by describing systems for nonstandard Heyting arithmetic, which also include a new kind of type for sequences. See Section 3.1 of Borges' Master thesis.

Speaker: Ana Borges
Title: Gödel's dialectica interpretation
Date: Wednesday, October 25, 2017
Time: 12:30-14:00
Location: Logic Seminar

Abstract: In this session, armed with the knowledge of what Heyting Arithmetic in all finite types is, we will learn about Gödel's dialectica interpretation from a theoretical point of view, seeing what it does and how it works. We will also talk about ways it can be changed and applied to other theories of arithmetic. See Section 2.2 of Borges' Master thesis or this document also written by Ana Borges.

Date: Wednesday, October 4, 2017
Title: Heyting Arithmetic in all finite types
Speaker: Ana Borges
Time: 12:30 --14:00
Location: Logic Seminar Room

Abstract: First proposed as a way of reducing the consistency of Peano Arithmetic to the consistency of a quantifier-free version of Heyting Arithmetic, Gödel's dialectica interpretation ended up being the seed for a whole new tool of mathematics: proof mining. In this session, we will learn about the theory of (weakly extensional) Heyting Arithmetic in all finite types, which is the theory interpreted by the dialectica interpretation. This will give us the tools to study Gödel's interpretation in the next session.

Date: Thursday, June 15, 2017
Title: Complexity of alpha-equality in untyped lambda-calculus and separation of lambda-terms
Speaker: Andrea Condoluci
Time: 12:45 --13:45
Location: TBA

Abstract: Complexity of alpha-equality in untyped lambda-calculus and separation of lambda-terms

Date: Wednesday, April 19, 2017
Title: Decidability of some interpretability logics
Speaker: Luka Mikec
Time: 10:30 --12:00
Location: Logic Seminar Room

Abstract: The usual way to prove decidability of a modal logic with relational (Kripke-style) semantics is to prove it has the finite model property. Interpretability logics are usually interpreted on classes of Veltman models, or generalized Veltman models, which are both extensions of Kripke models. In this talk, we describe an approach to proving the finite model property by defining a certain filtration. We work with generalized Veltman models, and use maximal bisimilarity for gluing the worlds. We will sketch some issues that appear when trying to work with regular Veltman models. We will use this approach to prove decidability of the logic ILM_0. If time permits, we will also comment on decidability of ILW*, and possibly on the computational complexity of some interpretability logics.

Luka Mikec is an invited speaker from the University of Rijeka, Croatia (Department of Mathematics) and his travel is supported by the project 2016 DI 0032.

Date: Wednesday, March 22, 2017
Title: On the Turing Jump interpretation of transfinite provability logic and its formalizations II
Speaker: Joost J. Joosten
Time: 11:05 --12:05
Location: Logic Seminar Room

Abstract: We describe a recursive provability equation which is a transfinite generalization of "provable together with all true Pi_n formulas". We discuss the good properties of such a recursion equation and next dwell on the questions where such recursion is definable so that the basic properties become provable.

Date: Wednesday, March 15, 2017
Title: On the Turing Jump interpretation of transfinite provability logic and its formalizations I
Speaker: Joost J. Joosten
Time: 11:05--12:05
Location: Logic Seminar Room

Abstract: We describe a recursive provability equation which is a transfinite generalization of "provable together with all true Pi_n formulas". We discuss the good properties of such a recursion equation and next dwell on the questions where such recursion is definable so that the basic properties become provable.

Date: Thursday, March 9, 2017
Title: Transfinite Turing Jumps
Speaker: Joost J. Joosten
Time: 11:05
Location: 12:05

Abstract: We dwell on transfinite iterations of the Turing jump and discuss the various degree structures endowed with these jumps.

Date: Wednesday, March 1, 2017
Title: Vaught's conjecture in Computability theory
Speaker: Antonio Montalban
Time: 11:05-12:05
Location: Room 401, Philosophy Department, C. Montalegre 6

We have decided to allocate this as a session of the Barcelona Logic Seminar.

Abstract: We'll describe Vaught's conjecture, which is one of the most well-known and longest-standing open questions in logic. The conjecture essentially says that the continuum hypothesis holds when restricted to counting the number of models of a theory. We'll mention the author's result that this conjecture is equivalent to a computability-theoretic statement. No background knowledge will be assumed.

Date: Wednesday, January 25, 2017
Title: Caristi's theorem in reverse mathematics
Speaker: David Fernánuez-Duque
Time: 11:05-12:05
Location: Logic Seminar

Abstract: Caristi's theorem is a fixed-point result in dynamical systems. Unlike many related results, it applies to possibly discontinuous functions. This makes it a challenge to analyze it in the context of reverse mathematics, where theorems in analysis are formalized using the natural numbers and its powerset, suitable for reasoning about real numbers and continuous functions. In this talk, we will discuss Caristi's result and show that it can be formalized using only arithmetical comprehension; however, we note that a stronger version of the result can be extracted from the original proof. As we will show, this strong Caristi theorem is equivalent to the arithmetical inflationary fixed point scheme, a theory which is much stronger than any of the 'big five' systems of reverse mathematics.

Date: Wednesday, November 9, 2016
Title: Transfinite Turing Jumps and Provability
Speaker: Joost J. Joosten
Time: 11:05-12:05
Location: Logic Seminar

Abstract: We will study definability of subsets of the natural numbers in terms of provability predicates and relate this to the well known hierarchy of Turing jumps. Our emphasis will be on the hyperarithmetical sets. We present work in progress on how exactly our new notion of provability runs in phase with the hierarchy of Turing jumps. Apart from providing some preliminary results, we will give an ample motivation for the project. In particular, it seems that recent algebraic formulations of the so-called Reduction Property will prove useful once the exact relation between Turing jumps and provability predicates is in place.

Date: Wednesday, October 26, 2016
Title: Turing Jumps and provability
Speaker: Joost J. Joosten
Time: 11:05-12:05
Location: Logic Seminar

Abstract: We will study definability of subsets of the natural numbers in terms of provability predicates and relate this to the well known hierarchy of Turing Jumps. We start with the arithmetical hierarchy and next make our first explorations into the realm of hyperarithmetical sets.

Date: Wednesday, October 19, 2016
Title: First steps towards logic of informal provability, II
Speaker: Pawel Pawlowski (Ghent University)
Time: 11:05-12:05
Location: Logic Seminar

Abstract: Mathematicians prove theorems. They don't do that in any particular axiomatic system. Rather, they reason in a semi-formal setting, providing what we'll call informal proofs. There are quite a few reasons not to reduce informal provability to formal provability within some appropriate axiomatic theory. But the main worry is that we seem committed to all instances of the so-called reflection schema, which roughly says that if something is provable then it is true. Yet, adding all its instances to any theory for which other intuitive principles of provability hold leads to inconsistency. We develop a non-functional many-valued logics which avoid this problem and captures our intuitions about informal provability. The logics are inspired by paraconsistent logic CLuN, in whose standard semantics the value of a negation is not determined by the value of its argument. We describe the semantics of our logics and some of their properties.

The second part will enter into the details of a new proposal whereas the first part of the talk, two weeks ago, merely set the stage and intended to provide motivation and background.

Date: Wednesday, October 5, 2016
Title: First steps towards logic of informal provability, I
Speaker: Pawel Pawlowski (Ghent University)
Time: 11:05-12:05
Location: Logic Seminar

Abstract:
Mathematicians prove theorems. They don't do that in any particular axiomatic system. Rather, they reason in a semi-formal setting, providing what we'll call informal proofs. There are quite a few reasons not to reduce informal provability to formal provability within some appropriate axiomatic theory. But the main worry is that we seem committed to all instances of the so-called reflection schema, which roughly says that if something is provable then it is true. Yet, adding all its instances to any theory for which other intuitive principles of provability hold leads to inconsistency. We develop a non-functional many-valued logics which avoid this problem and captures our intuitions about informal provability. The logics are inspired by paraconsistent logic CLuN, in whose standard semantics the value of a negation is not determined by the value of its argument. We describe the semantics of our logics and some of their properties.

Date: Wednesday, September 21, 2016
Title: The Topological Completeness of GLP_Lambda
Speaker: Juan Pablo Aguilera (Vienna University of Technology)
Time: 16:30-17:30
Location: Philosophy Seminar (fourth floor of Carrer Montalegre 6, the room next to the Aula Magna)

Abstract:
We sketch the proof of the fact that any tall-enough scattered space can be extended to a model of the polymodal provability logic GLP_Lambda.

Date: Tuesday, September 20, 2016
Title: Numerical Approximations to Non-computable Functions for Graph and Tensor Complexity
Speaker: Hector Zenil (Karolinska Institute and Oxford University)
Time: 16:30-17:10
Location: Theoretical Philosophy Seminar Room (4085)

Abstract:
I will show that real-value approximations of Kolmogorov-Chaitin complexity K(s) using the so-called Algorithmic Coding Theorem, as calculated from the output frequency of a large set of small deterministic Turing machines, is consistent with various theoretical and numerical expectations, such as an almost perfect correlation between number of instructions (program size) and string algorithmic frequency. I will also show that neither K(s) nor the number of instructions used manifest any correlation with Bennett's Logical Depth LD(s), other than what's predicted by the theory itself (shallow and non-random strings have low complexity for both K and LD). The agreement between the theory and the numerical calculations shows that despite the undecidability of these theoretical measures, the rate of convergence of approximations is stable enough to devise applications. I will show that numerical approximations of algorithmic complexity measures can be used to approach the challenge of string, graph and tensor complexity capturing important group-theoretic and topological properties. We explore a measure, based upon the concept of Algorithmic Probability, that elegantly connects to Kolmogorov complexity, and that provides a natural approach to n-dimensional algorithmic complexity by using n-dimensional deterministic Turing machines. Finally, these measures drawn from computability and complexity theories are used in fundamental problems of causality and in molecular biology experiments, thus coming all the way from theory to computer simulation to biological validation.

Location: History Seminar Room (4029)
Date: Wednesday, May 25, 2016
Time: 12:30-14:00
Title: A term model for the closed fragment of transfinite provability logic
Speaker: Joost J. Joosten

Abstract:
In this talk we will look at the well-known structure known as Ignatiev's model as a universal model for the closed fragment of the transfinite polymodal provability logic GLP. Our focus will not be to prove that indeed the model is universal, but rather we wish to understand why the model is as it is and if other structures would have served the same purpose. To answer this question we start out with a rather general set-up and shall see that, given some modeling choices, Ignatiev's model is the necessary outcome. Although we do not perform a Henkin construction, nor do we consider the canonical model, we do work with sets of worms and thereby refer to the resulting structure as a term model.

Location: History Seminar Room (4029)
Date: Wednesday, May 4, 2016
Time: 12:30-14:00
Title: Turing Taylor Expansions of Arithmetical Theories
Speaker: Joost J. Joosten

Abstract:
Analytic functions can be endowed with a Taylor expansion around any given point in its domain. In a sense, one can project an analytical function f on a basis of orthogonal monomials x^n and f can be written as some sum of such monomials. We shall see that for a large class of arithmetical theories T something similar holds. The monomials are replaced by Turing progressions over Elementary Arithmetic and natural theories T can be expressed as the union of these monomials. However, we only have orthogonality of the monomials on certain intervals. This is not a problem since we can show that any union of monomials is provably equivalent to one in such an interval. These intervals are seen to live in a well-known structure: Ignatiev's universal modal model of the closed fragment of Japaridze's polymodal provability logic GLP. This is very nice and thus, points in Ignatiev's model can be interpreted in various ways: Turing Taylor expansions of natural arithmetical theories, ordinals, natural sequences of iterating end-logarithms on ordinals, and of course, modal formulae. This cross-interpretability powers applicability of these polymodal provability logics which we shall discuss as well.

Location: Logic Seminar Room
Date: Thursday, April 7, 2016
Time: 12:30-14:00
Title: Labelled Tableaux for Interpretability Logics
Speaker: Tuomas Hakoniemi

Abstract:
We present labelled tableaux proof systems for interpretability logics. We give a base system for the basic interpretability logic IL and show how to extend the system for any interpretability logic that is sound and complete with respect to a class of IL-frames determined by a set of strict universal Horn sentences.

This is joint work with Joost J. Joosten.

Location: Logic Seminar Room
Date: Wednesday, February 3, 2016
Time: 12:30-14:00
Title: Metamathematics in bounded arithmetic
Speaker: Joost J. Joosten

Abstract:
Bounded arithmetic is tailored to capture and reason about the poly-time functions. We shall point out how one can formalize syntax in bounded arithmetic and perform simple inductive arguments. However, we do not have access to normal induction. Rather we shall work with what is called length induction or other types of induction. The idea is that you only need to do logarithmically (in the size of the number) many calls upon the induction hypothesis and not linearly many. Next we return our focus to the previous session and to the notion of relative interpretability as introduced by Tarski, Mostowski and Robinson. Recall that relative interpretations are widely used in mathematics and logic, for example to yield relative consistency proofs or undecidability results.

We shall see how the notion of relative interpretability can be formalized in different ways in bounded arithmetic. Next we shall discuss the Orey-Hájek characterization of relative interpretability and comment on where the various implications can be formalized.

Location: Logic Seminar Room
Date: Thursday, January 14, 2016
Time: 17:00-18:30
Title: Formalizations of relative interpretability
Speaker: Joost J. Joosten

Abstract:
We consider the notion of relative interpretability as introduced by Tarski, Mostowski and Robinson. Relative interpretations are widely used in mathematics and logic, for example to yield relative consistency proofs or undecidability results.

We shall see how the notion of relative interpretability can be formalized in different ways in arithmetic. These different ways coincide for stronger theories but yield different notions over weaker base theories. If time allows we shall discuss the Orey-Hájek characterization of relative interpretability.

Speaker: David Fernández Duque
Title: Transfinite reflection principles and systems of second-order arithmetic
Date: Wednesday, December 2, 2015
Time: 12:00-13:00
Location: Logic Seminar Room

Abstract:
A classic result of Kreisel and Lévy states that Peano Arithmetic is equivalent to uniform reflection over Primitive Recursive Arithmetic. We will show how this is not an isolated phenomenon, as the stronger three of the "Big Five" theories of reverse mathematics, ACA0, ATR0, and Π11-CA0, are also equivalent to strong reflection principles over the weakest of the Big Five, RCA0. Such principles are obtained by transfinitely iterating the ω-rule up to a suitable ordinal and allowing an oracle for an arbitrary set X. We will also discuss how these results may lead to a Π01 ordinal analysis of these theories, as Beklemishev has done for Peano Arithmetic. There are slides of the talk available.

Location: Logic Seminar Room
Date: Wednesday, March 18, 2015
Time: 13:00-14:15
Title: On the core logic for relative interpretability
Speaker: Joost J. Joosten

Abstract:
We shall look at various principles in the core logic of relative interpretability and shall prove them to be sound in any arithmetical theory strong enough to formalize coding of syntax. Next we shall look at modal semantics for the logic. Since we work with a binary modality, we will work with ternary accessibility relations.

Location: Logic Seminar Room
Date: Wednesday, March 4, 2015
Time: 13:00-14:15
Title: Logics for interpretabiilty
Speaker: Joost J. Joosten

Abstract:
A theory U interprets a theory V in the sense of Tarski, Mostowski and Robinson if there is some translation under which all theorems of V are provable in U (where quantifiers may be restricted to a domain specifier). One can formalize this notion in arithmetical theories that allow for coding of syntax. We will study the structural behavior of formalized interpretability between theories which are sentential extensions of an arithmetical base theory of some minimal strength and collect our findings in modal logics which are called interpretability logics.

We shall see that logics for interpretability are not as stable as logics for provability. It is an open problem to determine the core logic of basic interpretability logics.

Location: Logic Seminar Room
Date: Wednesday, January 28, 2015
Time: 13:00-14:15
Title: Countable omega models and predicative reflection
Speaker: Joost J. Joosten

Abstract:
We will use some classical results on countable omega-models in predicative analysis to show that predicative analysis proves predicative Π12-reflection. Basically, predicative Π12-reflection says that whenever we can prove that a certain ordering is a well-order, then all Π12-statements that we can prove using omega-rules along this well-order are actually true. This is joint work with Andrés Cordon Franco, David Fernández Duque and Félix Lara Martín.

Location: Logic Seminar Room
Date: Wednesday, January 14, 2015
Time: 13:00-14:15
Title: Rosser-style arguments
Speaker: Joost J. Joosten

Abstract:
Rosser could prove a strengthening of Goedel's First Incompleteness Theorem in that he only required the c.e. theory with sufficient number theory to be consistent for it to be incomplete. We shall focus on the underlying technique of witnessing comparison. This technique can be used to prove the so-called Friedman-Goldfarb-Harrington Theorem to the extend that each Sigma formula is provably equivalent to some provability statement (modulo consistency). If time allows, we shall discuss this theorem, its generalizations and applications.

Location: Logic Seminar Room
Date: Wednesday, December 17, 2014
Time: 13:00-14:15
title: On formalized interpretability in not too strong theories of arithmetic
Speaker: Joost J. Joosten

Abstract:
A theory U interprets a theory V in the sense of Tarski, Mostowski and Robinson if there is some translation under which all theorems of V are provable in U (where quantifiers may be restricted to a domain specifier). One can formalize this notion in arithmetical theories that allow for coding of syntax. We will study the structural behavior of formalized interpretability between theories which are sentential extensions of an arithmetical base theory of some minimal strength and collect our findings in a modal logic.

Location: Logic Seminar Room
Date: Wednesday, October 29, 2014
Time: 13:00-14:15
title: Provability with a set-oracle
Speaker: Joost J. Joosten

Abstract:
We wish to characterize principles of second order arithmetic like comprehension or transfinite recursion in terms of reflection principles. In order to deal with second order set parameters in these principles we need to be able to denote such parameters in the context of formalized provability. We know that each number can be denoted by a name for it. In a countable language we cannot do so for sets of course. To overcome this obstacle we introduce the notion of oracle provability and see how this behaves and can be formalized in second order number theory.

This is joint work with Andrés Cordon Franco, David Fernández Duque and Félix Lara Martín.

Location: Logic Seminar Room
Date: Wednesday, October 29, 2014
Time: 13:00-14:15
title: On the intimate relations between reflection, consistency and induction
Speaker: Joost J. Joosten

Abstract:
We revisit classical results relating the intimate relations between reflection principles, consistency statements and fragments of first order arithmetic and shall dwell on the question how this can be extended to second order arithmetic.

Location: Logic Seminar Room
Date: Wednesday, May 28, 2014
Time: 12:15-14:00
title: Graded Turing progressions through modal logic
Speaker: Euardo Hermo-Reyes

Abstract:
Graded Turing progressions arise by iteratedly adding formalized n-consistency statements to a base theory using different natural numbers n. It is known that the modal logic GLP can be used to denote any finite level of these progressions. However, at transfinite levels, this link between GLP and Turing progressions is only by approximating the progression. We propose a new modal signature that can directly denote transfinite progressions and not only approximate them. We shall prove certain axioms of this logic to be arithmetically correct.

This is joint work with Laia Jornet-Somoza and Joost J. Joosten.

Location: Logic Seminar Room
Date: Wednesday, April 02, 2014
Time: 12:15-14:00
title: Reflexive transfinite induction and applications to formalized Turing progressions
Speaker: Joost J. Joosten

Abstract:
In weaker theories we do not have access to full arithmetic transfinite induction, even for small ordinals. For various statements, however, a weaker notion Reflexive transfinite induction suffices so that often EA can serve as a base theory. In case we need formalized collection we have to resort to a base theory where Sigma_1 collection in provable leading to accepting the totality of the hyper-exponential function. If all is in place, we can formalize well the notion of Turing progression and apply that as the basis for proof-theoretic analyses.

Location: Logic Seminar Room
Date: Wednesday, March 19, 2014
Time: 12:15-14:00
title: Formalizing transfinite progressions in the absence of transfinite induction
Speaker: Joost J. Joosten

Abstract:
Various natural transfinite progressions of theories of increasing strength are defined using provability. The natural way to reason about these progressions is by using transfinite induction. However, transfinite induction is quite a strong principle so that if we wish to formalize our reasoning this is bad. However, we can do better. Since the progressions are defined using provability, often we can formalize our reasoning in rather weak theories due to tricks based on Lüb's rule and the Outside Big, Inside Small principle. The latter asserts that, although not all elements are inside any definable cut, they are provably so! We revisit these tricks resulting in among others what is called Reflexive Induction. Next we shall see how this can be put to work to formalize various transfinite progressions in Elementary Arithmetic. If time allows we shall move on to see some applications.

Location: Logic Seminar Room
Date: Wednesday, January 22, 2014
Time: 12:15-14:00
title: An empirical logician's apology
Speaker: Joost J. Joosten

Abstract:
In this talk we see how running simulations of small Turing machines on super-computers reveals an unexpected and new relation between geometrical complexity (fractal dimension) on the one hand and computational complexity on the other hand. After presenting the results we shall try to place them in the panorama of various other --relevant to our research-- results, that relate different notions of complexity to each other. This is joint work with Hector Zenil from Unit of Computational Medicine, Center for Molecular Medicine, Karolinska Institutet, and Fernando Soler-Toscano from the University of Sevilla.

Location: Logic Seminar Room
Date: Wednesday, January 8, 2014
Time: 12:15-14:00
title: Logics for Turing progressions
Speaker: Joost J. Joosten

Abstract:
The logics of GLP and RC are nice in that they have good algebraic, logical and computational properties and moreover provide an alternative ordinal notation system. The applicability of the logics GLP and RC to proof theory is mainly given through the link to Turing progressions. Finite Turing progressions can be explicitly given by a modal formula. For transfinite Turing progressions we only have approximations. In this talk we wish to start an investigation to see, on the one hand, to what extend we can expand the expressibility of the modal language to better speak of Turing progressions while, on the other hand, still maintain the nice properties of the logics. In particular we shall present a logic of Beklemishev's that has for each ordinal α below ε0 a modality [α] that will be interpreted as provability in the αth Turing progression.

Location: Logic Seminar Room
Date: Wednesday, December 18, 2013
Time: 12:15-14:00
title: HOTT Reading group
Speaker: Cory Knapp

Abstract:
An overview of univalence and higher inductive types.

Location: Logic Seminar Room
Date: Wednesday, November 27, 2013
Time: 12:15-14:00
title: HOTT Reading group
Speaker: Cory Knapp

Abstract:
We will quickly cover coproducts, booleans and natural numbers, and spend the rest of the time dwelling on identity types.

Location: Logic Seminar Room
Date: Wednesday, November 20, 2013
Time: 12:15-14:00
title: PSPACE completeness of the closed fragment of GLP
Speaker: Joost J. Joosten

Abstract:
It is known that the closed fragment of GL is decidable (theoremhood) in PTIME. Bou and the author showed that some extension of GL by adding a binary modal operator for interpretability yields a PSPACE complete closed fragment. In this presentation we shall look at a result of Pakhomov to the extent that the closed fragment of GLP is also PSCPACE complete.

Location: Logic Seminar Room
Date: Wednesday, November 13, 2013
Time: 12:15-14:00
title: Homotopy Type Theory
Speaker: Cory Knapp

Abstract:
We spoke on introduction, elimination and computation rules and in particular dwelt on (dependent) product and W-types.

Location: Logic Seminar Room
Date: Wednesday, November 06, 2013
Time: 12:15-14:00
title: TBA
Speaker: Joost J. Joosten

Abstract:
We saw how questions about the xi-consistency ordering can be reduced to simplified questions. In particular we saw a recursive reduction to the 0-consistency ordering.

Location: Logic Seminar Room
Date: Wednesday, October 30, 2013
Time: 12:15-14:00
title: Homotopy Type Theory
Speaker: Cory Knapp

Abstract:
TBA

Location: Logic Seminar Room
Date: Wednesday, October 23, 2013
Time: 12:15-14:00
title: Combinatorics in formal provability
Speaker: Paul Erdös

Abstract:
Of course, this is a silly joke.

Location: Logic Seminar Room
Date: Wednesday, October 23, 2013
Time: 12:15-14:00
title: Homotopy Type Theory
Speaker: Cory Knapp

Abstract:
We discuss motivations for HOT and introduce some basic formation, elimination and computation rules.

Location: Logic Seminar Room
Date: Wednesday, October 15, 2013
Time: 12:15-14:00
title: The worm project: current state of affairs
Speaker: Joost J. Joosten

Abstract:
In this talk, we have given an overview of recent results in the Pi^0_1 ordinal analysis project.

Location: Logic Seminar Room
Date: Wednesday, May 15, 2013
Time: 12:15-14:00
title: Well-founded orders and anti-chains in the Japaridze Algebra
Speaker: Joost J. Joosten

Abstract:
It is known that we can order the class of all worms according to consistency strength. For regular consistency this yields a well-order. For higher consistency notions the relation is still well-founded, yet no longer linear, containing wild structures of anti-chains.

Location: Logic Seminar Room
Date: Wednesday, May 8, 2013
Time: 12:15-14:00
title: Predicativism and the foundations of mathematics
Speaker: Joost J. Joosten

Abstract:
In this session we discuss writings of Feferman on Predicativism and the foundations of mathematics.

Location: Logic Seminar Room
Date: Wednesday, April 24, 2013
Time: 12:15-14:00
title: Topological models of GLP and set theory II
Speaker: Joan Bagaria

Abstract:
In this talk we discuss which large cardinal assumptions are needed for certain natural topologies to be non-discrete. The non-discreteness in turn is needed for completeness proofs for natural topological interpretations of GL and GLP.

Location: Logic Seminar Room
Date: Wednesday, April 17, 2013
Time: 12:00-14:00
title: Impredicative provability logic
Speaker: David Fernández Duque

Abstract:
Recent work by Joosten and the speaker shows how Japaridze's polymodal provability logic GLP may be interpreted using iterated omega-rules. This in turn suggests a strategy for extending Beklemishev's technique for computing Pi^0_1-ordinals to predicative theories of second-order arithmetic, whose proof-theoretic strength is bounded by the Feferman-SchŸtte ordinal Gamma_0. However, the analysis of stronger theories, such as the theory ID_1 of inductive definitions, typically involves the study of potentially uncountable proofs. Such proofs cannot be directly modeled using omega-rules. To this end, in this talk we shall introduce provability operators based on an uncountable well-order. Given a cardinal k, one considers a k-rule, which has one premise for each x<k. Such a rule may be iterated transfinitely, much as the omega-rule. We shall show that this gives rise to a proof-theoretic interpretation for the polymodal provability logic enriched with uncountable modalities, and discuss how ID_1 may be represented within this framework.

Location: Logic Seminar Room
Date: Wednesday, April 03, 2013
Time: 12:15-14:00
title: Topological models of GLP and set theory
Speaker: Joan Bagaria

Abstract
In this talk we discuss which large cardinal assumptions are needed for certain natural topologies to be non-discrete. The non-discreteness in turn is needed for completeness proofs for natural topological interpretations of GL.

Location: Logic Seminar Room
Date: Wednesday, March 20, 2013
Time: 12:15-14:00
title: Omega completeness for ∏11 sentences
Speaker: Joost J. Joosten

Abstract
In this session we look at one-sided Tait calculus for pseudo ∏11 sentences. We prove that the truth complexity of true ∏11 sentences is always below ω1CK.

Location: Logic Seminar Room
Date: Wednesday, March 13, 2013
Time: 12:15-14:00
title: Truth complexity for ∏11 sentences
Speaker: Joost J. Joosten

Abstract
In this session we look at one-sided Tait calculus for Second Order Logic and fragments. Next we introduce the truth complexity of formulas and analyze the truth complexity of true ∏11 sentences.

Location: Logic Seminar Room
Date: Wednesday, March 6, 2013
Time: 12:15-14:00
title: Arithmetical Completeness of Gšdel Lšb Provability logic
Speaker: Joost J. Joosten

Abstract
In this presentation we present Solovay's classical proof to the extent that GL is complete for its provability interpretation in Peano Arithmetic. We shall use arithmetical soundness as given in this presentation.

Location: Logic Seminar Room
Date: Wednesday, February 27, 2013
Time: 12:15-14:00
title: Sequent calculi, completeness and a non-constructive cut-elimination proof
Speaker: Joost J. Joosten

Abstract
We will study Tait's one-sided cut-free calculus in more detail. We shall prove completeness of this calculus using Schütte's method of search-trees. Once we have completeness it is easy to see that the cut-rule is admissible in this calculus yielding a non-constructive proof of cut-elimination.

Location: Logic Seminar Room
Date: Wednesday, February 20, 2013
Time: 12:15-14:00
title: Sequent calculi, first and second order
Speaker: Joost J. Joosten

Abstract
In this session we shall look at various sequent calculi. In particular we will study Tait's one-sided cut-free calculus and its main properties.

Location: Logic Seminar Room
Date: Wednesday, February 13, 2013
Time: 12:15-14:00
title: Normalization for Natural Deduction
Speaker: Joost J. Joosten

Abstract
In this session we presented a classical result on normalization/cut-elimination in a Natural Deduction proof system for Predicate Logic yielding a syntactic consistency proof of Predicate Logic.

Location: Logic Seminar Room
Date: Wednesday, January 23, 2013
Time: 12:15-14:00
title: Introspective theories and the omega rule
Speaker: Joost J. Joosten

Abstract
In this session we shall prove the two most involved GLP axioms correct for our omega-rule interpretation. We shall see that we need to assume the existence of a provability predicate to prove soundness of our Euclidean axiom < a > A --> [b] <a> A for a<b. However, we shall prove that each theory is equi-consistent with one that has a provability predicate. We call such theories introspective. Moreover, we see that introspective theories are provably introspective.

Joint work with David Fernández Duque.

Location: Logic Seminar Room
Date: Wednesday, December 19, 2012
Time: 12:15-14:00
title: Fragments of second order arithmetic
Speaker: Joost J. Joosten

Abstract
In this session we will focus on some main systems of second order arithmetic like Arithmetic Transfinite Recursion, Arithmetic Comprehension Axioms, and Recursive Comprehension Axioms. Moreover, we shall see what can be proven in these respective systems about formalized transfinite provability. We shall relate the existence of transfinite provability predicates to principles of transfinite induction.

Joint work with David Fernández Duque.

Location: Logic Seminar Room
Date: Wednesday, November 21, 2012
Time: 12:15-14:00
title: The omega rule interpretation of transfinite provability logics
Speaker: Joost J. Joosten

Abstract
In this session we will derive some first provable basic results when interpreting [α]T as "provable in T using a proof tree with at most α many nested applications of the omega-rule". It is our aim to see that the logic thus defined will be GLP again.

Joint work with David Fernández Duque.

Location: Logic Seminar Room
Date: Wednesday, November 11, 2012
Time: 12:15-14:00
title: Omega rules formalized in Second Order Arithmetic
Speaker: Joost J. Joosten

Abstract
We shall see how to formalize the notion of being provable by transfinitely iterated applications of the omega rule in second order number theory.

Joint work with David Fernández Duque.

Location: Logic Seminar Room
Date: Wednesday, October 24, 2012
Time: 12:15-14:00
title: Omega rules
Speaker: Joost J. Joosten

Abstract
We will discuss omega-rules, their history, their applications and possible systems where to formalize the notion of being provable by transfinitely iterated applications of the omega rule.

Location: Logic Seminar Room
Date: Wednesday, May 16, 2012
Time: 12:15-14:00
title: Ordinal analysis for set theory and fragments
Speaker: Joost J. Joosten

Abstract
We shall explore possible set-theoretical interpretations of the poly-modal provability logic GLP. In particular, we shall look at ZFC minus Replacement and Infinity as our base theory. By a result of Levy it is known that adding reflection to this base theory gives us full ZFC again. Applying techniques from consistency proofs based on GLP gives us some indefinability results over this weak base theory.

Joint work with Joan Bagaria.

Location: Logic Seminar Room
Date: Wednesday, May 2, 2012
Time: 12:15-14:00
title: Π01 Ordinal analysis beyond Peano arithmetic
Speaker: Joost J. Joosten

Abstract
We strip the consistency proof of PA based on GLP from all unnecessary ingredients and try to milk this analysis. In particular, we note that only arithmetical soundness of GLP is needed for a consistency proof. Also we simplify the reduction property and note that as such this property is not needed in full generality for a consistency proof. Moreover, we sketch how this method can be used to obtain ordinal analyses relative to strong base theories.

Location: Logic Seminar Room
Date: Wednesday, March 28, 2012
Time: 12:15-14:00
title: Model constructions for the closed fragment of GLP
Speaker: Joost J. Joosten

Abstract
For GLPω we have a very good understanding of the universal model for the closed fragment. In particular we have various ways to look at this model and construct it. There is a definition around in terms of ordinal coordinates and there is a way how to define the model in terms of directed limits. For GLPΛ with Λ > ω we only have the definition in terms of ordinal coordinates. In this talk we put forward a natural candidate to also have directed limits for this case. Moreover, we also try to address the problem of the dependence of our ordinal notation system since our candidate essentially works with Veblen Normal Form representations of ordinals.

Joint work with Enrique Casanovas.

Location: Logic Seminar Room
Date: Wednesday, March 21, 2012
Time: 12:15-14:00
title: A consistency proof of Peano Arithmetic
Speaker: Joost J. Joosten

Abstract
In this session we provide a consistency proof of PA based on GLP in full detail. The proof we present is due to Beklemishev.

Location: Logic Seminar Room
Date: Wednesday, March 7, 2012
Time: 12:15-14:00
title: Ordinal analysis based on Turing progressions
Speaker: Joost J. Joosten

Abstract
We see how Turing progressions can be used to obtain various ordinal analyses. Currently the state of art lies at Π0n analyses with n ∈ω but it is likely to generalize this.

Location: Logic Seminar Room
Date: Wednesday, February 22, 2012
Time: 12:15-14:00
title: Worms and Turing progressions
Speaker: Joost J. Joosten

Abstract
We shall see how generalized notions of consistency statements can be naturally employed to talk about Turing progressions. Moreover, our worms are seen to be sufficient for many purposes in this project.

Location: Logic Seminar Room
Date: Wednesday, February 8, 2012
Time: 12:15-14:00
title: Hyper-exponentials
Speaker: Joost J. Joosten

Abstract
In this sessions we shall look at how to transfinitely iterate normal functions in a non-trivial way. We define a new notion that we call hyperations that can be seen as transfinite iteration and see what happens if we hyperate (a minor adaptation) ordinal exponentiation with base ω. We see that we end up with a sequence of normal functions that is a refinement of the well-known Veblen functions. Moreover, we shall also briefly discuss what we call cohyperations which can be seen as transfinite iterations of initial functions (ordinal functions that map initial segments to initial segments). Cohyperations, like hyperations, possess a rich algebraic structure and they provide natural left inverses to hyperations.

Joint work with David Fernández Duque.

Location: Logic Seminar Room
Date: Wednesday, January 25, 2012
Time: 12:15-14:00
title: Ordinal assignments for worms beyond GLPω
Speaker: Joost J. Joosten

Abstract
This session is a natural follow-up to the previous ones where we now consider the general case for any worms. The formalism we present is new in that it uses special ordinal functions.

Joint work with David Fernández Duque.

Location: Logic Seminar Room
Date: Wednesday, January 11, 2012
Time: 12:15-14:00
title: Ordinal assignments for worms in GLPω
Speaker: Joost J. Joosten

Abstract
To each worm A, we can assign an ordinal o(A) in a very natural way. We look at the collection of worms B whose consistency follows from A and order this collection under the relation of implying consistency. The corresponding order type of this collection is our ordinal assignment o(A). We will provide a known calculus as presented by Beklkemishev but provide new proofs.

Joint work with David Fernández Duque.

Location: Logic Seminar Room
Date: Wednesday, December 14, 2011
Time: 12:15-14:00
title: Well-orders in GLP
Speaker: Joost J. Joosten

Abstract
We shall discuss how the transfinite Japaridze algebra naturally lodges various interesting well-orders. In later sessions we shall see that these well-orders are actually very informative in a well-defined proof-theoretical sense.

Joint work with David Fernández Duque.

Location: Logic Seminar Room
Date: Wednesday, November 30, 2011
Time: 12:15-14:00
title: Models for GLPω
Speaker: Joost J. Joosten

Abstract
We shall see that GLPω in general is Kripke incomplete. In particular the various frame conditions would enforce us to only consider trivial models. However the closed fragment does allow for natural Kripke semantics as was pointed out by Ignatiev. We present a purely modal presentation of Ignatiev's model here and prove the model to be sound and complete for GLPω.

Joint work with Marco Vervoort and Lev Beklemishev.

Location: Logic Seminar Room
Date: Wednesday, September 28, 2011
Time: 12:15-14:00
title: Beklemishev Normal Forms
Speaker: Joost J. Joosten

Abstract
There are various different worms that are actually equivalent over GLP. We will see that the class of worms has a subset of natural unique representatives which we baptize Beklemishev Normal Forms. We slightly change the existing definition of Worm Normal Form as to emphasize its similarities with Cantor Normal Forms.

Location: Logic Seminar Room
Date: Wednesday, June 15, 2011
Time: 12:15-14:00
title: Worms in GLP
Speaker: Joost J. Joosten

Abstract
We look at iterated consistency statements within GLP which are called worms. We show some basic facts about them. In particular we shall see that they are closed under conjunction.

Location: Logic Seminar Room
Date: Wednesday, June 1, 2011
Time: 12:15-14:00
title: On the closed fragment of GLP
Speaker: Joost J. Joosten

Abstract
We shall focus on the closed fragment of GLP. In particular we see that each closed formulas can be written as a Boolean combination of worms.

Location: Logic Seminar Room
Date: Wednesday, May 18, 2011
Time: 12:15-14:00
title: Non-discreteness of Derived Topologies is Independent of ZFC
Speaker: Joan Bagaria

Abstract
In this talk we continue the previous lecture. We shall see that the non-discreteness of the next topology is independent of ZFC at every level.

Location: Logic Seminar Room
Date: Tuesday, May 12, 2011
Time: 12:15-14:00
title: On Derived Topologies
Speaker: Jaon Bagaria

Abstract
We shall look at derived topologies on ordinal spaces. In particular we define a hierarchy of nested topologies. Here each next topology is extending the previous one by adding all derived sets (in terms of the Mahlo operator) as new open sets. We prove some basic properties of these topologies and link them to well-known set-theoretical notions.

Location: Logic Seminar Room
Date: Wednesday, December 12, 2011
Time: 12:15-14:00
title: Topological Completeness for GLB
Speaker: Joost J. Joosten

Abstract
We present the topological completeness (using Jensen's square principle up to ℵω) result for GLB as proven by Beklemishev. Blass' result on topological interpretations of GL is a central ingredient here.

Location: Logic Seminar Room
Date: Wednesday, April 6, 2011
Time: 12:15-14:00
title: Topological spaces: trees versus partitions
Speaker: Joost J. Joosten

Abstract
We shall see how we can embed finite trees into topological spaces. For this purpose we essentially rely on Blass' results on topological interpretations of GL. Embedding trees is a first step in a completeness proof for GL à la Solovay.

Location: Logic Seminar Room
Date: Wednesday, March 16, 2011
Time: 12:15-14:00
title: Topological Semantics for GLB
Speaker: Joost J. Joosten

Abstract
We present topological semantics for modal logics based on either the interior operator or the derived set operator. We shall see that the latter is good for topological semantics for GL when using scattered spaces.

Joint work with David Fernández Duque.