**Mathematical Logic Webinar **

**March 8 | 4pm (Lisbon time)**

** **

Isabel Oitavem (FCT - Universidade Nova de Lisboa)

TITLE :: The polynomial hierarchy of functions

ABSTRACT ::

We give recursion-theoretic characterizations of all levels of the polynomial hierarchy of time and of the hierarchy itself. We characterize both, the $\Box^P_n$ and the $\Sigma^P_n$ levels.

In this work, only composition and recursion schemes are used. We identify the recursion scheme which added to FPtime leads to the full polynomial hierarchy.

LOCATION: Zoom Meeting:

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 40

**March 1 | 4pm (Lisbon time)**

Sérgio Marcelino (Instituto de Telecomunicações - IST)

TITLE :: Platypus: an unexpected Boolean connective

ABSTRACT :: Unexpectedly, this very simple connective and the logic it defines, illustrate various key advantages in working with generalized notions of semantics (by incorporating non-determinism), calculi (by allowing multiple-conclusion rules) and even of logic (moving from Tarskian to Scottian consequence relations). We show that the associated logic cannot be characterized by any finite set of finite matrices, whereas with non-determinism two values suffice. Furthermore, this logic is not finitely axiomatizable using single-conclusion rules, however we provide a very simple analytical multiple-conclusion axiomatization using only two rules. Finally, deciding the associated multiple-conclusion logic is coNP-complete, but deciding its single-conclusion fragment is in P.

LOCATION: Zoom Meeting:

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**February 22 | 4pm (Lisbon time)**

Daniel Graça (Departamento de Matemática, Faculdade de Ciências e Tecnologia da Universidade do Algarve)

TITLE :: Computability of an exact variant of Hilbert's 16th problem

ABSTRACT :: At the beginning of the 20th century, David Hilbert proposed a list of 23 open problems in mathematics which proved to be very influential. The 16th problem consists on two subproblems, the second of which asks for an upper bound on the number of limit cycles that planar polynomial vector fields of degree n can have and an investigation of their relative positions. This problem remains unsolved for all n>1.

In this talk we consider an exact variant of Hilbert's 16th problem, where we will be interested in studying the operator which maps a planar vector field to the exact number of its limit cycles. We will show that, while this operator is in general not computable, it is uniformly computable on a dense subset of C^1 vector fields over the unit ball. This talk describes joint work with Ning Zhong.

LOCATION: Zoom Meeting:

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**February 8 | 4pm (Lisbon time)**

Emanuele Frittaion (Mathematics Department of TU-Darmstadt – Germany)

TITLE :: Generic realizability for intuitionistic set theory

ABSTRACT :: Generic realizability goes back to Kreisel's and Troelstra's interpretation of intuitionistic second order arithmetic. It was later adapted to systems of intuitionistic set theory by Friedman, Beeson, McCarthy, and Rathjen. We survey known applications and present some recent ones.

Joint with Michael Rathjen and Takako Nemoto.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**February 1 | 4pm (Lisbon time)**

Matteo Manighetti (Inria Saclay & LIX, École Polytechnique, Palaiseau, France)

TITLE :: Applications of focusing to the proof theory of arithmetic

ABSTRACT ::

Linear Logic uncovered many hidden structures in the proof theory of classical and intuitionistic logic. An important property of Linear Logic, that was later also found in classical and intuitionistic logic, is the availability of focused proof systems: these are sequent calculi that drastically restrict the non-determinism associated with usual sequent calculi. The fact that they remain a sequent calculus at the core, while gaining stronger normal forms, provided a good setting for

several results in computer science. Some focused proof systems have been proposed for systems of arithmetic, aiming at applications in theorem proving and model checking. However, this is also a setting where some classical results of the metatheory of arithmetic can be studied.

In this talk, I will present a focused proof system for the theory of inductive definitions in Multiplicative-Additive Linear Logic (a linear logic without weakening and contraction) due to D. Baelde, as well as some early applications to the metatheory of arithmetic.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**January 25 | 4pm (Lisbon time)**

Fernando Ferreira (Universidade de Lisboa - CMAFcIO)

TITLE :: What is the bounded functional interpretation?

ABSTRACT ::

We explain what is the bounded functional interpretation. We work in classical logic and include an abstract type. The type can stand for the reals, a metric space, a normed space, a ring, etc. We emphasize three features of the bounded functional interpretation: (1) it provides quantitative versions of ordinary statements of mathematics; (2) it allows for the extraction of quantitative information, provided that the statements are proved in certain theories; (3) the theories may include certain nonconstructive principles, not necessarily set-theoretically correct. Some examples are given.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**January 18 | 4pm (Lisbon time)**

Bruno Jacinto (Universidade de Lisboa) and José Mestre (Stirling (SASP) and LanCog (Lisboa))

TITLE :: NeoRussellian Logicism

ABSTRACT ::

Russell argued for the logicist claim that arithmetic is reducible to logic on the basis of the derivability of the Peano axioms in his type-theoretic system. Unlike his logicist ally Frege, who conceived of numbers as individuals, Russell thought of them as attributes of attributes of individuals. As a result, Russell's brand of logicism faced a number of distinctive problems. Chief among these is that his derivation of the Peano axioms relies on the assumption that the domain of individuals is infinite. As critics have pointed out, this assumption does not constitute a logical law.

The aim of the present talk is to pave the way for a novel argument for the reducibility of arithmetic to logic. Departing from the Russellian view that numbers are attributes of attributes of individuals, a result will be presented to the effect that the axioms of Peano arithmetic are theorems of a modal and type-theoretic system committed solely to a potential infinity of individuals. In addition, we will examine the prospects of formulating and defending a novel form of logicism about arithmetic on the basis of this result.

LOCATION: Zoom Meeting:

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**January 11 | 4pm (Lisbon time)**

Ana Borges

University of Barcelona

TITLE :: Quantified Reflection Calculus with one modality

ABSTRACT ::

We present the logic QRC1, which is a strictly positive fragment of quantified modal logic. The intended reading of the diamond modality is that of consistency of a formal theory. Predicate symbols are interpreted as parametrized axiomatizations. QRC1 is sound with respect to this arithmetical interpretation. Quantified provability logic is known to be undecidable. However, the undecidability proof cannot be performed in our signature and arithmetical reading. We conjecture the logic QRC1 to be arithmetically complete. We takes the first steps towards arithmetical completeness by providing relational semantics for QRC1 with a corresponding completeness proof. We further show the finite model property with respect to domains and number of worlds, which implies decidability.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**DECEMBER 14 | 4pm (Lisbon time)**

Paulo Guilherme Santos

Departamento de Matemática – Universidade Nova de Lisboa

TITLE :: Arithmetical Numeral Completeness

ABSTRACT :: In this talk, we will present a form of completeness for numerals that holds for Peano Arithmetic. We will establish relationships between this result and a weak version of an initial form of Hilbert's Program .

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**DECEMBER 7 | 4pm (Lisbon time)**

**Ulrich Kohlenbach**

Department of Mathematics - Technische Universität Darmstadt

**TITLE** :: Some recent developments in proof mining

**ABSTRACT :: **

During the last two decades a systematic program of `proof mining' emerged as a new applied form of proof theory and has successfully been applied to a number of areas of core mathematics.

We are primarily concerned with the extraction of hidden finitary and combinatorial content from proofs that make use of infinitary noneffective principles. The main logical tools for this are so-called interpretations. Logical metatheorems based on such interpretations have been applied with particular success in the context of nonlinear analysis including fixed point theory, ergodic theory, continuous optimization, game theory and abstract Cauchy problems. The combinatorial content can manifest itself both in explicit effective bounds as well as uniformity results.

In this talk we will outline some recent new developments in proof mining and focus on the following points:

- tameness of bounds extracted,
- new qualitative results obtained as a byproduct of proof mining,
- mathematically enriched metastability results as finitizations of theorems going beyond mere convergence.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**30 ^{th} of November | 4pm (Lisbon time)**

Imme van den Berg

CIMA, Universidade de Évora

TITLE :: A nonstandard model for linear systems with uncertainties

ABSTRACT :: Uncertainties and imprecisions in measurement and calculation are modelled within nonstandard analysis. The approach is asymptotic, taking profit of the existence of infinitesimals and of a large hierarchy of orders of magnitude within the infinitesimals. We do not use groups of functions, like Oh’s and oh’s, but convex groups of real numbers, so-called (scalar) neutrices. They obey algebraic laws not unlike the laws of the real number system itself, modelling error propagation.

We study systems of linear equations, treating imprecisions individually by neutrices, both in the coefficients and the right-hand side. The algebraic laws are strong enough for defining the usual concepts of linear algebra and applying general solution methods, like Gauss-Jordan elimination and Cramer’s rule. Solution sets are intermediate between points and linear subspaces, based on neutrices with a well-defined higher dimension.

Joint work with Nam Van Tran, Ho Chi Min City University of Technology and Education, Vietnam, and Júlia Justino, Instituto Politécnico de Setubal.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**23 ^{rd} of November | 4pm (Lisbon time)**

Étienne Miquey

École Normale Supérieure de Lyon

TITLE :: A journey through Krivine realizability **(Part II)**

ABSTRACT :: Classical realizability is a theory born from Krivine's work, lying in between mathematical logic and theoretical computer science. Regarding the latter, Krivine realizability indeed defines a framework that has shown to be very conducive to unveiling the computational content of a wide range of classical proofs (going from arithmetical formulas to Cohen's forcing) while maintaining many benefits of intuitionistic realizability. On its logical side, it allows to define new models of set theory, providing for instance for a direct construction of a model in which neither the axiom of choice nor the continuum hypothesis hold.

These talks will be devoted to giving a comprehensive introduction to Krivine realizability and its applications. During the first one, I intend to focus on its definition and its core properties, trying to emphasize its peculiarities with respect to intuitionistic realizability. In particular, we shall focus on the computational interpretation it gives to classical proofs. If everything goes as planned, next week we will pay attention to several applications of Krivine realizability to logic and computer science.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**16 ^{th} of November | 4pm (Lisbon time)**

**Étienne Miquey**

**École Normale Supérieure de Lyon**

** **

**TITLE :: A journey through Krivine realizability**

**ABSTRACT ::** Classical realizability is a theory born from Krivine's work, lying in between mathematical logic and theoretical computer science. Regarding the latter, Krivine realizability indeed defines a framework that has shown to be very conducive to unveiling the computational content of a wide range of classical proofs (going from arithmetical formulas to Cohen's forcing) while maintaining many benefits of intuitionistic realizability. On its logical side, it allows to define new models of set theory, providing for instance for a direct construction of a model in which neither the axiom of choice nor the continuum hypothesis hold.

These talks will be devoted to giving a comprehensive introduction to Krivine realizability and its applications. During the first one, I intend to focus on its definition and its core properties, trying to emphasize its peculiarities with respect to intuitionistic realizability. In particular, we shall focus on the computational interpretation it gives to classical proofs. If everything goes as planned, next week we will pay attention to several applications of Krivine realizability to logic and computer science.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**9 ^{th} of November | 4pm (Lisbon time)**

**ANTÓNIO MARQUES FERNANDES**

Instituto Superior Técnico - Universidade de Lisboa

**TITLE :: What is Truth?**

**ABSTRACT** :: (There will be no abstract for this talk)

**LOCATION**: Zoom Meeting:

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**2 ^{nd} of November | 16:00 (Lisbon time)**

JAIME GASPAR

Centro de Matemática e Aplicações (CMA), FCT, UNL

TITLE :: Short introduction by example to Coq

ABSTRACT :: Proof assistants are computer programs that help mathematicians to prove theorems and to formally verify the correctness of proofs. Proof assistants are nowadays one of the more exciting areas in the intersection of mathematical logic and computer science. For example, one particularly exciting achievement is the formal verification of the proof of the four colour theorem using the proof assistant Coq.

In this talk we give a very elementary introduction to Coq by means of a very simple example: the proofs of the theorems

(1) if ≤ is a non-strict partial order, then < defined by x < y ↔ x ≤ y ∧ x ≠ y is a strict partial order;

(2) if < is a strict partial order, then ≤ defined by x ≤ y ↔ x < y ∨ x = y is a non-strict partial order.

Then we end by discussing what is achieved with this kind of formal verification. We keep this talk very short, simple and sweet.

LOCATION: Zoom Meeting:

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**26 ^{th} of October | 16:00 (Lisbon time)**

**PEDRO PINTO**

Technische Universitat Darmstadt

TITLE :: Quantitative translations for viscosity approximation methods

ABSTRACT :: Proof mining is a research program that employs proof theoretical tools to obtain additional information from mathematical results, [1].

Its techniques have been applied successfully to many areas of Mathematics with special focus on Nonlinear Analysis.

This presentation reports ongoing joint work with Ulrich Kohlenbach.

Two well-known strongly convergent algorithms in Fixed Point Theory are due to Browder and Halpern. Their original convergence results were generalized in several different ways.

First introduced by Moudafi, the viscosity approximation method is one such generalization in which the anchor point of the iteration is replaced with a strictly contracting

mapping. In [2], Suzuki showed that the convergence of the generalized viscosity version of these algorithms (with more general Meir-Keeler contractions) can be reduced

to the convergence of the original iterations.

Another extensively studied algorithm is the Krasnosel'skii-Mann iteration. This iteration has many useful properties (e.g. it is Fejér monotone), but in general is only

weakly convergent. A hybrid version of the Krasnosel'skii-Mann iteration with the viscosity method was recently studied in [3] and shown to be strongly convergent.

In this talk, we will discuss the quantitative analysis of these results. We start by recalling the relevant iterations and useful quantitative notions. We will point out

the main obstacles in the analysis of Suzuki's theorems, and explain how they were overcome to obtain rates of metastability and Cauchy rates.

Some applications of our results are given. In a second part, we discuss a certain notion of uniform accretive operators (discussed also in [3]), which allowed for an extraction

of a modulus of uniqueness in uniformly convex Banach spaces. It is well known that in this situation (together with a rate of asymptotic regularity) it is possible to

obtain Cauchy rates. We illustrate this with some applications. We conclude with some remarks regarding the additional generality of our work and its connection with the original results.

[1] Ulrich Kohlenbach. Applied Proof Theory: Proof Interpretations and their Use in Mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008.

[2] Tomonari Suzuki. Moudafi 's viscosity approximations with Meir-Keeler contractions. Journal of Mathematical Analysis and Applications, 325(1):342-352, 2007.

[3] Hong-Kun Xu, Najla Altwaijry and Souhail Chebbi. Strong convergence of Mann's iteration process in Banach spaces. Mathematics 2020, 8, 954; doi:10.3390/math8060954.

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**19 ^{th} of October | 16h00 (Lisbon time)**

https://videoconf-colibri.zoom.us/j/89084793299?pwd=amRYK3pwcFZDTnV5MHhYMDh3Ni9UQT09

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**CLARENCE PROTIN**

TITLE :: Bealer's Intensional Logic (Part II)

ABSTRACT :: Many intuitively valid arguments involving intensionality cannot be captured by first-order logic, even when extended by modal and epistemic operators.

Indeed, previous attempts at providing an adequate treatment of the phenomenon of intensionality in logic and language, such as those of Frege, Church, Russell, Carnap, Quine, Montague and others are fraught with numerous philosophical and technical difficulties and shortcomings.

We present Bealer's solution to this problem which hinges on an ontological commitment to theory of Properties, Propositions and Relations (PRP). At the most basic level we can distinguish two conceptions in the theory of PRPs. An objective one tied to modality and necessary equivalence, and a mental (intentional) one tied to concepts and the requirement of non-circularity in definitions. Building on the work of Russell, Church and Quine, Bealer proposes two distinct intensional logics T1 and T2 (presented in Hilbert form) corresponding to these two conceptions, both based on the language of first-order logic extended with an intensional abstraction operator.

In T1 necessitation can be directly defined and the axioms express S5 modal logic.

Both logics have a series of desirable features which set them apart from higher-order approaches.

Bealer constructs a non-Tarskian algebraic semantic framework, distinct from possible worlds semantics, yielding two classes of models for which T1 and T2 are both sound and complete.

Other features include being able to deal with quantifying-in, and the various substitution puzzles, being free from artificial type restrictions, having a Russellian semantics, satisfying Davidson's learnability requirement, etc.

Bealer unifies both logics to serve as a basis of a larger philosophical project in the tradition of logicism (or logical realism) as detailed in his book Quality and Concept (1982). This includes a neo-Fregean account of Arithmetic and Set Theory in which various purely logical (according to him) predication axioms (and intensional analogues of ZF, NGB, or Kelley-Morse axioms) are adjoined to T2, thereby explaining incompleteness as a property of pure logic rather than of mathematics.

Surprisingly, and rather ironically, Bealer's logic also fulfils Carnap's thesis of extensionality due precisely to its ontological commitment to the reality of PRPs.

In this series of two talks we will focus on the technical details of the proof of soundness and completeness of T1 and T2 and hint at some proof-theoretic and foundational developments.

**12 ^{th} of October | 16h00 (Lisbon time)**

Location: Zoom Meeting: https://videoconf-colibri.zoom.us/j/89247873078?pwd=QW1Ra0FTYWJCWTB4T3R0blZSdnJEZz09

Meeting ID: 892 4787 3078

Password: 268768

**CLARENCE PROTIN**

TITLE :: Bealer's Intensional Logic (Part I)

ABSTRACT :: Many intuitively valid arguments involving intensionality cannot be captured by first-order logic, even when extended by modal and epistemic operators.

Indeed, previous attempts at providing an adequate treatment of the phenomenon of intensionality in logic and language, such as those of Frege, Church, Russell, Carnap, Quine, Montague and others are fraught with numerous philosophical and technical difficulties and shortcomings.

We present Bealer's solution to this problem which hinges on an ontological commitment to theory of Properties, Propositions and Relations (PRP). At the most basic level we can distinguish two conceptions in the theory of PRPs. An objective one tied to modality and necessary equivalence, and a mental (intentional) one tied to concepts and the requirement of non-circularity in definitions. Building on the work of Russell, Church and Quine, Bealer proposes two distinct intensional logics T1 and T2 (presented in Hilbert form) corresponding to these two conceptions, both based on the language of first-order logic extended with an intensional abstraction operator.

In T1 necessitation can be directly defined and the axioms express S5 modal logic.

Both logics have a series of desirable features which set them apart from higher-order approaches.

Bealer constructs a non-Tarskian algebraic semantic framework, distinct from possible worlds semantics, yielding two classes of models for which T1 and T2 are both sound and complete.

Other features include being able to deal with quantifying-in, and the various substitution puzzles, being free from artificial type restrictions, having a Russellian semantics, satisfying Davidson's learnability requirement, etc.

Bealer unifies both logics to serve as a basis of a larger philosophical project in

the tradition of logicism (or logical realism) as detailed in his book Quality and Concept (1982). This includes a neo-Fregean account of Arithmetic and Set Theory in which various purely logical (according to him) predication axioms (and intensional analogues of ZF, NGB, or Kelley-Morse axioms) are adjoined to T2, thereby explaining incompleteness as a property of pure logic rather than of mathematics.

Surprisingly, and rather ironically, Bealer's logic also fulfils Carnap's thesis of extensionality due precisely to its ontological commitment to the reality of PRPs.

In this series of two talks we will focus on the technical details of the proof of

soundness and completeness of T1 and T2 and hint at some proof-theoretic and foundational developments.

**6 ^{th} of July** |

**16h00 (Lisbon time)**

Location: Zoom Meeting: https://videoconf-colibri.zoom.us/j/92351703489?pwd=Q245VmlJUitDVS9vZGJkSlJIc3BOUT09

Meeting ID: 923 5170 3489

Password: 251275

**ANDREI SIPOS **(TU Darmstadt & Institute of Mathematics of the Romanian Academy)

TITLE :: **Recent results in proof mining**

ABSTRACT :: We present some novel kinds of rates of metastability extracted from proofs in classical analysis and ergodic theory that we recently analyzed using proof mining techniques.