Mathematical Logic Webinar

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

Meeting ID: 837 8989 1971

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

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.

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.

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

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

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.

Meeting ID: 837 8989 1971

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

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

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.

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

Meeting ID: 837 8989 1971

February 14 | Monday | 4pm (Lisbon time)

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

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.

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

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

ID da reunião: 890 8479 3299
Senha de acesso: 409604

January 17 | Monday | 4pm (Lisbon time)

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

ID da reunião: 890 8479 3299
Senha de acesso: 409604

January 10 | Monday | 4pm (Lisbon time)

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.

ID da reunião: 890 8479 3299
Senha de acesso: 409604

December 13 | Monday | 4pm (Lisbon time)

Paulo Santos

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

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.

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.

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.

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

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.

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

ID da reunião: 890 8479 3299
Senha de acesso: 409604

October 25 | 4pm |  6.2.33

A Theory of Marginal and Large Difference

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.

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:

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.

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)

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.

LOCATION:  Zoom Meeting:
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)

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

LOCATION:  Zoom Meeting:
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.

LOCATION:  Zoom Meeting:
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.

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.

LOCATION:  Zoom Meeting:
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.

LOCATION:  Zoom Meeting:
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.

LOCATION:  Zoom Meeting:
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.

LOCATION:  Zoom Meeting:
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 .

LOCATION:  Zoom Meeting:
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.

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

ID da reunião: 890 8479 3299
Senha de acesso: 409604

30th of November | 4pm (Lisbon time)

Imme van den Berg

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.

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

ID da reunião: 890 8479 3299
Senha de acesso: 409604

23rd 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.

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

ID da reunião: 890 8479 3299
Senha de acesso: 409604

16th 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.

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

ID da reunião: 890 8479 3299
Senha de acesso: 409604

9th 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

2nd 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

26th of October | 16:00 (Lisbon time)

PEDRO PINTO

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.

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

ID da reunião: 890 8479 3299

Senha de acesso: 409604

19th of October | 16h00 (Lisbon time)

LOCATION:  Zoom Meeting:
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.

12th of October | 16h00 (Lisbon time)

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

Meeting ID: 892 4787 3078

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.

6th of July | 16h00 (Lisbon time)

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

Meeting ID: 923 5170 3489