### Mathematical Logic Webinar

25 outubro | 16:00 | sala 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