Seminari Cuc, Seminar on Proof Theory and Foundations of Mathematics
Organization
In principle, we meet on a bi-weekly basis on Wednesday from 12:15 -- 14:00 at the Ramon Llull Seminar Room (Room 4047, formerly called the Logic Seminar Room) at the fourth floor of the Philosophy department at Carrer Montalegre 6.
This seminar was formerly called Seminari Cuc, Seminar on Proof Theory and Modal Logic. Related presentations of a more informal nature are allocated at the PhD Seminar on Mathematical Logic informally referred to as the Seminari Alterne.
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 Σ01 propositions (i.e.
existential quantification over a decidable predicate on N) are stable under
double negation. However, there are various non-equivalent definitions of
decidable predicates and thus Σ01 in constructive
foundations, leading to non-equivalent Markov’s principles. This fact is often
overlooked and leads to confusion: at the time of writing, both Wikipedia and
nlab claim propositions to be equivalent to MP that are however only
respectively equivalent to two non-equivalent forms of MP.
We give three variants of MP in constructive type theory, along with respective
equivalence proofs to different formulations of Post’s theorem
(“Σ01 -predicates with complement in
Σ01 are decidable”), stability of termination of
computations, the statement that an extended natural number is finite if it is
not infinite, and to completeness of natural deduction w.r.t. Tarski semantics
over the (∀, →, ⊥)-fragment of classical first-order logic for
Σ01-theories. The first definition (MP_Prop) uses a
purely logical definition of Σ01 for predicates N → Prop,
while the second one (MP_bool) relies on type-theoretic functions N → B, and
the third one (MP_PR) on a model of computation.
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 Π11-CA0
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 Π11-CA0
that uses the interplay of the methods of functorial proof theory and iterated reflection.
An interesting feature of the approach is that it completely sidesteps predicative cut elimination.
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 Δ0 truth
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 Δ0 formula φ(x) and a natural number n in unary, whether φ(n) is true. We are interested in instances of the problem where n is much bigger than φ. More precisely, we consider the parameterized problem with parameter |φ|. We show unconditionally that this problem does not belong to the parameterized version of AC0. We also show that certain natural upper bounds on the parameterized complexity of the problem imply separations of classical complexity classes. These results are obtained by an analysis of a parameterized halting problem. A related problem concerns the provability of the MRDP theorem in bounded arithmetic.
Speaker: Ana de Almeida Borges
Title: QRC1 through the formalization lens
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
QRC1, is a strictly positive quantified modal logic inspired by the
unimodal fragment of the Reflection Calculus, RC1. The language
consists of a verum constant and relation symbols as atomic formulas,
with the only available connectives being the conjunction, the diamond, and the
universal quantifier.
QRC1 was born out of the wish for a nice quantified provability
logic for theories of arithmetic such as PA, even though Vardanyan showed that
this is in general impossible. However, restricting the language to the
strictly positive fragment is a viable solution.
Showing that QRC1 is indeed a provability logic (i.e., that it is
arithmetically complete) relies on the existence of Kripke models refuting
given unprovable statements, and as such it is fundamental to prove Kripke
soundness and completeness theorems. The proofs of these theorems are
reasonably elementary and predictable, with the notable exception of the
Lindenbaum-like lemma, which needs a work-around due to the absence of
implications in the language.
In this talk I will share my progress on formalizing the Kripke
soundness and completeness theorems for QRC1 in Coq, focusing
on the challenges encountered. My main goal is to give an example of what the
process of formalizing something in Coq entails, and what the final product
looks like.
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 Π02-complete, and in particular 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 show that it is a provability logic: there is a Solovay-like completeness theorem relating QRC1 to Peano Arithmetic. Then by the Π02 conservativity of PA over HA, we conclude that QRC1 is also the provability logic of Heyting Arithmetic.
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 GL taken under this interpretation. Later Japaridze expanded the language by adding modalities [n] for every n < ω. A corresponding Solovay theorem has been proven for various interpretations of the [n] modalities, however there are some obstacles to overcome while in Japaridze's GLP theory of modal logic. In these two sessions we will take a look at GLP with only two modalities, interpreted as provable and ω-provable in the theory of Analysis of second order arithmetic, respectively. We will follow the paper by G. Boolos to showcase: what differs when moving from GL to GLP; considerations needed in regards to Analysis; and a somewhat different way of defining the Solovay formulas.
Here are slides of the presentation.
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 GL taken under this interpretation. Later Japaridze expanded the language by adding modalities [n] for every n < ω. A corresponding Solovay theorem has been proven for various interpretations of the [n] modalities, however there are some obstacles to overcome while in Japaridze's GLP theory of modal logic. In these two sessions we will take a look at GLP with only two modalities, interpreted as provable and ω-provable in the theory of Analysis of second order arithmetic, respectively. We will follow the paper by G. Boolos to showcase: what differs when moving from GL to GLP; considerations needed in regards to Analysis; and a somewhat different way of defining the Solovay formulas.
Here are slides of the presentation.
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 S12.
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 admissible in a deductive system when its addition to the system does not enlarge the set of tautologies. Furthermore, it is said to be derviable when it belongs to the consequence relation naturally associated with the system. Deductive system whose admissible rules are derivable have been called structurally complete. In this talk we will review some results in the theory of admissible rules, including the well-known Prucnal's trick. If time allows, we will sketch a new duality theoretic proof of Citkin's 1978 description of hereditarily structurally complete intermediate logics, developed in collaboration with N. Bezhanishvili.
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 True of arithmetic such that for every formula φ of arithmetic, True(φ) ↔ φ holds.
We talk about the idea behind the proof of this statement, and give some preliminary notions and results towards a full proof. This talk is based on Chapter 17 of Boolos' The Logic of Provability.
Speaker: Joost J. Joosten
Title: The Logic Road to Software Homologation.
Date: Wednesday, April 24, 2019
Time: 15:00 - 16:30
Location: Salon de grados, Facultad de derecho, UB
This talk was given in the context of the Second UB International PhD in Law Conference.
Software always contains mistakes. Most of them are small and innocuous since they passed expert scrutiny and dynamic testing. However, the mistakes are there and from time to time they can have disastrous consequences: exploding rockets, planes or erroneous legal verdicts. These days we are getting increasingly dependent on algorithmic legal processes. But how are we to trust them knowing that software always contains errors. In the face of this, what is the value of a DNA sequencing run, the reading of a tachograph, the measurement and interpretation of a speeding device? In this talk with we will see how proof assistants can help to significantly reduce operational risk. As such, software will be proven to comply the specification. Of course humans can still err in claiming that the formal specification faithfully describes a situation. But, in our solution, at least the errors in the software are reduced to zero.
Slides of this talk can be found here.
Speaker: Tuomas Hakoniemi
Title: Lower bounds on size of Sums-of-Squares refutations.
Date: Monday, March 18, 2019
Time: 10:30 - 12:00
Location: Logic Seminar/Ramon Llull
We discuss a size-degree trade-off for Sums-of-Squares proofs and show how to obtain strong lower bounds on the monomial size of refutations from the trade-off and the existing degree lower bounds. This talk is based on joint work with Albert Atserias. Here is the paper.
Speaker: David Fernández Duque
Title: Intuitionistic linear temporal logics.
Date: Thursday, March 14, 2019
Time: 10:15 - 11:45
Location: Maria Zambrano Seminar
Dynamical topological systems are pairs (X,S) where X is a topological space and S: X->X is continuous. These systems provide a natural semantics for the language of linear temporal logic by interpreting temporal modalities using the function S and interpreting implication according to the topological semantics for intuitionistic logic, giving rise to a family of natural intuitionistic temporal logics. In this talk we will give an overview of known results regarding such logics, including decidability and completeness theorems, and state some open problems.
This is joint work with Joseph Boudou and Martín Diéguez.
Speaker: Joost J. Joosten
Title: Provable completeness for Münchhausen provability, reflection, induction and collection.
Date: Monday, February 25, 2019
Time: 10:30 - 11:30
Location: Logic Seminar/Ramon Llull
In this talk we focus on provable completeness for our provability predicates and study the formula classes for which we have provable completeness. Using a Rosser-style fixpoint, we can show that sometimes we can import universal quantifiers from outside the box to inside the box. However, if all the technical machinery works depends on the amount of collection available which in turn can be related to reflection and induction.
The provable completeness results shall be key in proving that the [a] modality is, in a sense Sigma_{1+a}^0-definable.
Speaker: Joost J. Joosten
Title: Completeness for our Barony
Date: Monday, February 18, 2019
Time: 10:30 - 11:30
Location: Logic Seminar/Ramon Llull
In previous sessions we have spoken mainly on soundness for Münchhausen provability. In this talk we fix on various completeness phenomena for Münchhausen provability.
In this talk we shall see how arithmetical completeness can be easily obtained under some fairly general conditions. We revisit Solovay's completeness proof and comment on the changes to adopt to our setting.
Speaker: Amanda Vidal
Title: On non RE logics: some well-known cases and some new ones
Date: Wednesday, February 13, 2019
Time: 12:30 - 14:00
Location: Logic Seminar/Ramon Llull
In this talk we will do an overview of some non Recursively Enumerable logics, and then move to modal many-valued logics, where we can exhibit several new examples of non RE logics arising from a very natural semantical definition. Computability results for this logics naturally play a crucial role in proving so.
Slides of this talk can be found here.
Speaker: Cyril Cohen
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 Π1-consequences as the (ε0 + ε0)-th smooth Turing jump of EA+ by using our knowledge about the amount of "jumps" necessary to go from EA+ to an intermediate theory T and from T to PA + Con(PA). We shall see how Schmerl's Thoerem provides an alternative and easier proof of this fact and we will see some generalizations.
Speaker: Ana Borges
Title: Smooth Turing progressions
Date: Wednesday, May 23, 2018
Time: 12:30-14:00
Location: Logic Seminar
Abstract: We will show that PA + Con(PA) has the same Π1-consequences as the (ε0 + ε0)-th smooth Turing jump of EA+ by using our knowledge about the amount of "jumps" necessary to go from EA+ to an intermediate theory T and from T to PA + Con(PA).
Speaker: Daniel Ribeiro Sousa
Title: Formal epistemology: a primer and a surprising application
Date: Wednesday, May 16, 2018
Time: 12:15-13:15
Location: Logic Seminar
Abstract: We will see how to formalise the idea of "scientific
knowledge" through an infinite game between a scientist and the devil.
This means talking about what it means for an hypothesis to be decidable
with a deadline, with certainty, in the limit and gradually. We will
then apply this knowledge to talk about Regulation (EC) No 561/2006. If
time permits, we will see the connections between the concepts
introduced earlier with the Borel hierarchy.
Speaker: Fabian Romero
Title: Topological semantics for intuituionistic logic
Date: Wednesday, May 09, 2018
Time: 12:15-14:00
Location: Logic Seminar
Abstract: Intuitionistic logic is a natural framework to model several dynamic semantics. In this talk we will see a couple of topological interpretations: the classic one, and an alternative interpretation for the 'henceforth' modality which validates the Fisher Servi Axioms.
Speaker: Joost J. Joosten
Title: On conjunctions of bounded hyper arithmetical complexity but arbitrary length
Date: Wednesday, April 25, 2018
Time: 12:30-13:45
Location: Logic Seminar
Abstract: This talk is a continuation of previous week and as considers some aspects of the Turing Jump Interpretation (also called Münchhausen provability) of transfinite polymodal provability logic. Last week we saw how a straight-forward soundness proof does not allow for the separation of meta from object theory. If we had an artifact to express arbitrary long conjunctions of formulas of some (transfinitely) bounded complexity, then we can prove soundness with the object theory different from the meta-theory. However, the canonical way of writing such arbitrary long conjunctions makes use of a generalization of the Friedman-Goldfarb-Harrington theorem and as such requires quite heavy artillery from the object theory. We see how partial truth predicates can play an important role here.
Speaker: Joost J. Joosten
Title: Separating object-theory from meta-theory for Münchhausen provability
Date: Wednesday, April 18, 2018
Time: 12:15-13:45
Location: Logic Seminar
Abstract: This talk considers some aspects of the Turing Jump Interpretation (also called Münchhausen provability) of transfinite polymodal provability logic. In particular, we revisit how a straight-forward soundness proof does not allow for the separation of meta from object theory. If we had an artifact to express arbitrary long conjunctions of formulas of some (transfinitely) bounded complexity, then we can prove soundness with the object theory different from the meta-theory. However, the canonical way of writing such arbitrary long conjunctions makes use of a generalization of the Friedman-Goldfarb-Harrington theorem and as such requires quite heavy artillery from the object theory. We see how partial truth predicates can play an important role here.
Speaker: Joost J. Joosten
Title: On universal models of WC and RC
Date: Wednesday, March 14, 2018
Time: 12:15-13:45
Location: Logic Seminar
Abstract: We write RC for the reflection calculus and WC for the worm calculus. Both RC and WC are known to have the finite model property. We prove however that any universal model U of them is in essence infinite and inherits some complexity from Ignatiev's universal model I for the closed fragment of GLP. In particular, we show that for each point x on the main axis of I, there is a point y in U so that x and y have the same modal theory. However, in some sense, simplifications can be present. For example, we can restrict the order types of the accessibility relations to omega. This is joint work with Ana de Almeida Borges.
Speaker: Eduardo Hermo Reyes
Title: Relational semantics for TSC, Part III
Date: Wednesday, March 7, 2018
Time: 12:15-13:30
Location: Logic Seminar
Abstract: This talk is a continuation of previous week. As such, we study relational semantics for the system TSC_omega^\Lambda by considering a small variation on Ignatiev's frame. This is joint work with Joost J. Joosten.
Speaker: Eduardo Hermo Reyes
Title: Relational semantics for TSC, Part II
Date: Wednesday, February 21, 2018
Time: 12:15-13:30
Location: Logic Seminar
Abstract: This talk is a continuation of previous week. As such, we introduce relational semantics for the system TSC_omega^\Lambda by considering a small variation on Ignatiev's frame. This is joint work with Joost J. Joosten.
Speaker: Eduardo Hermo Reyes
Title: Relational semantics for TSC
Date: Wednesday, February 14, 2018
Time: 12:15-13:30
Location: Logic Seminar
Abstract: We introduce relational semantics for the system TSC_omega^\Lambda by considering a small variation on Ignatiev's frame. This is joint work with Joost J. Joosten.
Speaker: Joost J. Joosten
Title: Formalized conjunctions of arbitrary length
Date: Wednesday, February 07, 2018
Time: 12:15-13:30
Location: Logic Seminar
Abstract: In this session, we revisit the soundness proof of transfinite provability logic under the Turing jump interpretation. In the previous talks we saw how formalized reflexive transfinite induction helped us prove the arithmetical soundness of GLP_Lambda. In this talk, we finish this proof and observe that the proof disallows us to make a difference between the object and the meta theory which is undesirable. Thus, we will present an alternative proof by formalizing conjunctions of arbitrary length. In principle this requires much arithmetic but we will see that for our purposes we will only need to consider conjunctions of arbitrary length for formulas that shall be seen can be bound by some complexity measure. These bounds will take care that under some mild assumptions --that are needed anyway for the soundness proof-- we can mimic conjunctions of arbitrary length. This allows for a soundness proof where object and meta theory can be chosen differently.
Speaker: Joost J. Joosten
Title: Induction: internal, external, transfinite, reflexive, formalized and combinations thereof
Date: Wednesday, January 31, 2018
Time: 12:15-13:30
Location: Logic Seminar
Abstract: This session is a continuation of our session of two weeks ago. A such, we study a recursive equation for what we coined the Turing jump interpretation of transfinite polymodal provability logic. A theory that can express and prove this recursion up to some ordinal Lambda is called a GLP_Lambda amenable theory (GAT). We will show that for GATs, we can obtain soundness of the GLP axioms without many further assumptions on the base theory. However, we will need a form of transfinite induction since external transfinite induction does not suffice. At first sight the amount of induction seems huge but we shall see that things don't come that bad after all and ACA_0 will work. In this session we dwell on the subtleties between the various kinds of induction. In particular, we shall look at what is called reflexive transfinite induction.
Speaker: Joost J. Joosten
Title: The Turing Jump interpretation of modal logic revisited
Date: Wednesday, January 17, 2018
Time: 12:30-13:45
Location: Logic Seminar
Abstract: We study a recursive equation for what we coined the Turing jump interpretation of transfinite polymodal provability logic. A theory that can express and prove this recursion up to some ordinal Lambda is called a GLP_Lambda amenable theory (GAT). We will show that for GATs, we can obtain soundness of the GLP axioms without many further assumptions on the base theory. However, we will need a form of transfinite induction since external transfinite induction does not suffice. At first sight the amount of induction seems huge but we shall see that things don't come that bad after all and ACA_0 will work.
Speaker: Fabian Romero Jimenez
Title: Current trends in industry applications of software verification tools
Date: Tuesday, November 28, 2017
Time: 12:30-14:00
Location: Logic Seminar
Abstract:Software bugs have a combined cost of hundreds of millions of
dollars and many human casualties. They disrupt essential services and cause uncountable other lesser damages.
Formal verification has made significant strides over the last years and has proven to be is a great way to reduce these risks.
Today it is completely feasible to create verified software within sensible effort.
Moreover, in mission-critical software, it is only reasonable and responsible to do so.
But even when feasible, it is still much harder to build verified software than "regular" software.
Building software is still hard enough, for the "software crisis" is still well and alive.
Slides are available.
Speaker: Joost J. Joosten
Title: Soundness of GLP axioms from a recursive equation
Date: Wednesday, November 22, 2017
Time: 12:30-14:00
Location: Logic Seminar
Abstract: We define a recursive equation for what we coined the Turing jump interpretation of transfinite polymodal provability logic. A theory that can express and prove this recursion up to some ordinal Lambda is called a GLP_Lambda amenable theory (GAT). We will show that for GATs, we can obtain soundness of the GLP axioms without many further assumptions on the base theory.
Speaker: Eduardo Hermo Reyes
Title: Turing-Schmerl Calculus beyond \varepsilon_0
Date: Wednesday, November 15, 2017
Time: 12:30-14:00
Location: Logic Seminar
Abstract: We shall present the system TSC (Turing-Schmerl Calculus) tailored to express all principles that hold between different Turing progressions given a particular set of natural consistency notions and a recursive ordinal \Lambda. The system is proven to be arithmetically sound and complete for a natural interpretation, named the Formalized Turing Progressions Interpretation.
Joint work with Joost Joosten.
Speaker: Ana Borges
Title: Systems for nonstandard Heyting arithmetic
Date: Thursday, November 2, 2017
Time: 12:30-14:00
Location: Logic Seminar
Abstract: Our goal is to extend Gödel's dialectica
interpretation to the nonstandard setting. In order to accomplish
that, we start by describing systems for nonstandard Heyting
arithmetic, which also include a new kind of type for sequences. See
Section 3.1 of Borges' Master
thesis.
Speaker: Ana Borges
Title: Gödel's dialectica interpretation
Date: Wednesday, October 25, 2017
Time: 12:30-14:00
Location: Logic Seminar
Abstract: In this session, armed with the knowledge of what Heyting Arithmetic in all finite types is, we will learn about Gödel's dialectica interpretation from a theoretical point of view, seeing what it does and how it works. We will also talk about ways it can be changed and applied to other theories of arithmetic. See Section 2.2 of Borges' Master thesis or this document also written by Ana Borges.
Date: Wednesday, October 4, 2017
Title: Heyting Arithmetic in all finite types
Speaker: Ana Borges
Time: 12:30 --14:00
Location: Logic Seminar Room
Abstract: First proposed as a way of reducing the consistency of Peano Arithmetic to the consistency of a quantifier-free version of Heyting Arithmetic, Gödel's dialectica interpretation ended up being the seed for a whole new tool of mathematics: proof mining. In this session, we will learn about the theory of (weakly extensional) Heyting Arithmetic in all finite types, which is the theory interpreted by the dialectica interpretation. This will give us the tools to study Gödel's interpretation in the next session.
Date: Thursday, June 15, 2017
Title: Complexity of alpha-equality in untyped lambda-calculus and separation of lambda-terms
Speaker: Andrea Condoluci
Time: 12:45 --13:45
Location: TBA
Abstract: Complexity of alpha-equality in untyped lambda-calculus and separation of lambda-terms
Date: Wednesday, April 19, 2017
Title: Decidability of some interpretability logics
Speaker: Luka Mikec
Time: 10:30 --12:00
Location: Logic Seminar Room
Abstract:
The usual way to prove decidability of a modal logic with relational (Kripke-style) semantics is to prove it has the finite model property. Interpretability logics are usually interpreted on classes of Veltman models, or generalized Veltman models, which are both extensions of Kripke models. In this talk, we describe an approach to proving the finite model property by defining a certain filtration. We work with generalized Veltman models, and use maximal bisimilarity for gluing the worlds. We will sketch some issues that appear when trying to work with regular Veltman models. We will use this approach to prove decidability of the logic ILM_0. If time permits, we will also comment on decidability of ILW*, and possibly on the computational complexity of some interpretability logics.
Luka Mikec is an invited speaker from the University of Rijeka, Croatia (Department of Mathematics) and his travel is supported by the project 2016 DI 0032.
Date: Wednesday, March 22, 2017
Title: On the Turing Jump interpretation of transfinite provability logic and its formalizations II
Speaker: Joost J. Joosten
Time: 11:05 --12:05
Location: Logic Seminar Room
Abstract:
We describe a recursive provability equation which is a transfinite generalization of "provable together with all true Pi_n formulas". We discuss the good properties of such a recursion equation and next dwell on the questions where such recursion is definable so that the basic properties become provable.
Date: Wednesday, March 15, 2017
Title: On the Turing Jump interpretation of transfinite provability logic and its formalizations I
Speaker: Joost J. Joosten
Time: 11:05--12:05
Location: Logic Seminar Room
Abstract:
We describe a recursive provability equation which is a transfinite generalization of "provable together with all true Pi_n formulas". We discuss the good properties of such a recursion equation and next dwell on the questions where such recursion is definable so that the basic properties become provable.
Date: Thursday, March 9, 2017
Title: Transfinite Turing Jumps
Speaker: Joost J. Joosten
Time: 11:05
Location: 12:05
Abstract:
We dwell on transfinite iterations of the Turing jump and discuss the various degree structures endowed with these jumps.
Date: Wednesday, March 1, 2017
Title: Vaught's conjecture in Computability theory
Speaker: Antonio Montalban
Time: 11:05-12:05
Location: Room 401, Philosophy Department, C. Montalegre 6
We have decided to allocate this as a session of the Barcelona Logic Seminar.
Abstract:
We'll describe Vaught's conjecture, which is one of the most
well-known and longest-standing open questions in logic. The
conjecture essentially says that the continuum hypothesis holds when
restricted to counting the number of models of a theory. We'll mention
the author's result that this conjecture is equivalent to a
computability-theoretic statement.
No background knowledge will be assumed.
Date: Wednesday, January 25, 2017
Title: Caristi's theorem in reverse mathematics
Speaker: David Fernánuez-Duque
Time: 11:05-12:05
Location: Logic Seminar
Abstract:
Caristi's theorem is a fixed-point result in dynamical systems. Unlike
many related results, it applies to possibly discontinuous functions.
This makes it a challenge to analyze it in the context of reverse
mathematics, where theorems in analysis are formalized using the natural
numbers and its powerset, suitable for reasoning about real numbers and
continuous functions. In this talk, we will discuss Caristi's result and
show that it can be formalized using only arithmetical comprehension;
however, we note that a stronger version of the result can be extracted
from the original proof. As we will show, this strong Caristi theorem is
equivalent to the arithmetical inflationary fixed point scheme, a theory
which is much stronger than any of the 'big five' systems of reverse
mathematics.
Date: Wednesday, November 9, 2016
Title: Transfinite Turing Jumps and Provability
Speaker: Joost J. Joosten
Time: 11:05-12:05
Location: Logic Seminar
Abstract:
We will study definability of subsets of the natural numbers in terms of provability predicates and relate this to the well known hierarchy of Turing jumps. Our emphasis will be on the hyperarithmetical sets. We present work in progress on how exactly our new notion of provability runs in phase with the hierarchy of Turing jumps. Apart from providing some preliminary results, we will give an ample motivation for the project. In particular, it seems that recent algebraic formulations of the so-called Reduction Property will prove useful once the exact relation between Turing jumps and provability predicates is in place.
Date: Wednesday, October 26, 2016
Title: Turing Jumps and provability
Speaker: Joost J. Joosten
Time: 11:05-12:05
Location: Logic Seminar
Abstract:
We will study definability of subsets of the natural numbers in terms of provability predicates and relate this to the well known hierarchy of Turing Jumps. We start with the arithmetical hierarchy and next make our first explorations into the realm of hyperarithmetical sets.
Date: Wednesday, October 19, 2016
Title: First steps towards logic of informal provability, II
Speaker: Pawel Pawlowski (Ghent University)
Time: 11:05-12:05
Location: Logic Seminar
Abstract:
Mathematicians prove theorems. They don't do that in any particular axiomatic system. Rather, they reason in a semi-formal setting, providing what we'll call informal proofs. There are quite a few reasons not to reduce informal provability to formal provability within some appropriate axiomatic theory. But the main worry is that we seem committed to all instances of the so-called reflection schema, which roughly says that if something is provable then it is true. Yet, adding all its instances to any theory for which other intuitive principles of provability hold leads to inconsistency.
We develop a non-functional many-valued logics which avoid this problem and captures our intuitions about informal provability. The logics are inspired by paraconsistent logic CLuN, in whose standard semantics the value of a negation is not determined by the value of its argument. We describe the semantics of our logics and some of their properties.
The second part will enter into the details of a new proposal whereas the first part of the talk, two weeks ago, merely set the stage and intended to provide motivation and background.
Date: Wednesday, October 5, 2016
Title: First steps towards logic of informal provability, I
Speaker: Pawel Pawlowski (Ghent University)
Time: 11:05-12:05
Location: Logic Seminar
Abstract:
Mathematicians prove theorems. They don't do that in any particular axiomatic system. Rather, they reason in a semi-formal setting, providing what we'll call informal proofs. There are quite a few reasons not to reduce informal provability to formal provability within some appropriate axiomatic theory. But the main worry is that we seem committed to all instances of the so-called reflection schema, which roughly says that if something is provable then it is true. Yet, adding all its instances to any theory for which other intuitive principles of provability hold leads to inconsistency.
We develop a non-functional many-valued logics which avoid this problem and captures our intuitions about informal provability. The logics are inspired by paraconsistent logic CLuN, in whose standard semantics the value of a negation is not determined by the value of its argument. We describe the semantics of our logics and some of their properties.
Date: Wednesday, September 21, 2016
Title: The Topological Completeness of GLP_Lambda
Speaker: Juan Pablo Aguilera (Vienna University of Technology)
Time: 16:30-17:30
Location: Philosophy Seminar (fourth floor of Carrer Montalegre 6, the room next to the Aula Magna)
Abstract:
We sketch the proof of the fact that any tall-enough scattered space can be extended to a model of the polymodal provability logic GLP_Lambda.
Date: Tuesday, September 20, 2016
Title: Numerical Approximations to Non-computable Functions for Graph and Tensor Complexity
Speaker: Hector Zenil (Karolinska Institute and Oxford University)
Time: 16:30-17:10
Location:
Theoretical Philosophy Seminar Room (4085)
Abstract:
I will show that real-value approximations of Kolmogorov-Chaitin complexity K(s) using the so-called Algorithmic Coding Theorem, as calculated from the output frequency of a large set of small deterministic Turing machines, is consistent with various theoretical and numerical expectations, such as an almost perfect correlation between number of instructions (program size) and string algorithmic frequency. I will also show that neither K(s) nor the number of instructions used manifest any correlation with Bennett's Logical Depth LD(s), other than what's predicted by the theory itself (shallow and non-random strings have low complexity for both K and LD). The agreement between the theory and the numerical calculations shows that despite the undecidability of these theoretical measures, the rate of convergence of approximations is stable enough to devise applications. I will show that numerical approximations of algorithmic complexity measures can be used to approach the challenge of string, graph and tensor complexity capturing important group-theoretic and topological properties. We explore a measure, based upon the concept of Algorithmic Probability, that elegantly connects to Kolmogorov complexity, and that provides a natural approach to n-dimensional algorithmic complexity by using n-dimensional deterministic Turing machines. Finally, these measures drawn from computability and complexity theories are used in fundamental problems of causality and in molecular biology experiments, thus coming all the way from theory to computer simulation to biological validation.
Location: History Seminar Room (4029)
Date: Wednesday, May 25, 2016
Time: 12:30-14:00
Title: A term model for the closed fragment of transfinite provability logic
Speaker: Joost J. Joosten
Abstract:
In this talk we will look at the well-known structure known as Ignatiev's model as a universal model for the closed fragment of the transfinite polymodal provability logic GLP. Our focus will not be to prove that indeed the model is universal, but rather we wish to understand why the model is as it is and if other structures would have served the same purpose. To answer this question we start out with a rather general set-up and shall see that, given some modeling choices, Ignatiev's model is the necessary outcome. Although we do not perform a Henkin construction, nor do we consider the canonical model, we do work with sets of worms and thereby refer to the resulting structure as a term model.
Location: History Seminar Room (4029)
Date: Wednesday, May 4, 2016
Time: 12:30-14:00
Title: Turing Taylor Expansions of Arithmetical Theories
Speaker: Joost J. Joosten
Abstract:
Analytic functions can be endowed with a Taylor expansion around any given point in its domain. In a sense, one can project an analytical function f on a basis of orthogonal monomials x^n and f can be written as some sum of such monomials. We shall see that for a large class of arithmetical theories T something similar holds. The monomials are replaced by Turing progressions over Elementary Arithmetic and natural theories T can be expressed as the union of these monomials. However, we only have orthogonality of the monomials on certain intervals. This is not a problem since we can show that any union of monomials is provably equivalent to one in such an interval. These intervals are seen to live in a well-known structure: Ignatiev's universal modal model of the closed fragment of Japaridze's polymodal provability logic GLP. This is very nice and thus, points in Ignatiev's model can be interpreted in various ways: Turing Taylor expansions of natural arithmetical theories, ordinals, natural sequences of iterating end-logarithms on ordinals, and of course, modal formulae. This cross-interpretability powers applicability of these polymodal provability logics which we shall discuss as well.
Location: Logic Seminar Room
Date: Thursday, April 7, 2016
Time: 12:30-14:00
Title: Labelled Tableaux for Interpretability Logics
Speaker: Tuomas Hakoniemi
Abstract:
We present labelled tableaux proof systems for interpretability logics. We give a base system for the basic interpretability logic IL and show how to extend the system for any interpretability logic that is sound and complete with respect to a class of IL-frames determined by a set of strict universal Horn sentences.
This is joint work with Joost J. Joosten.
Location: Logic Seminar Room
Date: Wednesday, February 3, 2016
Time: 12:30-14:00
Title: Metamathematics in bounded arithmetic
Speaker: Joost J. Joosten
Abstract:
Bounded arithmetic is tailored to capture and reason about the poly-time functions. We shall point out how one can formalize syntax in bounded arithmetic and perform simple inductive arguments. However, we do not have access to normal induction. Rather we shall work with what is called length induction or other types of induction. The idea is that you only need to do logarithmically (in the size of the number) many calls upon the induction hypothesis and not linearly many.
Next we return our focus to the previous session and to the notion of relative interpretability as introduced by Tarski, Mostowski and Robinson.
Recall that relative interpretations are widely used in mathematics and logic, for example to yield relative consistency proofs or undecidability results.
We shall see how the notion of relative interpretability can be formalized in different ways in bounded arithmetic. Next we shall discuss the Orey-Hájek characterization of relative interpretability and comment on where the various implications can be formalized.
Location: Logic Seminar Room
Date: Thursday, January 14, 2016
Time: 17:00-18:30
Title: Formalizations of relative interpretability
Speaker: Joost J. Joosten
Abstract:
We consider the notion of relative interpretability as introduced by Tarski, Mostowski and Robinson.
Relative interpretations are widely used in mathematics and logic, for example to yield relative consistency proofs or undecidability results.
We shall see how the notion of relative interpretability can be formalized in different ways in arithmetic. These different ways coincide for stronger theories but yield different notions over weaker base theories. If time allows we shall discuss the Orey-Hájek characterization of relative interpretability.
Speaker: David Fernández Duque
Title: Transfinite reflection principles and systems of second-order arithmetic
Date: Wednesday, December 2, 2015
Time: 12:00-13:00
Location: Logic Seminar Room
Abstract:
A classic result of Kreisel and Lévy states that Peano Arithmetic is equivalent to uniform reflection over Primitive Recursive Arithmetic. We will show how this is not an isolated phenomenon, as the stronger three of the "Big Five" theories of reverse mathematics, ACA0, ATR0, and Π11-CA0, are also equivalent to strong reflection principles over the weakest of the Big Five, RCA0. Such principles are obtained by transfinitely iterating the ω-rule up to a suitable ordinal and allowing an oracle for an arbitrary set X. We will also discuss how these results may lead to a Π01 ordinal analysis of these theories, as Beklemishev has done for Peano Arithmetic. There are slides of the talk available.
Location: Logic Seminar Room
Date: Wednesday, March 18, 2015
Time: 13:00-14:15
Title: On the core logic for relative interpretability
Speaker: Joost J. Joosten
Abstract:
We shall look at various principles in the core logic of relative interpretability and shall prove them to be sound in any arithmetical theory strong enough to formalize coding of syntax. Next we shall look at modal semantics for the logic. Since we work with a binary modality, we will work with ternary accessibility relations.
Location: Logic Seminar Room
Date: Wednesday, March 4, 2015
Time: 13:00-14:15
Title: Logics for interpretabiilty
Speaker: Joost J. Joosten
Abstract:
A theory U interprets a theory V in the sense of Tarski, Mostowski and Robinson if there is some translation under which all theorems of V are provable in U (where quantifiers may be restricted to a domain specifier). One can formalize this notion in arithmetical theories that allow for coding of syntax. We will study the structural behavior of formalized interpretability between theories which are sentential extensions of an arithmetical base theory of some minimal strength and collect our findings in modal logics which are called interpretability logics.
We shall see that logics for interpretability are not as stable as logics for provability. It is an open problem to determine the core logic of basic interpretability logics.
Location: Logic Seminar Room
Date: Wednesday, January 28, 2015
Time: 13:00-14:15
Title: Countable omega models and predicative reflection
Speaker: Joost J. Joosten
Abstract:
We will use some classical results on countable omega-models in predicative analysis to show that predicative analysis proves predicative Π12-reflection. Basically, predicative Π12-reflection says that whenever we can prove that a certain ordering is a well-order, then all Π12-statements that we can prove using omega-rules along this well-order are actually true.
This is joint work with Andrés Cordon Franco, David Fernández Duque and Félix Lara Martín.
Location: Logic Seminar Room
Date: Wednesday, January 14, 2015
Time: 13:00-14:15
Title: Rosser-style arguments
Speaker: Joost J. Joosten
Abstract:
Rosser could prove a strengthening of Goedel's First Incompleteness Theorem in that he only required the c.e. theory with sufficient number theory to be consistent for it to be incomplete. We shall focus on the underlying technique of witnessing comparison. This technique can be used to prove the so-called Friedman-Goldfarb-Harrington Theorem to the extend that each Sigma formula is provably equivalent to some provability statement (modulo consistency). If time allows, we shall discuss this theorem, its generalizations and applications.
Location: Logic Seminar Room
Date: Wednesday, December 17, 2014
Time: 13:00-14:15
title: On formalized interpretability in not too strong theories of arithmetic
Speaker: Joost J. Joosten
Abstract:
A theory U interprets a theory V in the sense of Tarski, Mostowski and Robinson if there is some translation under which all theorems of V are provable in U (where quantifiers may be restricted to a domain specifier). One can formalize this notion in arithmetical theories that allow for coding of syntax. We will study the structural behavior of formalized interpretability between theories which are sentential extensions of an arithmetical base theory of some minimal strength and collect our findings in a modal logic.
Location: Logic Seminar Room
Date: Wednesday, October 29, 2014
Time: 13:00-14:15
title: Provability with a set-oracle
Speaker: Joost J. Joosten
Abstract:
We wish to characterize principles of second order arithmetic like comprehension or transfinite recursion in terms of reflection principles. In order to deal with second order set parameters in these principles we need to be able to denote such parameters in the context of formalized provability. We know that each number can be denoted by a name for it. In a countable language we cannot do so for sets of course. To overcome this obstacle we introduce the notion of oracle provability and see how this behaves and can be formalized in second order number theory.
This is joint work with Andrés Cordon Franco, David Fernández Duque and Félix Lara Martín.
Location: Logic Seminar Room
Date: Wednesday, October 29, 2014
Time: 13:00-14:15
title: On the intimate relations between reflection, consistency and induction
Speaker: Joost J. Joosten
Abstract:
We revisit classical results relating the intimate relations between reflection principles, consistency statements and fragments of first order arithmetic and shall dwell on the question how this can be extended to second order arithmetic.
Location: Logic Seminar Room
Date: Wednesday, May 28, 2014
Time: 12:15-14:00
title: Graded Turing progressions through modal logic
Speaker: Euardo Hermo-Reyes
Abstract:
Graded Turing progressions arise by iteratedly adding formalized n-consistency statements to a base theory using different natural numbers n. It is known that the modal logic GLP can be used to denote any finite level of these progressions. However, at transfinite levels, this link between GLP and Turing progressions is only by approximating the progression. We propose a new modal signature that can directly denote transfinite progressions and not only approximate them. We shall prove certain axioms of this logic to be arithmetically correct.
This is joint work with Laia Jornet-Somoza and Joost J. Joosten.
Location: Logic Seminar Room
Date: Wednesday, April 02, 2014
Time: 12:15-14:00
title: Reflexive transfinite induction and applications to formalized Turing progressions
Speaker: Joost J. Joosten
Abstract:
In weaker theories we do not have access to full arithmetic transfinite induction, even for small ordinals. For various statements, however, a weaker notion Reflexive transfinite induction suffices so that often EA can serve as a base theory. In case we need formalized collection we have to resort to a base theory where Sigma_1 collection in provable leading to accepting the totality of the hyper-exponential function. If all is in place, we can formalize well the notion of Turing progression and apply that as the basis for proof-theoretic analyses.
Location: Logic Seminar Room
Date: Wednesday, March 19, 2014
Time: 12:15-14:00
title: Formalizing transfinite progressions in the absence of transfinite induction
Speaker: Joost J. Joosten
Abstract:
Various natural transfinite progressions of theories of increasing strength are defined using provability. The natural way to reason about these progressions is by using transfinite induction. However, transfinite induction is quite a strong principle so that if we wish to formalize our reasoning this is bad. However, we can do better. Since the progressions are defined using provability, often we can formalize our reasoning in rather weak theories due to tricks based on Lüb's rule and the Outside Big, Inside Small principle. The latter asserts that, although not all elements are inside any definable cut, they are provably so! We revisit these tricks resulting in among others what is called Reflexive Induction. Next we shall see how this can be put to work to formalize various transfinite progressions in Elementary Arithmetic. If time allows we shall move on to see some applications.
Location: Logic Seminar Room
Date: Wednesday, January 22, 2014
Time: 12:15-14:00
title: An empirical logician's apology
Speaker: Joost J. Joosten
Abstract:
In this talk we see how running simulations of small Turing machines on super-computers reveals an unexpected and new relation between geometrical complexity (fractal dimension) on the one hand and computational complexity on the other hand. After presenting the results we shall try to place them in the panorama of various other --relevant to our research-- results, that relate different notions of complexity to each other. This is joint work with Hector Zenil from Unit of Computational Medicine, Center for Molecular Medicine, Karolinska Institutet, and Fernando Soler-Toscano from the University of Sevilla.
Location: Logic Seminar Room
Date: Wednesday, January 8, 2014
Time: 12:15-14:00
title: Logics for Turing progressions
Speaker: Joost J. Joosten
Abstract:
The logics of GLP and RC are nice in that they have good algebraic, logical and computational properties and moreover provide an alternative ordinal notation system. The applicability of the logics GLP and RC to proof theory is mainly given through the link to Turing progressions. Finite Turing progressions can be explicitly given by a modal formula. For transfinite Turing progressions we only have approximations. In this talk we wish to start an investigation to see, on the one hand, to what extend we can expand the expressibility of the modal language to better speak of Turing progressions while, on the other hand, still maintain the nice properties of the logics. In particular we shall present a logic of Beklemishev's that has for each ordinal α below ε0 a modality [α] that will be interpreted as provability in the αth Turing progression.
Location: Logic Seminar Room
Date: Wednesday, December 18, 2013
Time: 12:15-14:00
title: HOTT Reading group
Speaker: Cory Knapp
Abstract:
An overview of univalence and higher inductive types.
Location: Logic Seminar Room
Date: Wednesday, November 27, 2013
Time: 12:15-14:00
title: HOTT Reading group
Speaker: Cory Knapp
Abstract:
We will quickly cover coproducts, booleans and natural numbers, and spend the rest of the time dwelling on identity types.
Location: Logic Seminar Room
Date: Wednesday, November 20, 2013
Time: 12:15-14:00
title: PSPACE completeness of the closed fragment of GLP
Speaker: Joost J. Joosten
Abstract:
It is known that the closed fragment of GL is decidable (theoremhood) in PTIME. Bou and the author showed that some extension of GL by adding a binary modal operator for interpretability yields a PSPACE complete closed fragment. In this presentation we shall look at a result of Pakhomov to the extent that the closed fragment of GLP is also PSCPACE complete.
Location: Logic Seminar Room
Date: Wednesday, November 13, 2013
Time: 12:15-14:00
title: Homotopy Type Theory
Speaker: Cory Knapp
Abstract:
We spoke on introduction, elimination and computation rules and in particular dwelt on (dependent) product and W-types.
Location: Logic Seminar Room
Date: Wednesday, November 06, 2013
Time: 12:15-14:00
title: TBA
Speaker: Joost J. Joosten
Abstract:
We saw how questions about the xi-consistency ordering can be reduced to simplified questions. In particular we saw a recursive reduction to the 0-consistency ordering.
Location: Logic Seminar Room
Date: Wednesday, October 30, 2013
Time: 12:15-14:00
title: Homotopy Type Theory
Speaker: Cory Knapp
Abstract:
TBA
Location: Logic Seminar Room
Date: Wednesday, October 23, 2013
Time: 12:15-14:00
title: Combinatorics in formal provability
Speaker: Paul Erdös
Abstract:
Of course, this is a silly joke.
Location: Logic Seminar Room
Date: Wednesday, October 23, 2013
Time: 12:15-14:00
title: Homotopy Type Theory
Speaker: Cory Knapp
Abstract:
We discuss motivations for HOT and introduce some basic formation, elimination and computation rules.
Location: Logic Seminar Room
Date: Wednesday, October 15, 2013
Time: 12:15-14:00
title: The worm project: current state of affairs
Speaker: Joost J. Joosten
Abstract:
In this talk, we have given an overview of recent results in the Pi^0_1 ordinal analysis project.
Location: Logic Seminar Room
Date: Wednesday, May 15, 2013
Time: 12:15-14:00
title: Well-founded orders and anti-chains in the Japaridze Algebra
Speaker: Joost J. Joosten
Abstract:
It is known that we can order the class of all worms according to consistency strength. For regular consistency this yields a well-order. For higher consistency notions the relation is still well-founded, yet no longer linear, containing wild structures of anti-chains.
Location: Logic Seminar Room
Date: Wednesday, May 8, 2013
Time: 12:15-14:00
title: Predicativism and the foundations of mathematics
Speaker: Joost J. Joosten
Abstract:
In this session we discuss writings of Feferman on Predicativism and the foundations of mathematics.
Location: Logic Seminar Room
Date: Wednesday, April 24, 2013
Time: 12:15-14:00
title: Topological models of GLP and set theory II
Speaker: Joan Bagaria
Abstract:
In this talk we discuss which large cardinal assumptions are needed for certain natural topologies to be non-discrete. The non-discreteness in turn is needed for completeness proofs for natural topological interpretations of GL and GLP.
Location: Logic Seminar Room
Date: Wednesday, April 17, 2013
Time: 12:00-14:00
title: Impredicative provability logic
Speaker: David Fernández Duque
Abstract:
Recent work by Joosten and the speaker shows how Japaridze's polymodal provability logic GLP may be interpreted using iterated omega-rules. This in turn suggests a strategy for extending Beklemishev's technique for computing Pi^0_1-ordinals to predicative theories of second-order arithmetic, whose proof-theoretic strength is bounded by the Feferman-Sch�tte ordinal Gamma_0.
However, the analysis of stronger theories, such as the theory ID_1 of inductive definitions, typically involves the study of potentially uncountable proofs. Such proofs cannot be directly modeled using omega-rules. To this end, in this talk we shall introduce provability operators based on an uncountable well-order. Given a cardinal k, one considers a k-rule, which has one premise for each x<k. Such a rule may be iterated transfinitely, much as the omega-rule. We shall show that this gives rise to a proof-theoretic interpretation for the polymodal provability logic enriched with uncountable modalities, and discuss how ID_1 may be represented within this framework.
Location: Logic Seminar Room
Date: Wednesday, April 03, 2013
Time: 12:15-14:00
title: Topological models of GLP and set theory
Speaker: Joan Bagaria
Abstract
In this talk we discuss which large cardinal assumptions are needed for certain natural topologies to be non-discrete. The non-discreteness in turn is needed for completeness proofs for natural topological interpretations of GL.
Location: Logic Seminar Room
Date: Wednesday, March 20, 2013
Time: 12:15-14:00
title: Omega completeness for ∏11 sentences
Speaker: Joost J. Joosten
Abstract
In this session we look at one-sided Tait calculus for pseudo ∏11 sentences. We prove that the truth complexity of true ∏11 sentences is always below ω1CK.
Location: Logic Seminar Room
Date: Wednesday, March 13, 2013
Time: 12:15-14:00
title: Truth complexity for ∏11 sentences
Speaker: Joost J. Joosten
Abstract
In this session we look at one-sided Tait calculus for Second Order Logic and fragments. Next we introduce the truth complexity of formulas and analyze the truth complexity of true ∏11 sentences.
Location: Logic Seminar Room
Date: Wednesday, March 6, 2013
Time: 12:15-14:00
title: Arithmetical Completeness of G�del L�b Provability logic
Speaker: Joost J. Joosten
Abstract
In this presentation we present Solovay's classical proof to the extent that GL is complete for its provability interpretation in Peano Arithmetic. We shall use arithmetical soundness as given in this presentation.
Location: Logic Seminar Room
Date: Wednesday, February 27, 2013
Time: 12:15-14:00
title: Sequent calculi, completeness and a non-constructive cut-elimination proof
Speaker: Joost J. Joosten
Abstract
We will study Tait's one-sided cut-free calculus in more detail. We shall prove completeness of this calculus using Schütte's method of search-trees. Once we have completeness it is easy to see that the cut-rule is admissible in this calculus yielding a non-constructive proof of cut-elimination.
Location: Logic Seminar Room
Date: Wednesday, February 20, 2013
Time: 12:15-14:00
title: Sequent calculi, first and second order
Speaker: Joost J. Joosten
Abstract
In this session we shall look at various sequent calculi. In particular we will study Tait's one-sided cut-free calculus and its main properties.
Location: Logic Seminar Room
Date: Wednesday, February 13, 2013
Time: 12:15-14:00
title: Normalization for Natural Deduction
Speaker: Joost J. Joosten
Abstract
In this session we presented a classical result on normalization/cut-elimination in a Natural Deduction proof system for Predicate Logic yielding a syntactic consistency proof of Predicate Logic.
Location: Logic Seminar Room
Date: Wednesday, January 23, 2013
Time: 12:15-14:00
title: Introspective theories and the omega rule
Speaker: Joost J. Joosten
Abstract
In this session we shall prove the two most involved GLP axioms correct for our omega-rule interpretation. We shall see that we need to assume the existence of a provability predicate to prove soundness of our Euclidean axiom < a > A --> [b] <a> A for a<b. However, we shall prove that each theory is equi-consistent with one that has a provability predicate. We call such theories introspective. Moreover, we see that introspective theories are provably introspective.
Joint work with David Fernández Duque.
Location: Logic Seminar Room
Date: Wednesday, December 19, 2012
Time: 12:15-14:00
title: Fragments of second order arithmetic
Speaker: Joost J. Joosten
Abstract
In this session we will focus on some main systems of second order arithmetic like Arithmetic Transfinite Recursion, Arithmetic Comprehension Axioms, and Recursive Comprehension Axioms. Moreover, we shall see what can be proven in these respective systems about formalized transfinite provability. We shall relate the existence of transfinite provability predicates to principles of transfinite induction.
Joint work with David Fernández Duque.
Location: Logic Seminar Room
Date: Wednesday, November 21, 2012
Time: 12:15-14:00
title: The omega rule interpretation of transfinite provability logics
Speaker: Joost J. Joosten
Abstract
In this session we will derive some first provable basic results when interpreting [α]T as "provable in T using a proof tree with at most α many nested applications of the omega-rule". It is our aim to see that the logic thus defined will be GLP again.
Joint work with David Fernández Duque.
Location: Logic Seminar Room
Date: Wednesday, November 11, 2012
Time: 12:15-14:00
title: Omega rules formalized in Second Order Arithmetic
Speaker: Joost J. Joosten
Abstract
We shall see how to formalize the notion of being provable by transfinitely iterated applications of the omega rule in second order number theory.
Joint work with David Fernández Duque.
Location: Logic Seminar Room
Date: Wednesday, October 24, 2012
Time: 12:15-14:00
title: Omega rules
Speaker: Joost J. Joosten
Abstract
We will discuss omega-rules, their history, their applications and possible systems where to formalize the notion of being provable by transfinitely iterated applications of the omega rule.
Location: Logic Seminar Room
Date: Wednesday, May 16, 2012
Time: 12:15-14:00
title: Ordinal analysis for set theory and fragments
Speaker: Joost J. Joosten
Abstract
We shall explore possible set-theoretical interpretations of the poly-modal provability logic GLP. In particular, we shall look at ZFC minus Replacement and Infinity as our base theory. By a result of Levy it is known that adding reflection to this base theory gives us full ZFC again. Applying techniques from consistency proofs based on GLP gives us some indefinability results over this weak base theory.
Joint work with Joan Bagaria.
Location: Logic Seminar Room
Date: Wednesday, May 2, 2012
Time: 12:15-14:00
title: Π01 Ordinal analysis beyond Peano arithmetic
Speaker: Joost J. Joosten
Abstract
We strip the consistency proof of PA based on GLP from all unnecessary ingredients and try to milk this analysis. In particular, we note that only arithmetical soundness of GLP is needed for a consistency proof. Also we simplify the reduction property and note that as such this property is not needed in full generality for a consistency proof.
Moreover, we sketch how this method can be used to obtain ordinal analyses relative to strong base theories.
Location: Logic Seminar Room
Date: Wednesday, March 28, 2012
Time: 12:15-14:00
title: Model constructions for the closed fragment of GLP
Speaker: Joost J. Joosten
Abstract
For GLPω we have a very good understanding of the universal model for the closed fragment. In particular we have various ways to look at this model and construct it. There is a definition around in terms of ordinal coordinates and there is a way how to define the model in terms of directed limits. For GLPΛ with Λ > ω we only have the definition in terms of ordinal coordinates. In this talk we put forward a natural candidate to also have directed limits for this case. Moreover, we also try to address the problem of the dependence of our ordinal notation system since our candidate essentially works with Veblen Normal Form representations of ordinals.
Joint work with Enrique Casanovas.
Location: Logic Seminar Room
Date: Wednesday, March 21, 2012
Time: 12:15-14:00
title: A consistency proof of Peano Arithmetic
Speaker: Joost J. Joosten
Abstract
In this session we provide a consistency proof of PA based on GLP in full detail. The proof we present is due to Beklemishev.
Location: Logic Seminar Room
Date: Wednesday, March 7, 2012
Time: 12:15-14:00
title: Ordinal analysis based on Turing progressions
Speaker: Joost J. Joosten
Abstract
We see how Turing progressions can be used to obtain various ordinal analyses. Currently the state of art lies at Π0n analyses with n ∈ω but it is likely to generalize this.
Location: Logic Seminar Room
Date: Wednesday, February 22, 2012
Time: 12:15-14:00
title: Worms and Turing progressions
Speaker: Joost J. Joosten
Abstract
We shall see how generalized notions of consistency statements can be naturally employed to talk about Turing progressions. Moreover, our worms are seen to be sufficient for many purposes in this project.
Location: Logic Seminar Room
Date: Wednesday, February 8, 2012
Time: 12:15-14:00
title: Hyper-exponentials
Speaker: Joost J. Joosten
Abstract
In this sessions we shall look at how to transfinitely iterate normal functions in a non-trivial way. We define a new notion that we call hyperations that can be seen as transfinite iteration and see what happens if we hyperate (a minor adaptation) ordinal exponentiation with base ω. We see that we end up with a sequence of normal functions that is a refinement of the well-known Veblen functions. Moreover, we shall also briefly discuss what we call cohyperations which can be seen as transfinite iterations of initial functions (ordinal functions that map initial segments to initial segments). Cohyperations, like hyperations, possess a rich algebraic structure and they provide natural left inverses to hyperations.
Joint work with David Fernández Duque.
Location: Logic Seminar Room
Date: Wednesday, January 25, 2012
Time: 12:15-14:00
title: Ordinal assignments for worms beyond GLPω
Speaker: Joost J. Joosten
Abstract
This session is a natural follow-up to the previous ones where we now consider the general case for any worms. The formalism we present is new in that it uses special ordinal functions.
Joint work with David Fernández Duque.
Location: Logic Seminar Room
Date: Wednesday, January 11, 2012
Time: 12:15-14:00
title: Ordinal assignments for worms in GLPω
Speaker: Joost J. Joosten
Abstract
To each worm A, we can assign an ordinal o(A) in a very natural way. We look at the collection of worms B whose consistency follows from A and order this collection under the relation of implying consistency. The corresponding order type of this collection is our ordinal assignment o(A). We will provide a known calculus as presented by Beklkemishev but provide new proofs.
Joint work with David Fernández Duque.
Location: Logic Seminar Room
Date: Wednesday, December 14, 2011
Time: 12:15-14:00
title: Well-orders in GLP
Speaker: Joost J. Joosten
Abstract
We shall discuss how the transfinite Japaridze algebra naturally lodges various interesting well-orders. In later sessions we shall see that these well-orders are actually very informative in a well-defined proof-theoretical sense.
Joint work with David Fernández Duque.
Location: Logic Seminar Room
Date: Wednesday, November 30, 2011
Time: 12:15-14:00
title: Models for GLPω
Speaker: Joost J. Joosten
Abstract
We shall see that GLPω in general is Kripke incomplete. In particular the various frame conditions would enforce us to only consider trivial models. However the closed fragment does allow for natural Kripke semantics as was pointed out by Ignatiev. We present a purely modal presentation of Ignatiev's model here and prove the model to be sound and complete for GLPω.
Joint work with Marco Vervoort and Lev Beklemishev.
Location: Logic Seminar Room
Date: Wednesday, September 28, 2011
Time: 12:15-14:00
title: Beklemishev Normal Forms
Speaker: Joost J. Joosten
Abstract
There are various different worms that are actually equivalent over GLP. We will see that the class of worms has a subset of natural unique representatives which we baptize Beklemishev Normal Forms. We slightly change the existing definition of Worm Normal Form as to emphasize its similarities with Cantor Normal Forms.
Location: Logic Seminar Room
Date: Wednesday, June 15, 2011
Time: 12:15-14:00
title: Worms in GLP
Speaker: Joost J. Joosten
Abstract
We look at iterated consistency statements within GLP which are called worms. We show some basic facts about them. In particular we shall see that they are closed under conjunction.
Location: Logic Seminar Room
Date: Wednesday, June 1, 2011
Time: 12:15-14:00
title: On the closed fragment of GLP
Speaker: Joost J. Joosten
Abstract
We shall focus on the closed fragment of GLP. In particular we see that each closed formulas can be written as a Boolean combination of worms.
Location: Logic Seminar Room
Date: Wednesday, May 18, 2011
Time: 12:15-14:00
title: Non-discreteness of Derived Topologies is Independent of ZFC
Speaker: Joan Bagaria
Abstract
In this talk we continue the previous lecture. We shall see that the non-discreteness of the next topology is independent of ZFC at every level.
Location: Logic Seminar Room
Date: Tuesday, May 12, 2011
Time: 12:15-14:00
title: On Derived Topologies
Speaker: Jaon Bagaria
Abstract
We shall look at derived topologies on ordinal spaces. In particular we define a hierarchy of nested topologies. Here each next topology is extending the previous one by adding all derived sets (in terms of the Mahlo operator) as new open sets. We prove some basic properties of these topologies and link them to well-known set-theoretical notions.
Location: Logic Seminar Room
Date: Wednesday, December 12, 2011
Time: 12:15-14:00
title: Topological Completeness for GLB
Speaker: Joost J. Joosten
Abstract
We present the topological completeness (using Jensen's square principle up to ℵω) result for GLB as proven by Beklemishev. Blass' result on topological interpretations of GL is a central ingredient here.
Location: Logic Seminar Room
Date: Wednesday, April 6, 2011
Time: 12:15-14:00
title: Topological spaces: trees versus partitions
Speaker: Joost J. Joosten
Abstract
We shall see how we can embed finite trees into topological spaces. For this purpose we essentially rely on Blass' results on topological interpretations of GL. Embedding trees is a first step in a completeness proof for GL à la Solovay.
Location: Logic Seminar Room
Date: Wednesday, March 16, 2011
Time: 12:15-14:00
title: Topological Semantics for GLB
Speaker: Joost J. Joosten
Abstract
We present topological semantics for modal logics based on either the interior operator or the derived set operator. We shall see that the latter is good for topological semantics for GL when using scattered spaces.
Joint work with David Fernández Duque.