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.
Speaker: Eric Sancho Adamson
Title: Kant's philosophy of mathematics, contextualized
Date: Wednesday, April 21, 2021
Time: 17:00 - 18:00 CEST
Location: Online
This talk is not on logic or mathematics, but about philosophy of mathematics. Accordingly, the topic to be discussed does not concern explaining or furthering mathematical or logical results, but rather grounding mathematical principles in mathematical cognition. In order to reflect upon mathematical cognition, most contemporary philosophers of mathematics either agree with Immanuel Kant's (1724-1804) philosophy of mathematics or react against it, and in both cases his original concepts are still widely used. In other words, for attaining a thorough understanding of philosophy of mathematics Kant must be reckoned with. My main aim of the talk is to provide a contextualized exposition of Immanuel Kant's philosophy of mathematics and an evaluation of its historical relevance, without assuming that the audience holds any preexisting knowledge about philosophy of mathematics or history of philosophy. We will first talk about the importance of mathematics in modern philosophy as setting a paradigm for a widely sought demonstrative method of reasoning which would be capable of achieving absolute certainty in any intelligible topic. This doctrine is known as rationalism and was held by some of Kant’s predecessors, such as Descartes, Leibniz, Christian Wolff. Kant’s own philosophy of mathematics springs from and is instrumental to his critique of the “dogmatic” aspects of the metaphysical systems proposed by his rationalist predecessors, such as, according to Kant, illegitimately deriving existence predicates. We will dwell upon Kant's Inquiry Concerning the Distinctness of the Principles of Natural Theology and Morality (1764) and the Critique of Pure Reason (1781/1787) in order to explain his most significant ideas, such as the synthetic/analytic and a priori/a posteriori distinctions, as well as the role of intuition and construction in mathematics and the so-called "mathematical antinomies". If time allows, we will then briefly talk about the remarkable influence of Kant’s philosophy of mathematics on posterior mathematicians and logicians, which include "giants" such as Bolzano, Gauss, Riemann, Dedekind, Frege, Brouwer or Hintikka. If time allows even more, a short assessment of what is and what isn't considered to still be relevant today about Kant's proposal will also be provided.
Speaker: Joaquim Casals Buñuel
Title: Showing superpolynomial lower bounds for NEXP via circuit-sat
Date: Wednesday, April 7, 2021
Time: 17:00 - 18:00 CEST
Location: Online
In the 80's there were numerous results showing circuit lower bounds for various classes of circuits. In particular, Kannan showed superpolynomial lower bounds for NEXPNP.
Unfortunately advances on this front halted until a few years ago when Ryan Williams was able to give conditional superpolynomial lower bounds for NEXP.
In this seminar we will give an overview of the technique used by Williams to prove that NEXP cannot have polynomial size circuits provided that CIRCUIT-SAT can be
solved efficiently. Here is a link to Quim's master thesis and here are slides of the presenation.
Speaker: Oriola Gjetaj
Title: Application of fast-growing functions to the study of Ramsey-type combinatorial principles
Date: Wednesday, March 24, 2021
Time: 17:00 - 18:00 CET
Location: Online
After the publication of Gödel’s incompleteness theorems in the 30s, mathematicians tried to find an example of a true theorem that could not be proven inside some reasonably strong axiomatic system for number theory.
In the 70s Paris and Harrington proved the unprovability of a slight variant of the Finite Ramsey’s theorem in PA. The original proof uses model theory, but instead we will look into Loebl & Nešetril's paper An unprovable Ramsey-type theorem. In this paper the authors give a concise combinatorial proof of this result using transfinite ordinals and the characterization of the provably total functions of arithmetic.
Here are slides.
Speaker: Esperanza Buitrago
Title: Completeness theorem for IL, Part II
Date: Wednesday, March 10, 2021
Time: 17:00 - 18:00 CET
Location: Online
We will explore the techniques that Frank Veltman and Dick De Jongh used in their paper Probability logics for relative interpretability back in 1990.
Here are slides.
Speaker: Esperanza Buitrago
Title: Completeness theorem for IL
Date: Wednesday, March 3, 2021
Time: 17:00 - 18:00 CET
Location: Online
We will explore the techniques that Frank Veltman and Dick De Jongh used in their paper Probability logics for relative interpretability back in 1990.
Speaker: Ana de Almeida Borges
Title: The Quantified Reflection Calculus with one modality: Part II
Date: Wednesday, February 17, 2021
Time: 17:00 - 18:00 CET
Location: Online
Quantified provability logic is known to be impossible to recursively axiomatize for consistent theories containing a minimum of arithmetic.
However, the proof of this fact cannot be performed in a strictly positive signature.
We define a (decidable) strictly positive logic called QRC1 and conjecture that it is a provability logic, i.e.,
that there is a Solovay-like completeness theorem relating QRC1 to an arithmetical theory such as Peano Arithmetic.
In the second part of this series we delve into Kripke models for QRC1, going through the soundness and completeness proofs for the modal semantics.
This is joint work with Joost J. Joosten.
Speaker: Ana de Almeida Borges
Title: The Quantified Reflection Calculus with one modality: Part I
Date: Wednesday, February 10, 2021
Time: 17:00 - 18:00 CET
Location: Online
Quantified provability logic is known to be impossible to recursively axiomatize for consistent theories containing a minimum of arithmetic.
However, the proof of this fact cannot be performed in a strictly positive signature.
We define a (decidable) strictly positive logic called QRC1 and conjecture that it is a provability logic, i.e.,
that there is a Solovay-like completeness theorem relating QRC1 to an arithmetical theory such as Peano Arithmetic.
In the first part of the series we expose the context and motivation for defining QRC1, and give an overview of the steps needed to achieve a Solovay-like completeness proof.
This is joint work with Joost J. Joosten.
Speaker: Alfonso Alfaro
Title: Baumgartner's set theoretical proof of Hindman's theorem Part III
Date: Tuesday, January 26, 2020
Time: 17:00 - 18:30
Location: Online
Baumgartner's set theoretical proof of Hindman's theorem.
Speaker: Alfonso Alfaro
Title: Baumgartner's set theoretical proof of Hindman's theorem, Part II
Date: Thursday, December 17, 2020
Time: 15:00 - 16:30
Location: Online
Baumgartner's set theoretical proof of Hindman's theorem.
Speaker: Alfonso Alfaro
Title: Baumgartner's set theoretical proof of Hindman's theorem
Date: Thursday, December 10, 2020
Time: 15:00 - 16:30
Location: Online
Baumgartner's set theoretical proof of Hindman's theorem.
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.