**Mathematical Logic Webinar **

**November 14 | Monday | 4:00 pm (Lisbon time)**

Alexander Meduna (Brno University of Technology)

TITLE :: Jumping finite automata

ABSTRACT :: This talk proposes a new investigation area in automata theory — *jumping finite automata*. These automata work like classical finite automata except that they read input words discontinuously — that is, after reading a symbol, they can jump over some symbols within the words and continue their computation from there. The talk gives several results concerning jumping finite automata in terms of commonly investigated areas of automata theory, such as closure properties. Most importantly, it achieves several results that demonstrate differences between jumping finite automata and classical finite automata. In its conclusion, the talk formulates several open problems and suggests future investigation areas.

Author:

Prof. Alexander Meduna (born 1957 in Olomouc, Czech Republic ) is a theoretical computer scientist and expert on compiler design, formal languages and automata. He is a professor of Computer Science at the Brno University of Technology. Formerly, he taught theoretical computer science at various European and American universities, including the University of Missouri, where he spent a decade teaching advanced topics of formal language theory. He wrote over ninety papers related to theoretical computer scientist.

His latest book is

Meduna, Alexander; Tomko, Martin, Horacek, Petr (2019).* Handbook of Mathematical Models for Languages and Computation.* The Institution of Engineering and Technology, Stevenage, UK, ISBN: 978-1-78561-660-0 https://www.amazon.ae/Handbook-Mathematical-Models-Languages-Computation/dp/1785616595

His previous books include

*Meduna, Alexander (2000). Automata and Languages: Theory and Applications.**Springer Science & Business Media.**ISBN**9781852330743**.**Meduna, Alexander (2007). Elements of Compiler Design.**CRC Press.**ISBN**9781420063233**.**Meduna, Alexander (2014). Formal Languages and Computation: Models and Their Applications.**CRC Press.**ISBN**9781466513457**.**Meduna, Alexander; Švec, Martin (2005). Grammars with Context Conditions and Their Applications.**John Wiley & Sons.**ISBN**9780471736554**.**Meduna, Alexander; Techet, Jiří (2010). Scattered Context Grammars and Their Applications.**WIT Press.**ISBN**9781845644260**.**Meduna, Alexander; Zemek, Petr (2014). Regulated Grammars and Automata.**Springer.**ISBN**9781493903696**.**Meduna, Alexander; Soukup, Ondřej (2017). Modern Language Models and Computation: Theory with Applications.**Springer.**ISBN**9783319630991**.*

LOCATION: **Departamento de Matemática do Instituto Superior Técnico ULisboa, Room 3.10**

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**This is a joint session with IST**

**November 11 | Friday | 4:00 pm ****(Lisbon time)**

Emanuele Frittaion (University of Leeds)

TITLE :: Iterating reflection over Heyting Arithmetic.

ABSTRACT :: We will recall Turing and Feferman's work on iterations of reflection principles over Peano Arithmetic. The main result here, due to Feferman, is that every true sentence of arithmetic can be proved in some "transfinite recursive iteration" of uniform reflection over Peano Arithmetic. We will then see what happens in the case of Heyting Arithmetic. Spoiler alert: Feferman's completeness result, as expected, fails in the intuitionistic case.

LOCATION: **ONLINE**

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**November 4 | Friday | 4:00 pm ****(Lisbon time)**

Maria Osório (Universidade de Lisboa)

TITLE :: Decidability of the Presburger Arithmetic

ABSTRACT :: The main goal of this work is to prove that the Presburger Arithmetic is decidable. This theory is simpler than Peano's Arithmetic (PA) since it does not have multiplication, however, it enjoys properties that PA does not. We look at three theories of the Natural numbers, each more complex than the last one, and prove several properties, the main one being decidability. We build quantifier elimination procedures which, beyond the interest of proving the theories enjoy quantifier elimination themselves, allow us to prove the theories are decidable.

Our approach follows mainly Endertons's *A Mathematical Introduction to Logic*.

This work was done under the supervision of Professor Mário Edmundo and was part of my Master's degree.

LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**October 28 | Friday | 4:00 pm ****(Lisbon time)**

Pedro Pinto (Technische Universitat Darmstadt)

TITLE :: Proof mining on PDE theory

ABSTRACT :: Proof mining is the research program that employs proof-theoretical techniques to obtain new information from noneffective mathematical theorems [1]. Such new information may be of a quantitative nature (like rates of convergence, etc.) or of a qualitative nature (generalizations, independence on parameters, etc.). With the work of U. Kohlenbach and his collaborators, in the last 25 years this program has been successfully applied in a systematic way to various areas of mathematics, specially in the field of nonlinear analysis. However, at the moment there is a single study of results in the context of PDE theory [2]. Recent developments regarding a suitable formalization of monotone (accretive) set-valued maps in Hilbert (Banach) spaces due to N. Pischke [3] have allowed for a clear formal understanding of these types of maps and opened up proof mining to applications on a new class of results.

In this talk, we will discuss the asymptotic behavior of nonlinear semigroups generated by an accretive operator through the proof mining study of results due to O. Nevanlinna and S. Reich [4] as well as H.-K. Xu [5]. These results consider a particularly interesting condition on the underlying operator introduced by A. Pazy [6] under the name of ‘convergence condition’. We derive various notions of a ‘convergence condition with modulus’ which provide quantitative information on this condition of a varying computational strength. These notions then allow for the extraction of quantitative information on the convergence results of Nevanlinna and Reich as well as Xu in the form of rates of convergence. This talk is based on ongoing joint work [7] with Nicholas Pischke.

References:

[1] U. Kohlenbach, Applied proof theory: proof interpretations and their use in mathematics. Springer Monographs in Mathematics. Springer-Verlag Berlin Heidelberg, 2008.

[2] U. Kohlenbach, and A. Koutsoukou-Argyraki, Rates of convergence and metastability for abstract Cauchy problems generated by accretive operators, Journal of Mathematical Analysis and Applications, 423:10891112, 2015.

[3] N. Pischke, Logical Metatheorems for Accretive and (Generalized) Monotone Set-Valued Operators, Submitted, arXiv:2205.01788, 2022.

[4] O. Nevanlinna and S. Reich, Strong convergence of contraction semigroups and of iterative methods for accretive operators in Banach spaces, Israel Journal of Mathematics, 32:4458, 1979.

[5] H.-K. Xu, Strong asymptotic behavior of almost-orbits of nonlinear semigroups, Nonlinear Analysis: Theory, Methods & Applications, 46(1):135151, 2001.

[6] A. Pazy, Strong convergence of semigroups on nonlinear contractions in Hilbert space, Journal of Mathematical Analysis and Applications, 34:135, 1978.

[7] P. Pinto and N. Pischke, On the asymptotic behavior of Cauchy problems generated by an accretive operator, 2022.

LOCATION: **ONLINE**

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**October 21 | Friday | 4:00 pm ****(Lisbon time)**

Bruno Loff (Universidade do Porto)

TITLE :: Why is solving the P vs NP problem so damn hard?

ABSTRACT :: I will give a board-and-chalk-and-informal-talk presentation about the difficulty of proving lower-bounds in computational complexity.

The P vs NP problem is one of the most famous unsolved problems in mathematics. One may phrase the P vs NP question in various equivalent ways. One way, which is not completely equivalent, but almost, is the following ("P/poly vs NP problem"). Does there exist a small Boolean circuit which solves the CLIQUE problem? I.e., does there exist a poly(N)-size Boolean circuit which, when given as input the NxN adjacency matrix of an undirected graph, decides whether the graph has a clique of size N/2?

Complexity theorists, me included, believe that the answer is no. We believe that there exists a super-polynomial "lower-bound" on the complexity of CLIQUE. Many people have tried proving such a lower-bound, and so far all have failed. But why? Why is the problem so difficult?

In the late 1980s, Alexander Razborov proved that there exist no poly(N)-size "monotone" circuits for solving CLIQUE. Namely, if we forbid the Boolean circuit from doing negations, so they can only do ORs and ANDs, then polysize circuits cannot solve the CLIQUE problem. He (and many others) then tried to prove the same result for ordinary circuits (with negation gates). And he failed (and they all failed, too). But along the way he (and many others) proved many different lower-bounds. Lower-bounds for simpler kinds of circuits (e.g. constant-depth), lower-bounds for communication protocols (a different but related computational model), and lower-bounds for other models. Razborov proved these lower-bounds, and he also thought long and hard about why lower-bounds against Boolean circuits were so difficult to prove.

In 1994, Razborov and Stephen Rudich presented their paper, "natural proofs", which had a very reasonable explanation for why circuit lower-bounds were difficult to prove. They showed, remarkably, that every single lower-bound proof that was known at the time had a certain "logical structure" (or could be made to have such a structure by small changes to the argument). This logical structure made the proof very simple and natural, and they called proofs with such a structure "natural proofs". Then they showed that super-polynomial lower-bounds on CLIQUE cannot be shown using natural proofs, unless certain cryptographic primitives, such as factoring, are unsecure. This is a kind of informal independence result. (Based on the natural proofs result, Razborov also later proved formal independence results, showing that P vs NP is independent of certain weak systems of arithmetic, but I do now know the details of those.)

In one fell swoop, Razborov and Rudich ruled out every single lower-bound technique known at the time, saying: these techniques are not enough to solve the P vs NP problem (unless cryptography is insecure). To a very large extent this barrier still applies today, as almost all the lower-bound proofs that we know are natural proofs, i.e., they have the very same logical structure as the proofs known since the 1980s.

In this seminar, I will explain what is a "natural proof", and why it is reasonable to expect that no natural proof can solve the P vs NP problem. Only a few words will be said about some of my research and how it connects to this topic.

LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**October 14 | Friday | 4:00 pm ****(Lisbon time)**

Fernando Ferreira (Universidade de Lisboa)

TITLE :: The abstract type of the real numbers

ABSTRACT :: This talk has two parts. In the first part, we discuss how the bounded functional interpretation can be seen as a partial realization of Hilbert’s program (extending the well-known conservation result of Harvey Friedman in reverse mathematics). We give two mathematical applications of this extension. We also remark that this extension can contribute to the scholarly discussions of Hillbert’s program. In the second part, we show how the bounded functional interpretation can provide an abstract type for the real numbers. We do not know if such abstract type can be obtained when based on Gödel's dialectica interpretation.

LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**May 25 | Wednesday | 4:00 pm ****(Lisbon time)**

Clarence Protin

TITLE :: A Constructive Proof of the Univalence Axiom (Part II)

ABSTRACT :: The homotopy type theory/univalent foundations program aims at providing a type theory for proof assistants and proof

checkers suitable for formalising mathematics and in particular homotopy theory.

The original version of homotopy type theory/univalent foundations is based on dependent type theory

to which are added axioms for function extensionality and univalence. The basic idea is that concepts of homotopy theory are applied

to the treatment of equality types. Roughly speaking, the univalence axiom

gives formal justification for the standard mathematical practice of "identifying isomorphic structures."

Voevodsky gave a model of homotopy type theory based on simplicial sets. However this model made essential use of classical logic.

Furthermore in the original version univalence is introduced via a postulated constant with no computational interpretation.

Since the constructive nature of type theories is a major philosophical and practical advantage an important task in subsequent research

has been to give a computational interpretation to the axioms and to find a constructive model.

Since the first cubical set model was proposed around 2014 by Bezem and Coquand required additional operations on cubical sets (such as Kan operations and contraction) have been brought to light as well as the necessity of extending the original syntax of homotopy type theory with new constructors to express these operations. Such systems are called cubical type theories. The most promising

model has been the cubical set model presented in the paper of Cohen, Coquand, Huber and Mörtberg (2018) which is based on free De Morgan algebras over names. In the associated cubical type theory function extensionality and the univalence axiom actually become theorems.

In these talks we give a leisurely elementary introduction to the syntactical aspects of cubical type theory as found in the paper of Cohen et al. and present in detail the proof of the univalence axiom using Glue types. We also attempt to explain some of the geometric and topological intuitions behind the use of De Morgan algebras over names. Our presentation does not require any background in category theory or homotopy theory, only some acquaintance with natural deduction and type theory. Finally we touch briefly upon some ideas for actual implementations of cubical type theory which might address some of the efficiency problems.

LOCATION:: online

Online broadcast:

https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**May 18 | Wednesday | 4:00 pm ****(Lisbon time)**

Clarence Protin

TITLE :: A Constructive Proof of the Univalence Axiom

ABSTRACT :: The homotopy type theory/univalent foundations program aims at providing a type theory for proof assistants and proof

checkers suitable for formalising mathematics and in particular homotopy theory.

The original version of homotopy type theory/univalent foundations is based on dependent type theory to which are added axioms for function extensionality and univalence. The basic idea is that concepts of homotopy theory are applied to the treatment of equality types. Roughly speaking, the univalence axiom gives formal justification for the standard mathematical practice of "identifying isomorphic structures."

Voevodsky gave a model of homotopy type theory based on simplicial sets. However this model made essential use of classical logic.

Furthermore in the original version univalence is introduced via a postulated constant with no computational interpretation.

Since the constructive nature of type theories is a major philosophical and practical advantage an important task in subsequent research has been to give a computational interpretation to the axioms and to find a constructive model.

Since the first cubical set model was proposed around 2014 by Bezem and Coquand required additional operations on cubical sets (such as Kan operations and contraction) have been brought to light as well as the necessity of extending the original syntax of homotopy type theory with new constructors to express these operations. Such systems are called cubical type theories. The most promising model has been the cubical set model presented in the paper of Cohen, Coquand, Huber and Mörtberg (2018) which is based on free De Morgan algebras over names. In the associated cubical type theory function extensionality and the univalence axiom actually become theorems.

In these talks we give a leisurely elementary introduction to the syntactical aspects of cubical type theory as found in the paper of Cohen et al. and present in detail the proof of the univalence axiom using Glue types. We also attempt to explain some of the geometric and topological intuitions behind the use of De Morgan algebras over names. Our presentation does not require any background in category theory or homotopy theory, only some acquaintance with natural deduction and type theory. Finally we touch briefly upon some ideas for actual implementations of cubical type theory which might address some of the efficiency problems.

LOCATION:: ONLINE

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**May 11 | Wednesday | 4:00 pm ****(Lisbon time)**

Giuseppina Terzo (Universidade de Nápoles)

TITLE :: Exponential Ideals in exponential polynomial rings

ABSTRACT ::

When we work with exponential polynomial rings over an exponential field some classical results fail, as Hilbert’s Basis Theorem and Nullstellensatz.

We investigate E-maximal ideals and E-prime ideals, in order to see if some weak version of Nullstellensatz holds. There exist E-maximal ideals not of the form (x_1 – a_1, …. ,x_n -a_n) and this gives information on Nullstellensatz. Moreover we give conditions to be E-prime ideals and we prove that there are no relations between the notion of E-maximal ideals and E-prime ideals as was for rings.

LOCATION:: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**April 27 | Wednesday | 4:00 pm **

**(Lisbon time)**

Luiz Carlos Pereira (PUC-Rio)

TITLE :: Disjunctive Syllogism without *Ex falso*

ABSTRACT :: See attachment.

LOCATION:: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**March 28 | Monday | 4:00 pm (Lisbon time)**

Trifon Trifonov (Sofia University)

TITLE :: Modal Functional (Dialectica) Interpretation

ABSTRACT :: Gödel's functional (Dialectica) interpretation is a powerful tool for obtaining computations from proofs involving non-constructive principles. Practical uses necessitate control mechanisms for the complexity of the extracted terms.

We show how Dialectica can be soundly adapted to interpret a non-standard modal arithmetic extending system T and S4 into classical finite type arithmetic. The modalities act as erasers of irrelevant code "en masse", complementary to the finer mechanism of light quantifiers providing erasure of individual variables. The realizability of the defining axiom of the classical modal system S5 is shown to be equivalent to the Drinker's Paradox.

This is joint research with Dan Hernest.

LOCATION: **ONLINE**

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**March 21 | Monday | 4:00 pm (Lisbon time)**

Marie Kerjean (LIPN – Université Paris 13)

TITLE :: δ is for Dialectica

ABSTRACT :: Differential Linear Logic is an extension of Linear Logic allowing for the linearization of proofs. It was introduced by Ehrhard and Regnier 20 years ago. Its denotational models corresponds to the differentiation of higher-order functions in functional analysis, and it has led to differential extensions of lambda-calculus and categorical models of linear logic.

Dialectica is a proof transformation introduced by Gödel acting of intuitionistic logic which factors through Girard's translation, allowing the realization of several semi classical axioms such as Markov's principle.

By taking the viewpoint of differential lambda-calculus and recent developments in differentiable programming, we will show how Dialectica computes higher-order backward differentiation. We will illustrate this through the lens of categories, types and lambda-terms. This is joint work with Pierre-Marie Pédrot.

LOCATION: **ONLINE**

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**March 14 | Monday | 4:00 pm (Lisbon time)**

Luís Caires (NOVA Laboratory for Computer Science and Informatics)

TITLE :: Propositions-as-Types and Stateful Computation

ABSTRACT :: Propositions-as-types (PaT) goes back to the functional interpretation

of intuitionistic logic due to Brouwer, Heyting and Kolmogorov, but was brought under the spotlight only after the famous notes of Curry and Howard. It has been since then considered both an intriguing and prolific concept, with many instances and consequences in logic and the foundations of programming languages.

In 2010 we have (with Pfenning) developed for the first time a PaT interpretation of linear logic which yields an expressive session-based programming language, while ensuring ("for-free") progress (deadlock-freedom), confluence, and normalisation as a consequence of the correspondence between computation and proof reduction. In this talk, we review this line of work and glimpse at some recent developments (with Rocha) on PaT and shared state.

LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

This is a joint session with SAL (CMA/FCT-UNL)

**March 7 | Monday | 4:00 pm (Lisbon time)**

Diana Costa (Universidade de Lisboa)

TITLE :: A journey through 4-valued Modal and Hybrid Logics

ABSTRACT :: In this talk I will present Modal Logic and its extension to Hybrid Logic, in their classical formulation. Then, I will introduce 4-valued versions of each of them: I will start with an overview of 4-valued Modal Logics in literature, and I will explain why do I think neither of them captures the real meaning of modal operators. From there, I will introduce you to 4-valued Hybrid Logic, where modal operators are not dual.

LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**February 21 | Monday | 4:00 pm (Lisbon time)**

Melissa Antonelli (University of Bologna)

TITLE :: ON LOGIC AND RANDOMIZED COMPUTATION

ABSTRACT :: Interactions between logic and theoretical computer science have been deeply investigated in the realm of deterministic computation but, strikingly, when switching to the probabilistic framework, the literature does not offer much. The main goal of our study is precisely to start bridging this gap by developing inherently quantitative logics and investigating their relations with specific aspects of randomized models. This talk is conceived as an overview of our work (in particular, of ongoing research) and is bipartite. In the first part, I will introduce our quantitative counting propositional logics, which are basically obtained by endowing standard propositional systems with counting quantifiers, expressing the probability of the (argument) formula. I will show that the classical fragment, CPL, is strongly linked to complexity theory, as characterizing the full counting hierarchy. On the other hand, in the context of programming language theory, the intuitionistic counting logic, iCPL_0, provides the first probabilistic correspondence in the style of Curry and Howard In the second part of the talk, I will introduce the more expressive logic MQPA, the language of which is defined by extending that of PA with measure-quantifiers. This logic is strongly connected to probabilistic computation, as shown by some results, such as “randomized arithmetization”. Starting from this, we are also developing randomized bounded theories, in order to logically characterize probabilistic complexity classes, following the path delineated by Buss’ and Ferreira’s bounded arithmetics. (Part of this work, which is still in progress, has been conducted during my visiting period at NOVA University.)

LOCATION: **Online **

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**February 14 | Monday | 4pm (Lisbon time)**

Nicholas Pischke (TU Darmstadt)

TITLE :: Bound extraction theorems for proofs involving monotone operators

ABSTRACT :: I show how proofs involving set-valued maximally monotone operators on inner product spaces can be treated in suitable higher-order logical systems which admit proof-theoretic metatheorems that allows for the extraction of computational content. I outline how the basic theory of these operators can be formally developed, how extensionality of a set-valued operator is characterized by maximality and related concepts and what kind of metatheorems can be derived using those systems. Lastly, I discuss how extensions of these systems motivated by mathematical practice can be developed in this context and how they are necessary for a recent application of the metatheorems.

LOCATION: **Online **

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**February 7 | Monday | 4pm (Lisbon time)**

Thomas Powell (University of Bath)

TITLE :: A proof theoretic analysis of Littlewood’s Tauberian theorems

ABSTRACT :: I present an overview of recent work on applying proof theoretic methods in Tauberian theory. The main result is a quantitative version of Littlewood’s celebrated Tauberian theorem from 1911, obtained using Goedel’s Dialectica interpretation. As a corollary of this, we obtain a rederivation of a so-called “remainder estimate” for Littlewood’s theorem and are moreover able to generalise it. I conclude by looking ahead to potential future directions of research in this direction.

LOCATION: **Online (Please notice the new link!)**

Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971

Meeting ID: 837 8989 1971

**January 31 | Monday | 4pm (Lisbon time)**

Luca Tranchini (University of Tubingen)

TITLE :: The Yoneda Reduction of Polymorphic Types (joint work with Paolo Pistone)

ABSTRACT :: In this talk I will present a family of type isomorphisms in System F (i.e. second-order propositional intuitionistic logic) whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under notions of identity of proofs (or programs) stronger than the one induced by βη-equivalence, like those induced by parametricity and dinaturality. We show that the Yoneda type isomorphisms yield a rewriting over types (i.e. formulas), that we call Yoneda reduction, which can be used to eliminate quantifiers from a polymorphic type, replacing them with a combination of monomorphic type constructors. We establish some sufficient conditions under which quantifiers can be fully eliminated from a polymorphic type, and we show some application of these conditions to count the inhabitants of a type and to study proof/program equivalence in some fragments of System F.

LOCATION: **ONLINE**

Online broadcast:

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**This is a joint session with SAL (CMA/FCT-UNL)**

**January 24 | Monday | 4pm (Lisbon time)**

Paolo Pistone (Università di Bologna)

TITLE :: Towards Logical Foundations for Randomized Computability

(joint work with Melissa Antonelli and Ugo Dal Lago)

ABSTRACT :: The interactions between logic and the theory of computation are plentiful and deep. On the one side, proof systems can be used to prove termination of certain classes of algorithms, or to establish complexity bounds. On the other side, higher-order programming languages, such as typed lambda-calculi, can be proved to capture the computational content of proofs.

However, there is one side of the theory of computation which was only marginally touched by this fruitful interaction, that is, randomized computation.

In this talk we introduce a family of logical systems based on a new class of counting quantifiers, assessing the extent to which one formula is true. We show that these logics provide ways to characterize some probabilistic complexity classes and to define a Curry-Howard correspondence for randomized computation.

LOCATION: **ONLINE**

Online broadcast:

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**January 17 | Monday | 4pm (Lisbon time)**

Guilherme Velez (Faculdade de Ciências da Universidade de Lisboa)

TITLE :: Introduction to Model Theory and its relation to Algebraic Geometry

ABSTRACT :: This presentation consists in a brief introduction to Model Theory and some important results regarding quantifier elimination, model-completeness and the theory of algebraically closed fields, which will then be used, together with some purely algebraic facts, to prove Hilbert’s Nullstellensatz, a fundamental theorem in Algebraic Geometry. I will also establish the relationship between definable sets (a model-theoretic object) and constructible sets (an algebraic & geometric object).

LOCATION: **ONLINE**

Online broadcast:

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**January 10 | Monday | 4pm (Lisbon time)**

Pedro Pinto (Technische Universität Darmstadt)

TITLE :: Halpern and Mann iterative schemas: A path towards generalization

ABSTRACT ::

In this talk I shall discuss recent joint work with Bruno Dinis, where we considered an iterative schema which alternates between Halpern and Krasnoselskii-Mann style iterations.

We prove, under suitable conditions, the strong convergence of this algorithm in the general nonlinear setting of CAT(0) spaces. Besides obtaining quantitative information, we will see how such proof was made possible by techniques and ideas from the proof mining program.

Our results generalize recent work by Boț, Csetnek and Meier, and Cheval and Leustean.

__References:__

[1] B. Dinis and P. Pinto. Strong convergence for the alternating Halpern-Mann iteration in CAT(0) spaces. arXiv:2112.14525, 2021.

[2] R. I. Bot, E. R. Csetnek, and D. Meier. Inducing strong convergence into the asymptotic behaviour of proximal splitting algorithms in Hilbert spaces. Optim. Methods Softw., 34(3):489{514, 2019.

[3] H. Cheval and L. Leuștean. Quadratic rates of asymptotic regularity for the Tikhonov-Mann iteration. arXiv:2107.07176, 2021.

[4] F. Ferreira, L. Leuștean, and P. Pinto. On the removal of weak compactness arguments in proof mining. Advances in Mathematics, 354:106728, 2019

[5] U. Kohlenbach and L. Leuștean. Effective metastability of Halpern iterates in CAT(0) spaces. Advances in Mathematics, 231(5):2526{2556, 2012.

LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33

Online broadcast:

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**December 13 | Monday | 4pm (Lisbon time)**

Paulo Santos

Universidade Nova de Lisboa (CMA)

TITLE :: Numeral completeness of S^1_2: Part B

ABSTRACT ::

We establish several consequences of numeral completeness, namely on: a computational version of Kreisel’s conjecture, finitist consistency, and a negative result on the size of proofs of consistency for bounded notions of provability.

LOCATION: **Faculdade de Ciências da Universidade de Lisboa, room C6.2.33 + ****ONLINE**

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**December 6 | 4pm | 6.2.33 + ONLINE**

Paulo Santos, Universidade Nova de Lisboa (CMA)

TITLE :: Numeral completeness of S^1_2: Part A

ABSTRACT ::

We prove numeral forms of completeness and consistency for S^1_2 and EA. We explore the derivability conditions needed to establish our result and present a weak form of G2 without using ``provability implies provable provability''. We present characterizations of the provability predicates for which our numeral results hold, having EA as the surrounding theory, and consequences of our results to the study of reflection principles and truth.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**November 29 | 4pm | 6.2.33 + ONLINE **

José Mestre, Stirling/St Andrews and LanCog (CFUL)

TITLE :: The role of functions in Frege’s *lingua characterica*

ABSTRACT ::

In Begriffsschrift, Frege set out to formulate a language powerful enough to express every mathematical thought. Central to this undertaking was his introduction of the notion of a function. It was this notion that underpinned not only his invention of the quantifier-variable notation but also a kind of synthesis of earlier traditions in logic. Calling it a ‘synthesis’, however, may be misleading. In this talk, I argue that an adequate understanding of the role functions had to play for Frege shows that, in one relevant sense of ‘property’, the values of higher-order variables cannot be properties in his system.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**November 22 | 4pm | 6.2.33 + ONLINE **

**Frege’s Begriffsschrift and second-order logic**

Joan San-Millán (Centro de Filosofia das Ciências da Universidade de Lisboa)

**Abstract: **

In Begriffsschrift, Frege presented a logical system and used it to formulate logical definitions of arithmetical notions and to deduce some noteworthy theorems by means of logical axioms and inference rules. It is often assumed that all derivations in this work — despite some oddities that should be corrected — can be reproduced in a second-order formal system.

In this talk, I argue that the deductive system of Begriffsschrift must not be reconstructed as a second-order calculus. An analysis of the nature of its language, logical axioms and inference rules leads me to argue that Begriffsschrift’s deductions do not need any correction but, on the contrary, can be explained in coherence with a global reading of this work.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**November 15 | 4pm | ONLINE**

**On proper direct image in o-minimal expansions of groups**

Mário Emundo (Faculdade de Ciências, CMAFcIO, Universidade de Lisboa)

**Abstract: **

(Work in progress with L. Prelli (U. Padova)). We show that the formalism of the six Grothendieck operations holds in the sub-category of definably locally closed definable subsets equipped with the o-minimal site in o-minimal expansions of ordered groups.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**November 8 | 4pm | ONLINE**

**Decidability of Logical Theories and their Combination**

João Rasga and Cristina Sernadas (Instituto Superior Técnico, Universidade de Lisboa e Instituto de Telecomunicações)

**Abstract: **

Talk related with the recent book with the same title, published in Studies in Universal Logic (SUL), Birkhäuser, Basel, Switzerland.

This book provides a comprehensive, self-contained introduction to decidability of first-order theories, using detailed proofs and examples to illustrate and clarify complex concepts. It incorporates computability theory and reduction techniques to determine the decidability of theories. It illustrates a variety of ways to deduce logical consequences from a theory, including the use of Gentzen calculus for first-order logic

https://link.springer.com/book/10.1007%2F978-3-030-56554-1

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**October 25 | 4pm | 6.2.33 **

**A Theory of Marginal and Large Difference**

Bruno Jacinto (Universidade de Lisboa)

**Abstract: **

In this talk we propose a new theory of vagueness based on the notions of marginal and large difference, and show that the theory has natural models in the context of nonstandard mathematics. In addition, we present a representation theorem establishing that, given tame conditions, the structure of marginal and large difference is representable in nonstandard models of arithmetic. We also present a uniqueness theorem establishing to what extent such a representation is unique. Finally, we apply our theory of marginal and large difference to an account of the meaning of vague adjectives, and to an explanation of the seductiveness of the Sorites paradox, by coupling it with Fara's interest-relative theory of vagueness.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**This is a joint session with SAL (CMA/FCT-UNL)**

**May 31 | Monday | 4pm ****(Lisbon time)**

** **

Luís Cruz-Filipe (Department of Mathematics and Computer Science, University of Southern Denmark)

TITLE :: Can computers prove theorems?

ABSTRACT ::

The proof of the four-color theorem in 1976 is usually referenced as the birth of computer-assisted mathematical proofs, although some earlier examples exist. Since then, computers have slowly started working their way into mathematicians' toolboxes; and the relevance of computers for mathematical proofs was confirmed with the inclusion of a panel discussion on the topic at ICM 2018.

In this talk we discuss the logical foundations of computer proofs and what it means to say that a theorem has been proved with the help of a computer. We cover some recent examples from combinatorics and number theory, and discuss ongoing work around the topic of session types.

LOCATION:

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**This is a joint session with SAL (CMA/FCT-UNL)**

**May 24 | Monday | 4pm ****(Lisbon time)**

** **

Charles Morgan (UCL)

TITLE :: The Ultrafilter Spectrum

ABSTRACT ::

The ultrafilter spectrum for a given cardinal $\kappa$ is the collection of possible sizes of bases for ultrafilters on $\kappa$. The talk will introduce the problem of what one can say about the ultrafilter spectrum and consider older and some more recent results addressing this question. Along the way the current state of set theory will be briefly be discussed, with questions about the ultrafilter spectrum serving as illustrations of some strands of interests.

Very little technical set theoretic knowledge should be necessary for the large bulk of the talk.

LOCATION: Zoom Meeting:

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**May 10 | Monday | 4pm ****(Lisbon time)**

** **

Luís Pinto (Centro de Matemática - Universidade do Minho)

TITLE :: Coinductive proof search for intuitionistic propositional logic

ABSTRACT :: The coinductive approach to proof search we present is based on three main ideas: (i) the Curry-Howard paradigm of representation of proofs

(by typed lambda-terms) is extended to solutions of proof-search problems (a solution is a run of the proof search process that does not

fail to apply bottom-up an inference rule, so it may be an infinite object); (ii) two typed lambda-calculi, one obtained by a coinductive

reading of the grammar of proof terms (acting as the universe for the mathematical definition of proof search concepts), the other by

enriching the grammar of proof terms with a formal fixed-point operator to represent cyclic behaviour (acting as the finitary setting where

algorithmic counterparts of those concepts can be found); (iii) formal (finite) sums are employed throughout to represent choice points, so not

only solutions but even entire solution spaces are represented, both coinductively and finitarily.

In this seminar we will illustrate this approach for intuitionistic implication, including applications to inhabitation and counting

problems in simply-typed lambda-calculus (e. g., results ensuring uniqueness of inhabitants related to coherence in category theory), and

briefly overview recent developments on the extension of the approach to polarized intuitionistic logic, which allows to obtain results about

proof search for full intuitionistic propositional logic.

This seminar is based on joint work with José Espírito Santo (CMAT, Univ. Minho) and Ralph Matthes (IRIT, CNRS and Univ. Toulouse III, France).

LOCATION: Zoom Meeting:

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**May 3 | Monday | 4pm ****(Lisbon time)**

** **

José Espírito Santo (Centro de Matemática - Universidade do Minho)

TITLE :: Polarized natural deduction

ABSTRACT :: In the context of polarized, intuitionistic propositional logic, starting from a fairly standard focused sequent calculus, a bidirectional natural deduction system is derived by an equally standard process. The result is a very disciplined and interesting syntax: the subformula property holds, polarity decides the style of the elimination rules, there are no commutative conversions, and even atomic formulas have introduction, elimination and normalization rules. In the corresponding polarized lambda-calculus, reduction follows a paradigm that subsumes both call-by-name and call-by-value.

LOCATION: Zoom Meeting:

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**April 26 | Monday | 4pm ****(Lisbon time)**

** **

Melissa Antonelli (University of Bologna)

TITLE :: On measure quantified logics

ABSTRACT :: Interactions between logics and theoretical computer science are numerous and deep. As it is well-known, the development of deterministic computational models has considerably benefitted from these mutual interchanges. There is, however, one aspect of the theory of computation which has only marginally been touched by such a back and forth interaction, namely randomized computation. This is becoming more and more evident, due to the increasing pervasiveness of probabilistic models in several areas of computer science. The aim of our study is to start bridging this gap by introducing a logical counterpart to certain aspects of randomized computation, therefore generalizing standard achievements to the probabilistic setting. All the results I am going to present are part of a joint work with Ugo Dal Lago and Paolo Pistone.

We will start by exploring counting propositional logic, which extends standard PL by means of counting quantifiers. We will first describe the simplistic fragment, CPL0, in which counting quantification is nameless, then move to its multivariate (actually non-conservative) generalization, CPL. Some interactions between these logics and theoretical computer science will be sketched. For example, thanks to CPL, we are able to give a logical characterization of the Counting Hierarchy (in the spirit of Meyer and Stockmeyer's work on QPL and PH), and to establish a correspondence with probabilistic lambda-calculi in the style of the Curry-Howard one.

We will conclude the presentation by briefly describing the more powerful MQPA, a generalization of CPL obtained by endowing the language of first-order arithmetic with second-order measure quantifiers. This logic is capable of expressing arithmetical formulas, dealing with probabilistic choices, and of formalizing basic results from probability theory. In our opinion, this system may constitute a logical counterpart to randomized computation, in the same way as Peano Arithmetic corresponds to deterministic computation.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**This is a joint session with SAL (CMA/FCT-UNL)**

**April 19 | Monday | 4pm ****(Lisbon time)**

** **

Benedict Eastaugh (Munich Center for Mathematical Philosophy-LMU)

TITLE :: Recursive counterexamples, reversals, and the foundational standpoint

ABSTRACT :: Many classical mathematical theorems are computably false: there are “recursive counterexamples” which satisfy their hypotheses but not their conclusions. This is often taken to show that these theorems are constructively unprovable. However, the theoretical standpoint from which recursive counterexamples are defined embeds assumptions that constructivists do not accept. These impossibility results are thus meaningless or invalid from their perspective. In this talk I will argue that reverse mathematics provides a way to internalise recursive counterexamples in weak formal systems acceptable to a range of broadly constructive foundational viewpoints. Although it cannot completely bridge the classical and foundational standpoints, this approach nevertheless brings them closer together.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**April 12 | Monday | 4pm (Lisbon time)**

** **

Anton Freund (Technische Universitat Darmstadt)

TITLE :: Patterns of resemblance - between proof theory and set theory

ABSTRACT :: Timothy Carlson's patterns of resemblance offer an astonishingly simple way to describe large computable ordinals, as used in proof theory.

In this talk I discuss fundamental definitions and results, without assuming any prerequisites from proof theory. My aim is to explain the following recent theorem: By relativizing patterns of resemblance to dilators, one obtains an equivalence with Pi^1_1-comprehension, a central principle from reverse mathematics (arXiv:2012.10292).

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

**March 22 | Monday | 4pm (Lisbon time)**

** **

Walter Dean (Department of Philosophy - University of Warwick)

TITLE :: The liar and the sorites: Towards a uniform arithmetical treatment

ABSTRACT :: The unification of the paradoxes of truth and vagueness has been a topic of recurrent philosophical interest (e.g. McGee 1990, Tappenden 1993, Field 2003/2008). I will present a sequence of observations which illustrate how the liar and sorites paradoxes are formally related, culminating in the claim that they give rise to similar sorts of mathematical incompleteness phenomena. A central tool will be the use of the arithmetized completeness theorem to provide interpretations of putatively paradoxical notions within the language of first-order arithmetic.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

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

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.

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.

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.