**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*.

Johan van Benthem | 26-01-2024 |

Johan van Benthem | 24-01-2024 |

Yannick Forster | 11-01-2024 |

Konstantinos Papafilippou | 07-05-2023 |

Fedor Pakhomov | 07-03-2023 |

Yannick Forster | 27-04-2022 |

Denis Merigoux | 27-04-2022 |

Joost J. Joosten | 20-04-2022 |

Moritz Müller | 23-02-2022 |

Ana de Almeida Borges | 26-01-2022 |

Sam Sanders | 17-03-2021 |

Ana de Almeida Borges | 24-02-2021 |

Konstantinos Papafilippou | 04-02-2021 |

Konstantinos Papafilippou | 21-01-2021 |

Fedor Pakhomov | 15-04-2020 |

Joost J. Joosten | 25-03-2020 |

Tommaso Moraschini | 18-03-2020 |

Joost J. Joosten | 04-03-2020 |

Luka Mikec | 28-02-2020 |

Michal Garlik | 19-02-2020 |

David Fernández Duque | 13-02-2020 |

Mateusz Łełyk | 07-02-2020 |

Mateusz Łełyk | 06-02-2020 |

Cyril Cohen | 29-01-2020 |

Mateusz Łełyk | 04-02-2020 |

Mateusz Łełyk | 03-02-2020 |

Luka Mikec | 23-01-2020 |

Joost J. Joosten | 22-01-2020 |

Joost J. Joosten | 17-12-2019 |

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: Johan van Benthem

Title: Interleaving logic and counting, a new view of combined logical-arithmetical systems

Date: Friday, January 26, 2024

Time: 11:00 - 12:00 +

Location: Aula T1. Facultat de Matemàtiques i Informàtica (UB). Gran Via de les Corts Catalanes 585.

This talk is embedded in the Barcelona Logic Seminar, see SLB announcement .

Reasoning patterns in natural language combine logical and arithmetical features, transcending divides between qualitative and quantitative. This natural practice blends into ‘grassroots mathematics’ such as using pigeon-hole principles. And from these basic abilities everyone has, the trail leads to the pinnacles of abstract mathematics.

In the foundations of science and philosophy, one often finds a hierarchy: ‘logic first, arithmetic later”, or the other way around. However, our topic is the cooperation of logic and counting on a par, studied with small formal systems and gradually extending these. We show what can be defined, and where complexity barriers arise, through connections with classical results in mathematical logic.

After this, we return to natural language, confronting our formal systems with linguistic quantifier vocabulary, monotonicity reasoning, and procedural semantics. We conclude with some challenges coming from the cognitive psychology of reasoning and the possible need to remodel what we mean by ‘counting’.

Ref. J. van Benthem & Th. Icard, Interfacing Logic and \Counting, Bulletin of Symbolic Logic, autumn 2023.

See an ILLC preprint

Speaker: Johan van Benthem

Title: Logic, Epistemology, and Evidence Dynamics

Date: Wednesday, January 24, 2024

Time: 15:00 - 17:00

Location: Philosophy Seminar Room (TBC)

This talk is embedded in the Barcelona Institute of Analytic Philosophy, see BIAP announcement .

Logic and epistemology have long interacted in various ways. We will give a historical sketch of some main themes and open problems in this encounter, with an emphasis on the role of evidence and the dynamic effects of new information.

Speaker: Yannick Forster

Title: Markov’s Principles in Constructive Type Theory

Date: Thursday, January 11, 2024

Time: 10:30 - 12:00

Location: Ramon Llull Seminar Room (Room 4047)

Markov’s principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ

We give three variants of MP in constructive type theory, along with respective equivalence proofs to different formulations of Post’s theorem (“Σ

We conclude with the – to the best of our knowledge – first separation of these three principles for type theory, using a model via Cohen and Rahli’s TT□C based on ideas by Kreisel (1959) and Smorynski (1973).

Joint work with Liron Cohen, Dominik Kirst, Bruno da Rocha Paiva, and Vincent Rahli.

Speaker: Konstantinos Papafilippou

Title: On the succinctness of the fixed-point theorem of GL

Date: Monday, May 7, 2023

Time: 11:30 - 12:30

Location: Maria Zambrano Seminar (Room 4029)

The fixed-point theorem of provability logic is a classical result first proved independently by D. de Jongh and G. Sambin in 1975 (Sambin 1976). It states that for GL formulae φ(p) of a specific form, there is a formula ψ such that GL ⊢ψ ↔ φ(ψ). We will first provide a constructive proof of the fixed point theorem, showing that the formula ψ can only be at most a (approximately) exponentially as succinct as φ. We will then show that the fixed points of GL are a bit more than exponentially as succinct, ie, we will present a sequence for formulae φ0,φ1,... such that any fixed point ψi of a φi has at least exponential size relative to the size of φi.

If time permits, I'll also give a short presentation of my work on the topological μ-calculus and a bit from the motivation that made us ask this question.

Speaker: Fedor Pakhomov

Title: Dilators, Reflection, and Forcing: A Proof-Theoretic Analysis of Π

Date: Tuesday, March 7, 2023

Time: 12:20 - 13:20

Location: Maria Zambrano Seminar (Room 4029)

In this talk I will sketch a new approach to ordinal analysis of Π

The talk will also be broadcasted via streaming. Please ask Sofia Santiago for details about the streaming.

Speaker: Yannick Forster

Title: Verified extraction to OCaml from Coq, in Coq

Date: Wednesday, April 27, 2022

Time: 12:00 - 13:00

Location: Ramon Llull

This is joint work with Matthieu Sozeau, Pierre Giraud, Pierre-Marie Pédrot, and Nicolas Tabareau.

The MetaCoq project provides a formalisation of PCUIC, the calculus underlying the Coq proof assistant, in the Coq proof assistant. We have verified Letouzey's type and proof erasure from PCUIC to an untyped lambda calculus called lambda_box, which is central in Coq's extraction to OCaml. We are now working on re-implementing Coq's extraction to OCaml in a verified way in MetaCoq, by choosing as target the Malfunction intermediate language of the OCaml compiler.

Yannick used slides from here and here.

Speaker: Denis Merigoux

Title: Catala: A Programming Language for the Law

Date: Wednesday, April 27, 2022

Time: 11:00 - 12:00

Location: Ramon Llull (tbc)

Law at large underpins modern society, codifying and governing many aspects of citizens' daily lives. Oftentimes, law is subject to interpretation, debate and challenges throughout various courts and jurisdictions. But in some other areas, law leaves little room for interpretation, and essentially aims to rigorously describe a computation, a decision procedure or, simply said, an algorithm. Unfortunately, prose remains a woefully inadequate tool for the job. The lack of formalism leaves room for ambiguities; the structure of legal statutes, with many paragraphs and sub-sections spread across multiple pages, makes it hard to compute the intended outcome of the algorithm underlying a given text; and, as with any other piece of poorly-specified critical software, the use of informal language leaves corner cases unaddressed. We introduce Catala, a new programming language that we specifically designed to allow a straightforward and systematic translation of statutory law into an executable implementation. Catala aims to bring together lawyers and programmers through a shared medium, which together they can understand, edit and evolve, bridging a gap that often results in dramatically incorrect implementations of the law. We have implemented a compiler for Catala, and have proven the correctness of its core compilation steps using the F* proof assistant. We evaluate Catala on several legal texts that are algorithms in disguise, notably section 121 of the US federal income tax and the byzantine French family benefits; in doing so, we uncover a bug in the official implementation. We observe as a consequence of the formalization process that using Catala enables rich interactions between lawyers and programmers, leading to a greater understanding of the original legislative intent, while producing a correct-by-construction executable specification reusable by the greater software ecosystem.

Slides can be found here.

Speaker: Joost J. Joosten

Title: Definite descriptions in modal logic

Date: Wednesday, April 20, 2022

Time: 12:00 - 13:00

Location: Ramon Llull

There is much literature on the non-existing king of France being bald. A current school of Practical Philosophy proposes to reinstall French royal family with a bald king to put this discussion to an end. In this talk we will not enter this discussion. Rather, we will informally present a formal framework that combines quantified modal logic with definite descriptions so that we can express statements like "The king of France is necessarily bald".

Speaker: Moritz Müller

Title: On the parameterized complexity of Δ

Date: Wednesday, February 23, 2022

Time: 11:00 - 12:00

Location: Ramon Llull (end of the 4th floor office corridor of the Faculty of Philosophy, Carrer Montalegre 6)

We consider the problem, given a Δ

Speaker: Ana de Almeida Borges

Title: QRC

Date: Wednesday, January 26, 2022

Time: 12:00 - 13:00

Location: Maria Zambrano (Room 4029 (Faculty of Philosophy, Carrer Montalegre 6))

Coq is an interactive theorem prover with which one can write definitions, executable algorithms, statements, and machine-checked proofs. Convincing Coq that a proof is correct is usually harder than convincing a fellow mathematician, mostly because "obvious" details cannot be swept under the rug (unless the problem has been automated).

However, there are some exceptions. For example, the Four Color Theorem was first proved with the aid of a (non-formalized) algorithm, and the resulting proof was not particularly human-readable. This shed some doubt over the proof, eventually leading to a full Coq formalization. Even if one does not understand a Coq proof, it is easier to understand the formalized definitions and statements, and then trust that every accepted proof is correct.

The Quantified Reflection Calculus with one modality, denoted by QRC

QRC

Showing that QRC

In this talk I will share my progress on formalizing the Kripke soundness and completeness theorems for QRC

Speaker: Sam Sanders

Title: The Big Six and Big Seven of Reverse Mathematics

Date: Wednesday, March 17, 2021

Time: 17:00 - 18:00 CET

Location: Online

Reverse Mathematics (RM for short) is a program in the foundations of mathematics where the aim is to identify the minimal axioms needed to prove a given theorem from ordinary, i.e. non-set theoretic, mathematics. RM has unveiled surprising regularities: the minimal axioms are very often equivalent to the theorem over the base theory, a weak system of `computable mathematics', while most theorems are either provable in this base theory, or equivalent to one of only four logical systems. The latter plus the base theory are called the `Big Five’ of RM and the associated equivalences are robust following Montalban, i.e. stable under small variations of the theorems at hand. Working in Kohlenbach's higher-order RM, we obtain two long series of equivalences based on theorems due to Bolzano, Weierstrass, and Cantor; these equivalences are extremely robust and have no counterpart among the Big Five systems, as they are strictly between the base theory and the higher-order counterpart of weak König's lemma. In this light, higher-order RM is much richer than its second-order cousin, boasting as it does two extra `Big' systems. Time permitting, we connect these results to computability theory in the sense of Turing. Slides can be found here.

Speaker: Ana de Almeida Borges

Title: An escape from Vardanyan's Theorem

Date: Wednesday, February 24, 2021

Time: 17:00 - 18:00 CET

Location: Online

Vardanyan's Theorem states that quantified provability logic is Π

This is joint work with Joost J. Joosten. A first draft of the paper is already on the ArXiv and we also have some slides of the presentation.

Speaker: Konstantinos Papafilippou

Title: Boolos' Analytical completeness, part II

Date: Thursday, February 4, 2021

Time: 11:00 - 12:30 CET

Location: Online

A compelling interpretation of modal logic suggested by Gödel is to interpret □φ as meaning that φ is provable. Solovay proved a completeness theorem for

Speaker: Konstantinos Papafilippou

Title: Boolos' Analytical completeness

Date: Thursday, January 21, 2021

Time: 11:00 - 12:30 CET

Location: Online (instructions will come in a future email)

A compelling interpretation of modal logic suggested by Gödel is to interpret □φ as meaning that φ is provable. Solovay proved a completeness theorem for

Speaker: Fedor Pakhomov

Title: Iterated ω-model reflection and Π¹₂ proof-theoretic analysis

Date: Wednesday, April 15, 2020

Time: 17:00 - 18:30 CEST

Location: Online (instructions will come in a future email)

This is a joint work with James Walsh.

From works of Schmerl and Beklemishev it is known that transfinite iterations of reflection principles in first-order arithmetic provide a powerful tool for proof-theoretic analysis of fragments of second-order arithmetic. In this talk I'll present a study of certain reflection principles in the language of second-order arithmetic that gives a new method of proof-theoretic analysis of theories of meta-predicative strength range (ATR₀ and some moderately stronger systems of second-order arithmetic). We consider the principles of uniform Π¹ₙ reflection as well as uniform Π¹ₙ ω-model reflection and establish a number of connections between them. This allows us to calculate proof-theoretic ordinals of certain theories expressed in the terms of this reflection principles. An interesting feature of our approach is that in addition to calculation of Π¹₁, Π⁰₂, and Π⁰₁ proof-theoretic ordinals, we also find the well-ordering principles that correspond to the systems that we consider.

Speaker: Joost J. Joosten

Title: Down at the bottom of the bar with Robinson

Date: Wednesday, March 25, 2020

Time: 11:30 - 13:00

Location: Seminari de Filosofia

This will be a talk with many results but few proofs. We will revisit some results from the literature on weak systems of arithmetic that still are essentially undecidable. One of the few proofs given will be about the techniques developed by Solovay to shorten definable cuts as to obtain nice closure properties. In particular, we shall sketch how Robinson’s Arithmetic interprets Buss’ theory S

Speaker: Tommaso Moraschini

Title: Structural completeness in intermediate logics

Date: Wednesday, March 18, 2020

Time: 11:30 - 13:00

Location: Seminari de Filosofia

A rule is said to be

Speaker: Joost J. Joosten

Title: Assuring and critical labels for relations between maximal consistent sets for interpretability logics

Date: Wednesday, March 4, 2020

Time: 11:30 - 13:00

Location: Ramon Llull Seminar

This talk is about a technical aspect of interpretability logics. We will try to keep it accessible though to an audience with some general knowledge of modal logic. We will consider some issues of modal completeness proofs for interpretability logics. Normally, in modal logics we consider maximal consistent sets (MCS’s) of formulas to be worlds in a Kripke model and glue them together to a big model defining accessibility relations between the MCS’s. For interpretability logics it is not generally possible to define a large canonical model in one single go. This is due, in a sense, to the fact that a single MCS may be needed for different roles. Thus, completeness proofs needed a system to keep track of all those roles. A new technique collects all these roles in a single label. General theory reveals a charming structure so that we can conceive these labels as theories. So theories connect MCS’s. We shall see the general theory of these labels. Depending on how fast we can go we shall see some applications of them.

This is joint work with Evan Goris, Marta Bilkova and Luka Mikec. The corresponding paper can be found here.

Speaker: Luka Mikec

Title: Syntax, semantics and labellings for interpretability logic

Date: Friday, February 28, 2020

Time: 11:30 - 12:30

Location: Seminari de Filosofia

In this talk we are going to define basic modal ingredients for interpretability logics, such as types of maximal consistent sets, criticality and Veltman semantics. We will then focus on a more advanced concept, the full labels and their role in modal completeness proofs.

Supported by Croatian Science Foundation (HRZZ) under the project UIP-05-2017-9219.

Speaker: Michal Garlik

Title: Resolution Lower Bounds for Refutation Statements

Date: Wednesday, February 19, 2020

Time: 11:30 - 13:00

Location: Seminari de Filosofia

A refutation statement for a propositional proof system $P$, a CNF $F$, and an integer $s$ is a statement that $F$ has a $P$-refutation of length $s$. We discuss why resolution requires exponential size to refute resolution refutation statements for any unsatisfiable $F$ (and for any $s$ greater than a small polynomial in the size of $F$). We look at some consequences, e.g., we show an exponential lower bound on the size of resolution refutations of the negation of the reflection principle for resolution. These results are motivated by a proof complexity viewpoint on automated proof search in propositional logic, in particular by the question of automatability of proof systems.

Speaker: David Fernández-Duque

Title: Ekeland's variational principle in reverse mathematics

Date: Thursday, February 13, 2020

Time: 10:30 - 11:30

Location: Ramon Llull Seminar

Joint work with Paul Shafer and Keita Yokoyama.

Ekeland's variational principle states that every non-negative, lower semicontinuous function f on a complete metric space X has a "critical point", i.e. a point which behaves similar to a minimum of f. I will discuss how natural variations of the theorem (e.g. f is continuous, X is compact) lead to statements equivalent to three of the 'big five' theories of reverse mathematics.

Speaker: Mateusz Łełyk

Title: The Arithmetical Part of Global Reflection

Date: Friday, February 7, 2020

Time: 10:00 - 12:00

Location: 4085 (Lluís Vives Room)

In the lecture we characterize the arithmetical consequences of theextension of CT− with the Global Reflection Principle for PA and prove that they can be axiomatized by ω-many iterations of uniform reflection over PA. The conservativity part is originally due to Kotlarski Kotlarski [1986] (modulo the results in Smorynski [1977]). We present a model-theoretical proofbased on the notion of prolongable satisfaction classes. As a byproduct we give model-theoretical characterizations of theories of finite iterations of uniform reflection principle over PA. Finally, we show how, using this machinery, one can obtain a model-theoretical proof of Theorem 1 in Beklemishev and Pakhomov [2019]. In understanding the lecture, some knowledge about the development ofmodel theory in PA might be helpful. Kaye [1991] (Chapter 13.2), Enayatet al. [forthcoming] (Section 2.2) and Kossak and Schmerl [2006] (Chapter 1) contain good introductions. We will introduce all the relevant definitions, butmost probably will not have time for a very careful explanation.

See the booklet for the full abstract of this talk.

Speaker: Mateusz Łełyk

Title: Many Faces of Global Reflection

Date: Thursday, February 6, 2020

Time: 10:00 - 12:00

Location: 4085 (Lluís Vives Room)

During the lecture we approximate the Tarski Boundary from above. We study the principles for the truth predicate, which, over CT−, are equivalent to the Global Reflection Principle for PA. In particular we prove that, over CT− the following principles are equivalent to the Global Reflection Principle:

• ∆0-induction for the language with the truth predicate;

• the global reflection principle for pure logic

• “The set of true sentences is closed under provability in first-order logic”;

• “The set of true sentences is closed under provability in propositional logic”;

• the disjunctive correctness principle + “All induction axioms are true”.

These results are all summarized in [2017]. Time permitting, we shall outline an argument by Fedor Pakhomov (from [2019]) that the disjunctive correctness axiom implies the sentence “All axioms of induction are true”.

See the booklet for the full abstract of this talk.

Speaker: Cyril Cohen

Title: Generating Mathematical Structure Hierarchies Using Coq-ELPI

Date: Wednesday, January 29, 2020

Time: 11:30 - 13:00

Location: Hannah Arendt Seminar

In this talk we describe an ongoing work which purpose is to generate hierarchies of mathematical structures from annotated sets of axioms. The work is carried out on top of Coq using a plugin to meta-program using the lambda prolog interpreter ELPI. We provide a high level interface to instruct how to package together the appropriate axioms and we focus on how to make the use of such generated code robust to changes.

This is joint work with Kazuhiko Sakaguchi and Enrico Tassi.

Speaker: Mateusz Łełyk

Title: Conservativity of Compositional Truth

Date: Tuesday, February 4, 2020

Time: 10:00 - 12:00

Location: 4085 (Lluís Vives Room)

The aim of the lecture is to carefully present the model-theoretical proof of conservativity of the theory of compositional truth, CT−, over PA. Our presentation will follow the lines of Visser and Enayat [2015]. By modifying the proof, we draw some conclusions about the regularity properties for the predicate T, which, although unprovable in CT−, can be conservatively added to this theory. In particular we shall show that CT− extended with the sentence expressing

“All axioms of induction are true”.

is a conservative extension of PA. Time permitting, we shall study the limitations of the above result by considering various different axiomatizations of PA. In understanding the Enayat-Visser conservativity proof a basic knowledge about the structure of non-standard models of PA will be helpful. A good source for this is Kaye [1991] (Chapters 1, 2, 6 & 15).

See the booklet for the full abstract of this talk.

Speaker: Mateusz Łełyk

Title: Introduction to Axiomatic Theories of Truth

Date: Monday, February 3, 2020

Time: 10:00 - 12:00

Location: 4085 (Lluís Vives Room)

The idea of the lecture is to give a bird’s-eye view on the discipline. In the first part of the lecture we explain some motivations for studying the notion of truth axiomatically. We briefly revisit the classical work of Friedman and Sheard [1987] and Feferman [1991] and spend some time describing the use of a truth predicate in a recent approach to ordinal analysis by Beklemishev and Pakhomov [2019]. In the second part of the lecture we introduce basic types of axiomatizations for the truth predicate and define the canonical

• typed and disquotational theories: TB(−), UTB(−).

• typed and compositional theory: CT(−).

• untyped and compositional theories: FS and KF.

• untyped and disquotational theories: PTB, PUTB.

We summarize their properties, including the results on (ω-)consistency, arithmetical consequences and compatibility with reflection principles. The basic source for this lecture is the textbook by Halbach [2011].

See the booklet for the full abstract of this talk.

Speaker: Luka Mikec

Title: Syntax, semantics and labelings for interpretability logic

Date: Thursday, January 23, 2020

Time: 10:00 - 12:00

Location: Ramon Llull Seminar

In this talk we are going to define basic modal ingredients for interpretability logics, such as types of maximal consistent sets, criticality and Veltman semantics. We will then focus on a more advanced concept, the full labels and their role in modal completeness proofs.

Speaker: Joost J. Joosten

Title: Bounded induction expressed by reflection principles

Date: Wednesday, January 22, 2020

Time: 11:30 - 13:00

Location: Room 409

This seminar talk coincides with the last class of the master course Proof theory and automated theorem proving. The idea is to see a `real-life’ application of cut elimination outside the pure logical realm. Kreisel and Lévy proved that Peano Arithmetic is, provably in Primitive recursive arithmetic (PRA), equivalent to PRA together with uniform reflection over PRA. Leivant then obtained similar results for fragments of bounded arithmetic extending ISigma_2. Beklemishev further generalised the result by taking Elementary arithmetic as base theory as to also include ISigma_1. We shall present Beklemishev’s proof and mention some useful corollaries.

Speaker: Joost J. Joosten

Title: Pretending finiteness

Date: Tuesday, December 17, 2019

Time: 12:15 - 13:15

Location: Ramon Llull Seminar

In this talk we shall see how we can, under certain circumstances, do as if a possibly infinitely axiomatized theory had a finite axiomatization. This quasi-finite theory will, given the circumstances, be extensionally the same as the original theory, but this equality is in general not provable. This trick is inspired by Feferman’s provability predicate that proves it’s own consistency. The trick that we present is due to Albert Visser and allows us to collapse the Sigma-three notion of interpretability to a Sigma-one one. As such we open the way to proving a myriad of new principles to be arithmetically sound. This method is an alternative to the method of definable cuts in the field of interpretability logics.

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

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

Title: Refinements for free! and applications

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 Π

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 Π

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

Speaker: Ana Borges

Title: Gödel's

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

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

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, ACA

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 Π

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

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

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 ε

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 ∏

Speaker: Joost J. Joosten

Abstract

In this session we look at one-sided Tait calculus for pseudo ∏

Location: Logic Seminar Room

Date: Wednesday, March 13, 2013

Time: 12:15-14:00

title: Truth complexity for ∏

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 ∏

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 [α]

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: Π

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

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 Π

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

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 ℵ

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.