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

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.

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

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic.

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

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic.

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 Π

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic.

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

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic.

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.

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

Beklemishev, L. D. (2005). Reflection principles and provability algebras in formal arithmetic.

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.

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.

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 ε

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 ε

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