PhD Seminar on Mathematical Logic

Organization

In principle, we meet on a bi-weekly basis. The meetings will be at the Logic Seminar Room at the fourth floor of the Philosophy department at Carrer Montalegre 6 or in Joost's office on the fourth floor. The idea is that in the sessions we read important literature and the presentations will be given mainly by and for PhD students and/or advanced Master students. Since the students alternately present in the seminar, the seminar is sometimes colloquially referred to as the Seminario Alterne.

David Fernández Duque 25-09-2019
David Fernández Duque 27-05-2019
David Fernández Duque 07-03-2019
Cyril Cohen 21-02-2019
Mireia González Bedmar 12-12-2018
Mireia González Bedmar 11-12-2018
Fabian Romero Jimenez 20-06-2018
Nika Pona 14-11-2017
Nika Pona 19-09-2017
Ana Borges 21-06-2017
Ana Borges 15-06-2017
Nika Pona 07-06-2017
Nika Pona 22-05-2017
Nika Pona 17-05-2017
Nika Pona 27-04-2017
Ana Borges 30-03-2017
Ana Borges 23-03-2017
Eduardo Hermo Reyes 30-11-2016
Tuomas Hakoniemi 23-11-2016
Pilar Garcia de la Parra 05-05-2016
Eduardo Hermo Reyes 07-04-2016
Eduardo Hermo Reyes 11-02-2016
David Fernández Duque  01-12-2015
Eduardo Hermo Reyes  30-11-2015
David Fernández Duque  26-11-2015
Eduardo Hermo Reyes 20-03-2014
Laia Jornet Somoza 19-03-2014





Speaker: David Fernández Duque
Title: NL Decidability of the Rest Compensation Article 8.6
Date: Wednesday, May 27, 2019
Time: 11:45 - 13:00
Location: Ramon Llull


Abstract: We show that the problem of determining whether a given driving record is legal is in NL, the class of nondeterministic logspace problems. Since NL is contained in P we obtain polytime decidability of compliance of a driving record with Article 8.6.




Speaker: David Fernández Duque
Title: On the adequacy of temporal logics for modelling European transport regulations
Date: Monday, May 27, 2019
Time: 10:30 - 12:00
Location: Ramon Llull


Abstract: We analyze the expressibility of some articles of the European transport regulations in subsystems of monadic second order logic (MSO), with particular emphasis on linear temporal logic (LTL). We argue that all articles under consideration can be represented in the \Sigma_1 fragment of MSO, although representations in LTL can sometimes be unfeasible if not impossible.




Speaker: David Fernández Duque
Title: Decidable frameworks for modelling traffic legislation
Date: Thursday, March 7, 2019
Time: 10:00 - 11:30
Location: Logic Seminar


We present some well-understood logical frameworks which could potentially be used for representing and automated reasoning about traffic legislation. We will argue that most, if not all, of current law can be modelled within frameworks known to be decidable, and present some speculations about possible tractable alternatives.




Speaker: Cyril Cohen
Title: Refinements for free! and applications
Date: Thursday, February 21, 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.



Speaker: Mireia González Bedmar
Title: Category theory, lambda calculus and functional programming, Part II
Date: Wednesday, December 12, 2018
Time: 11:15-12:45
Location: Ramon Llull Room/Logic Seminar Room


Abstract:
This is a continuation of Part I.




Speaker: Mireia González Bedmar
Title: Category theory, lambda calculus and functional programming, Part I
Date: Tuesday, December 11, 2018
Time: 11:15-12:45
Location: Ramon Llull Room/Logic Seminar Room


Abstract:
Since its birth in the early 1940s, category theory has proved to be a powerful framework capable of unifying apparently distant mathematical theories. Many modern mathematical disciplines would be inconceivable without categories, but even those theories which were largely developed on their own have benefited from the new categorical perspective. One of these theories is typed lambda calculus, which corresponds to a certain kind of categories called cartesian-closed. This fact has been known as the Curry-Howard-Lambek correspondence since Joachim Lambek described it in the 1970s. In this talk we will present (some of) the basic concepts of category theory and how it interacts with typed lambda calculus. We will also see how categorical notions such as functor and monad are considered and implemented in functional programming languages.




Speaker: Fabian Romero Jimenez
Title: Kripke completeness of strictly positive modal logics over meet-semilattices with operators
Date: Wednesday, June 20, 2018
Time: 17:00-19:00
Location: Ramon Llull Room/Logic Seminar Room


Abstract:
Our concern is the completeness problem for strongly positive (SP) theories, that is, sets of implications between SP-terms built from propositional variables, conjunction and modal diamond operators. Originated in logic, algebra and computer science, SP-theories have two natural semantics: meet-semilattices with monotone operators providing Birkhoff-style calculi, and first-order relational structures (aka Kripke frames) often used as the intended structures in applications.




Location: Logic Seminar Room
Date: Tuesday, November 14, 2017
Time: 11:00-12:30
Title: Induction and reflection rules
Speaker: Nika Pona


Abstract:
We continue with the section 4 of Beklemishev's paper, in which the relationship between induction and reflection principles is established. Previously we saw that partial induction schema with parameters IΣn is equivalent to partial uniform reflection schema RFNΣn + 1(EA), or (n+1)-Con(EA). Now the goal is to similarly characterize partial induction rules. We will focus our attention on section 4.3 where the equivalence between partial reflection rules and induction rules is proved. From this result one can conclude that, in contrast to IΠn, the closure of EA under the Πn induction rule (IΠnR) is not finitely axiomatizable.




Location: Logic Seminar Room
Date: Tuesday, September 19, 2014
Time: 12:15-13:30
Title: Induction with parameters and reflection
Speaker: Nika Pona


Abstract:
We will discuss sections 4.1 and 4.2 of Beklemishev's paper Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys. First, we define Tait's sequent calculus and then prove the equivalence of EA + RFNΣn + 1(EA) and IΣn over EA+ using cut-elimination theorem for predicate calculus.




Speaker: Ana Borges
Title: Provably total computable functions and 1-consistency
Date: Wednesday, June 21, 2017
Time: 13:00-14:30
Location: Logic Seminar


Abstract: We discuss different ways to enumerate the provably total computable functions in a theory T. Using universal funcions for these enumerations, we show that the totality of the iteration of a function is equivalent to the 1-consistency of the totality of said function, over EA. A nice corolary is that EA+ is the same as EA together with RFNΠ2(EA).

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197 pp. 31-34.



Speaker: Ana Borges
Title: Provably total computable functions and fragments of PA
Date: Thursday, June 15, 2017
Time: 11:00-12:30
Location: Logic Seminar


Abstract: We introduce provably total computable functions in a theory T, ℱ(T), and provide a characterization of ℱ(T) as the closure by composition of the elementary functions together with a function representing the axioms of theory T. We also discuss some fragments of PA.

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197, pp. 27-31.



Speaker: Nika Pona
Title: Hierarchy of partial local reflection principles
Date: Wednesday, June 7, 2017
Time: 10:30-12:00
Location: Logic Seminar


Abstract: In contrast to partial uniform reflection, partial local reflection principles are not finitely axiomatizable and prove the same Π1-sentences. These results are applications of provability logic techniques.

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197, pp.22-27.



Speaker: Nika Pona
Title: Hierarchy of partial uniform reflection principles
Date: Wednesday, May 22, 2017
Time: 10:30-12:00
Location: Logic Seminar


Abstract: We started talking about hierarchies of partial reflection principles. In particular we proved that RFNΠn+1(T) is stronger than RFNΠn(T), since T + RFNΠn+1(T) ⊦ Con(T + RFNΠn(T) ), which means that none of the extensions at any level of the hierarchy is conservative even for Π1-sentences.

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197, pp.21-22.



Speaker: Nika Pona
Title: Unboundedness theorem for partial reflection principles
Date: Wednesday, May 17, 2017
Time: 10:30-12:00
Location: Logic Seminar


Abstract: We talked about the so-called unboundedness theorems that state that partial uniform (local) reflection principles for T are not contained in any consistent (recursively enumerable) extension of T. This allows to show that uniform reflection is strictly stronger than local reflection.

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197, pp.18-21.



Speaker: Nika Pona
Title: Reflection principles
Date: Thursday, April 27, 2017
Time: 11:00-14:00
Location: Logic Seminar


Abstract: We introduced explicit, local Rfn(T) and uniform reflection principles RFN(T), as well as partial reflection principles RFNΣn(T) and RFNΠn(T). We proved that uniform reflection is equivalent to Kleene's rule and that partial reflection principles are finitely axiomatizable. We also saw that RFNΣn(T)≡ RFNΠn+1(T) and RFNΠ1(T) ≡ Con(T).

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197, pp.13-18.



Speaker: Ana Borges
Title: Gödel's theorems and provability logic
Date: Thursday, March 30, 2017
Time: 12:30-14:00
Location: Logic Seminar


Abstract: We discuss Gödel's theorems, as well as a generalisation by Rosser. We follow with provaility logic and the statement of Solovay's theorem.

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197.



Speaker: Ana Borges
Title: Elementary Arithmetic and the provability predicate
Date: Thursday, March 23, 2017
Time: 12:30-14:00
Location: Logic Seminar


Abstract: We present Elementary Arithmetic, as well as several extentions. We follow with the provability predicate and Löb's conditions.

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic. Russian Mathematical Surveys, 60(2), 197.



Speaker: Eduardo Hermo Reyes
Title: Big Schmerl and small Schmerl (TBC)
Date: Wednesday, November 30, 2016
Time: 12:30-14:00 (TBC)
Location: Logic Seminar


Abstract: We will study the Schmerl fine structure principle that relates different notions of Turing progressions and its relation with the Reduction Property which relates reflection axioms to reflection rules. We will also deal with a more general principle (big Schmerl) and see how it can be derived from the small one within our calculus for Turing progressions TSC (Turing Schmerl Calculus).



Speaker: Tuomas Hakoniemi
Title: Reduction property for GLP-algebras
Date: Wednesday, November 23, 2016
Time: 11:05-12:05
Location: Logic Seminar


Abstract: We discuss Beklemishev's proof that any free GLP-algebra satisfies a certain generalization of the reduction property of reflection algebras.



Speaker: Pilar Garcia de la Parra
Title: There's alway a Worm.
Date: Thursday, May 5, 2016
Time: 17:30-19:00
Location: Aula 412


Abstract: We explore the proof presented by Beklemishev in "Veblen Hierarchy in the context of provability algebras" that states that "for every two worms A,B in W_x, there is a worm C such that C is equivalent to A /\ B."



Speaker: Eduardo Hermo Reyes
Title: A practical introduction to the Coq proof assistant, Part 2
Date: Thursday, April 7, 2016
Time: 16:00-18:00
Location: History Seminar Room (4029)


Abstract: Continuing the functional programming approach to Coq, we will introduce the List library and Record constructions. We will also explore how to deal with loops and "partial" recursive functions. The History Seminar Room (4029) is at the same location as the Logic Seminar Room but then one hallway earlier.



Speaker: Eduardo Hermo Reyes
Title: A practical introduction to the Coq proof assistant, Part 1
Date: Thursday, February 11, 2016
Time: 11:00-12:30
Location: Logic Seminar Room


Abstract: Coq is an interactive theorem prover that provides a formal language to express mathematical definitions and theorems, together with an environment to develop machine-checked proofs. Coq can also be seen as implementing a dependently typed functional programming language. In this session we will present some basic elements of Coq's functional programming language and some basic tactics that can be used to prove simple properties of Coq programs. In particular, we will use Coq to prove some metatheorems about classical propositional calculus.

Here is a handout written by Eduardo. This should be loaded in some Coq-environment.

Speaker: David Fernández Duque
Title: Ordinal notations and provability algebras, Part 2
Date: Tuesday, December 1, 2015
Time: 19:15-20:30
Location: Logic Seminar Room


Abstract: An ordinal analysis of a formal theory T typically requires at least two ingredients: a suitable representation of T, and an ordinal notation system. Beklemishev's approach using provability algebras fuses both by representing ordinals up to ε0 as formulas in the language of Peano arithmetic. In this tutorial-style talk, we will present both traditional notation systems and others based on provability algebras up to the Howard-Bachmann ordinal, related to impredicative mathematics.



Speaker: Eduardo Hermo Reyes
Title: Semantics for Turing Schmerl Calculus
Date: Monday, November 30, 2015
Time: 12:00-14:00
Location: Logic Seminar Room


Abstract: We present a logic that denotes Turing progression corresponding to different notions of consistency and dwell on both arithmetical and modal semantics.



Speaker: David Fernández Duque
Title: Ordinal notations and provability algebras
Date: Thursday, November 26, 2015
Time: 19:15-20:30
Location: Logic Seminar Room


Abstract: An ordinal analysis of a formal theory T typically requires at least two ingredients: a suitable representation of T, and an ordinal notation system. Beklemishev's approach using provability algebras fuses both by representing ordinals up to ε0 as formulas in the language of Peano arithmetic. In this tutorial-style talk, we will present both traditional notation systems and others based on provability algebras up to the Howard-Bachmann ordinal, related to impredicative mathematics.



Location: Logic Seminar Room
Date: Thursday, March 20, 2014
Time: 12:15-14:00
Title: Collection, Conservativity and formalizations of conservativity
Speaker: Eduardo Hermo Reyes


Abstract: The collection axioms allow us to show that the arithmetical classes \Sigma_n, \Pi_n and \Delta_n are closed under bounded quantification. Also, it has been showed by Parsons, that they are useful for defining hierarchies of fragments of arithmetic. Following the work done by Beklemishev, we give a proof-theoretic approach to collection principles and show some conservativity results.





Location: Logic Seminar Room
Date: Wednesday, March 19, 2014
Time: 10:15-12:00
Title: Encoding Syntax in Primitive Recursive Arithmetic
Speaker: Laia Jornet Somoza


Abstract:
We will deal with Chapter 1 of Smoryński's book Self Reference and Modal Logic.