Mathematical Logic Webinars / Seminars
May 17 | Friday | 4:00 pm (Lisbon time)
Paulo Guilherme Santos (ISCAL and CMAFcIO)
TITLE :: Verifiability: an Empirical Account of Meaning
ABSTRACT :: Logical Positivism is widely considered a dead philosophy. In this talk, I will aim at giving new life to the movement by presenting parts of a book that I wrote on the subject that is ready for publication. Several key-ideas will be presented and one of the main aspects of this approach to Positivism is the absolute focus on empirical verifiability: even in the realm of Logic and Mathematics. As an example of the empirical analysis, I will account for Logic in my talk. My goal is to take a pragmatic approach to Logical Positivism and view it more as a description of meaning using Science, rather than engaging in never ending (pseudo-)philosophical debates on metaphysics.
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 10 | Friday | 3:00 pm (Lisbon time)
Jean-Baptiste Joinet (Université Jean Moulin, Lyon 3, France)
TITLE :: Dissymetrical Linear Logics
ABSTRACT :: A good way to introduce Linear Logic is to present it through the so called Curry-Howard correspondence (proofs-as-programs / cut elimination-as-computation / formulas-as-types). Indeed, in that frame, Linear Logic can be seen as a magnifying glass thanks to which the computational process (cut-elimination of intuitionistic or classical proofs) appears decomposed into specific, more elementary dynamical effects (which, in the dynamic of intuitionistic or classical proofs, are undistinguishable and remain mixed up).
The diversity of Linear Logic connectives (multiplicative, additive and exponential ones, and their variants as functorial exponentials, specialized exponentials etc) mirrors, at the level of types alias formulas (i.e. connectives and the rules involving them), that decomposition of the dynamic of proofs.
From that perpective, the various ways one is able to interpret (though translations) ``intuitionistic'' and ``classical'' Logic (respectively) in Linear Logic, have to be thought as catching statically some features of the respective possible dynamics of both logics.
Typically, when one interprets ``intuitionistic'' and ``classical'' implications in Linear Logic, the difference between them is not caught at the level of the implication connective itself (i.e. by distinguishing a classical and an intuitionistic implications as one sometimes does in the frame of the “Logical Ecumenism’’), but by using differently the modalities of Linear Logic: ``!'' and ``?’’. Statically, those modalities (called the exponentials) serve to indicate the (potential) use of left and right structural rules, respectively. Dynamically, structural rules are the source of the non linear, “structural” part of the computation (notably: duplication of code, erasing of code etc). Whence the slogan : “The exponentials are thus in charge of the structural part of the computation”.
In my talk, I will only (or mainly) focus on the exponentials “!” and “?” of Linear Logic. After presenting the four structural effects they are in charge of (in the simpler case of Intuitonistic Linear Logic, ILL), I will analyse the way “!” and “?” interact (statically and dynamically) and try to measure how far they are – or not – independent.
That investigation results in creating ``intermediate exponentials'' that I use to design computational systems of linear logic which are ``intermediate'' between Intuitionistic LL (ILL) and Classical LL (CLL). Methodologically, the focus is put on how to break the symmetrical interdependency between ! and ? which prevails in CLL, in order to get ``!'' and the resulting ``?'' playing well differentiated roles -- and this without to loose the computational properties (closure by cut-elimination, atomizability of identity axioms). Four main systems are designed (Dissymetrical LL, semi-functorial Dissymetrical LL, semi-specialized Dissymetrical LL, bi-conclusion LL).
If times allows, I will then show how to us Dissymetrical LL (DLL) as a tool to design multi-conclusion Intuitionistic sequent calculi.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
April 19 | Friday | 5:00 pm (Lisbon time)
Jaime Ramos (IST - Universidade de Lisboa)
TITLE :: (Bounded) Model Checking Distributed Temporal Logic
ABSTRACT :: The distributed temporal logic DTL is a logic for reasoning about temporal properties of distributed systems from the local point of view of the system's agents, which are assumed to execute sequentially and to interact by means of synchronous event sharing. In this talk, we propose an automata-theoretic model checking algorithm for DTL. To this end, we propose a notion of distributed transition system that will be used to specify the system to be verified. The properties that the system should meet are specified in DTL. In order to capture the models of these properties, we propose the notions of generalized distributed Buchi automaton and of distributed Buchi automaton. With these concepts, we are able to adapt results from automata-theoretic approaches to model checking in LTL to the distributed case. Then, we analyse the bounded model checking problem in the context of DTL. To this end, we adapt the bounded model checking algorithm for LTL to the case of DTL. To do so, a new notion of bounded semantics for DTL is proposed. In the bounded model checking approach, the witness problem is translated to the satisfiability of a propositional formula that can be addressed (efficiently) by SAT solvers.
Joint work with F. Dionísio, L. Viganò, F. Subtil and A. Peres.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
April 5 | Friday | 4:00 pm (Lisbon time)
Niko Gruben (Universidade de Lisboa)
TITLE :: Determinacy and Infinite Games
ABSTRACT :: The standard axioms of $ZFC$ have been fixed for some time now, with proposals for new axioms rarely gaining any traction. One particular area of set theory, the theory of infinite games, has nonetheless given rise to attractive new axioms exceptionally different from the classic ones. In this talk I will give an introduction to this area and some of its results, before moving on to the possible new axioms and their underlying philosophy.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
Online broadcast
March 22 | Friday | 4:00 pm (Lisbon time)
Albert Visser (Utrecht University)
TITLE :: Peano Arithmetic minus and Robinson's Arithmetic Siblings, so alike but so different
ABSTRACT :: This talk reports partly on research in collaboration with Ali Enayat and Mateusz Łełyk.
In my talk I give an introduction to two fundamental weak arithmetical theories, PA^- and Q. I will briefly review some of the salient facts about these theories.
We will zoom in on the question whether these theories have completions of restricted complexity. We consider both depth-of-quantifier-alternation complexity and the \Sigma_n-hierarchy. The theory PA^- has no complete extension of restricted depth-of-quantifier alternation complexity. The question whether Q has a complete extension of restricted depth-of-quantifier-alternation complexity remains open. Both Q and PA^- do have a complete extension of a single sentence plus a set of \Sigma_1-sentences. We will sketch a proof.
LOCATION: ONLINE
March 15 | Friday | 4:00 pm (Lisbon time)
António Marques Fernandes (Instituto Superior Técnico - Universidade de Lisboa)
TITLE :: The power of the power set axiom
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
March 8 | Friday | 4:00 pm (Lisbon time)
Clarence Protin (Universidade Aberta)
TITLE :: A Graph Calculus for Combinatory Intensional Logic
ABSTRACT :: Bealer's intensional logic project, expounded in Quality and Concept (1982), had the goal of developing a unified framework for modal logic and the intensional logic. The semantics aimed at being consistent with the position that properties, relations and propositions consist in entities in their own right, as well as furnishing the senses of linguistic expressions. In this talk we introduce Combinatory Intensional Logic (CIL), a generalized combinatory-style logic capable of representing both modal and intensional reasoning, and its associated concept-graph calculus. We show how CIL and this calculus can be used to address some of the problems and shortcomings of Bealer's original approach and to give an adequate definition of model. Finally we sketch the proof of the soundness of CIL.
Please note that the session will not be streamed via Zoom.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
March 1 | Friday | 4:00 pm (Lisbon time)
Maria Osório Costa (CMAFcIO, Faculdade de Ciências da Universidade de Lisboa)
TITLE :: On the proof theory of modal logics
ABSTRACT :: This talk is a report on my Master's Thesis, supervised by Professor Fernando Ferreira and Doctor Marianna Girlando. The thesis aims at presenting a proof-theoretical analysis of modal logics.
Modal logics extend classical propositional logic by adding to the language operators $'\Box'$ and $'\Diamond'$, expressing necessity and possibility. In this work, we will focus on the modal logics in the $\mathbf{S5}$-cube, built from the basic modal logic $\K$ by considering combinations of certain frame conditions such as reflexivity, symmetry and transitivity.
We are interested in studying sequent systems for this family of logics. The systems we present are based on Gentzen's calculus $\G$, with two additional pairs of rules for the modal operators and where the language has been extended with labels. These labels annotate formulas denoting worlds in a Kripke-model where they are satisfied. Note that this idea is not limited to sequent calculi, in fact, it has been studied for other formal systems such as natural deduction and tableaux. Moreover, the labels can represent, not only worlds in a model but also truth values.
We discuss several results that have been obtained in the literature for this family of modal logics, such as the admissibility of weakening, contraction, and most notably of the cut rule, which ensures the subformula property. Furthermore, we investigate proof-search termination strategies, which allows us to obtain countermodels for non-derivable sequents, and prove, via proof-theoretical tools, decidability and the finite model property for the logics in the cube, in particular for $\K$ and $\mathbf{S4}$ which we take as a case study.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
February 23 | Friday | 4:00 pm (Lisbon time)
Luís Cruz-Filipe (University of Southern Denmark)
TITLE :: Reasoning about Choreographic Programs
ABSTRACT :: Choreographic programming is a paradigm where a concurrent or distributed system is developed in a top-down fashion. Programs, called choreographies, detail the desired interactions between processes, and can be compiled to distributed implementations based on message passing. Choreographic languages usually guarantee deadlock-freedom and provide an operational correspondence between choreographies and their compiled implementations, but until now little work has been done on verifying other properties.
This talk presents a Hoare-style logic for reasoning about the behaviour of choreographies, and illustrate its usage in representative examples. We show that this logic is sound and complete, and discuss decidability of its judgements. Using existing results from choreographic programming, we show that {any functional correctness property proven for a choreography also holds for its} compiled implementation.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
February 16 | Friday | 4:00 pm (Lisbon time)
Melissa Antonelli (University of Helsinki)
TITLE :: Towards New Characterizations of Parallel Complexity Classes
ABSTRACT :: Implicit computational complexity is an active area of theoretical computer science, aiming to provide machine-independent characterizations of relevant complexity classes. One of the seminal works in this field appeared in 1964, when Cobham introduced a function algebra closed under bounded recursion on notation and able to capture FP, the class of functions computable in polynomial time. Since then, several complexity classes have been characterized using limited recursion schemas. Recently, an elegant algebra was defined by Bournez and Durand, who, in 2019, showed that ordinary differential equations (ODEs) offer a natural tool for algorithmic design and characterized FP via a special ODE schema. The overall goal of our study is precisely that of generalizing this approach to parallel computation and of providing (possibly uniform) ODE-style characterizations for small circuit classes. In particular, in this talk I will present the global aim and methodology at the basis of our in progress study and sketch our first result, namely our proposal for an original characterization of AC0 due to ODEs.
[Joint work with A. Durand and J. Kontinen]
LOCATION: ONLINE
February 9 | Friday | 4:00 pm (Lisbon time)
Chris Pollett (San Jose State University)
TITLE :: Arithmetics within the Linear Time Hierarchy
ABSTRACT :: The theory I∆0 of induction for bounded formulas in the language of arithmetic can be viewed as the union of the theories IEn, n > 0 where we restrict induction to n bounded quantifier alternations, the outermost being existential. The ∆0 formulas express exactly the linear time hierarchy sets, and so I∆0 is often the appropriate theory to prove complexity results concerning this hierarchy. Unfortunately, the theories IEn do not seem to correspond to natural complexity classes. On the other hand, if we add the Ω1 axiom, ∀x∀y∃z(x log2y = z) to I∆0, one gets a theory conservatively extended by Buss theory S2 whose sub-theories S i 2 do naturally correspond to complexity classes. Namely, the ∆b i -predicates of S i 2 are the P Σ p i sets. In this talk, I will survey arithmetics for complexity classes within the linear time hierarchy and will suggest what should be the appropriate analogs to the theories S i 2 within I∆0.
LOCATION: ONLINE
January 26 | Friday | 4:00 pm (Lisbon time)
Carlos Caleiro (Instituto Superior Técnico)
TITLE :: A manifesto for multiple-conclusions in logic
ABSTRACT :: In this talk we aim at showing the advantages of taking the notion of multiple-conclusion consequence relation proposed by Scott, Shoesmith and Smiley as an environment for studying Tarski-style single-conclusion logical consequence. For that purpose we will focus on two long-standing research tasks, modularization and axiomatizability, helping us to better understand how to obtain (good) calculi for given logics, as well as how to (effectively) build more complex logics incrementally from simpler ones.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
January 19, 2024 | Friday | 4:00 pm (Lisbon time)
Bruno Jacinto & Beatriz Souza (Universidade de Lisboa)
TITLE :: Choice in the Iterative Conception
ABSTRACT :: The iterative conception is arguably the best worked out conception of set available. What is the status of the Axiom of Choice, presumably the most controversial of ZFC's axioms, under this conception? Boolos argues that the iterative conception doesn't justify Choice. We show that Boolos's argument overgenerates. For, if cogent, it would also imply -- contrary to what Boolos advocates -- that the axioms of Pairing, Union, Separation and Powerset are not justified by the iterative conception. In addition, we offer a plural formulation of Boolos's stage theory (a formalization of the iterative conception) and show that prima facie plausible principles of the logic of plurals imply, together with plural stage theory, Choice as well as Pairing, Union, Separation and Powerset.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
January 12, 2024| Friday | 4:00 pm (Lisbon time)
Alan J. Cain
TITLE :: Albrecht Dürer's "Melencolia I" and Renaissance concepts of mathematical beauty
ABSTRACT :: Renaissance mathematicians knew -- and declared -- that they were recovering and building upon ancient mathematics. Archimedes was the ideal they aimed to emulate. But, at least initially, their aesthetic evaluation of mathematics -- their judgement of certain parts of mathematics as beautiful or elegant or otherwise -- owed more to the philosophy of Plato than to any inheritance from the mathematicians of antiquity. During the later Renaissance, this Platonic influence weakened: Johannes Kepler's work was shaped by it but also largely marked its end. In the seventeenth century, with the emergence of analytic geometry and number theory, there was little discernible Platonism in the aesthetic evaluation of mathematics.
This talk will briefly survey the influence of ancient Greek thought, philosophical and mathematical, on the Renaissance view of mathematical beauty, and illustrate how this view shifted away from the Greek influence. In particular, the contribution of the artist Albrecht Dürer will be discussed, and his famous engraving "Melencolia I" will be interpreted in the context of the Renaissance idea of mathematical beauty.
[This talk will be historical and philosophical. Only elementary algebra and geometry will appear.]
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
December 15 | Friday | 4:00 pm (Lisbon time)
Eduardo Skapinakis (NOVAMath, Universidade Nova de Lisboa)
TITLE :: The what, the why and the how of recursion theory in computational complexity
ABSTRACT :: While complexity classes are usually defined as the problems that can be solved by some computational model, under some resource bound, there is a variety of ways to characterize them without mentioning either of them. This is the topic of Implicit Complexity.
I will talk about the study of Complexity from the perspective of recursive functions, discussing the tools to capture non-deterministic, probabilistic and quantum classes and the role of composition in characterizing and restricting access to oracles.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
November 24 | Friday | 4:00 pm (Lisbon time)
Joan San-Millán (Centro de Filosofia das Ciências da Universidade de Lisboa)
TITLE :: Peano's structuralism
ABSTRACT :: Recent historical studies have investigated the first proponents of methodological structuralism in late nineteenth-century mathematics. In this paper, I shall attempt to answer the question of whether Peano can be counted amongst the early structuralists. I shall focus on Peano’s understanding of the primitive notions and axioms of geometry and arithmetic. First, I shall argue that the undefinability of the primitive notions of geometry and arithmetic led Peano to the study of the relational features of the systems of objects that compose these theories. Second, I shall claim that, in the context of independence arguments, Peano developed a schematic understanding of the axioms which, despite diverging in some respects from Dedekind’s construction of arithmetic, should be considered structuralist.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
November 10 | Friday | 4:00 pm (Lisbon time)
Paulo Guilherme Santos (NOVA FCT and ISCAL)
TITLE :: ω-Reflexive Theories
ABSTRACT :: We study the ω-reflexivity of theories T, i.e. the ability of a theory T to prove ω-con_{T_0}, with T_0 a finitely axiomatized sub-theory of T. We prove that, for every verifiably essentially reflexive theory T and every finitely axiomatized sub-theory T_0 of T, T+RFN_{\Sigma_2}(T) proves \ω-con_{T_0}. We develop a uniform version of ω-consistency, Uω-con_{T_0}, such that, for T and T_0 in the previous conditions, T proves Uω-con_{T_0}. n-consistency and theories of truth are also considered, namely Tr(PA) for which we get that Tr(PA) proves ω-con_{PA}.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
November 3 | Friday | 4:00 pm (Lisbon time)
Cristina Sernadas (Instituto Superior Técnico, Universidade de Lisboa /Instituto de Telecomunicações)
TITLE :: Conservative Translations Revisited
ABSTRACT :: We provide sufficient conditions for the existence of a conservative translation from a consequence system to another one. We analyze the problem in many settings, namely when the consequence systems are generated by a deductive calculus or by a logic system including both proof-theoretic and model-theoretic components. We also discuss reflection of several metaproperties with the objective of showing that conservative translations provide an alternative to proving such properties from scratch. We discuss soundness and completeness, disjunction property and metatheorem of deduction among others. We provide several illustrations of conservative translations.
Keywords: conservative translation between consequence systems, reflection of metatheorems by conservative translations
AMS MSC2020: 03B20, 03B45, 03B53, 03F03.
Jaime Ramos, João Rasga, Cristina Sernadas, Journal of Philosophical Logic, 52 (2023), no. 3, 889-913
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
October 13 | Friday | 2:00 pm (Lisbon time)*
Bruno Dinis (Universidade de Évora)
TITLE :: Strolling through a meadow
ABSTRACT :: Meadows are commutative rings with a multiplicative identity element and a total multiplicative inverse operation [1], which means that it is possible to divide by zero! Two of the main classes of meadows are involutive meadows, where the inverse of zero is defined to be zero, and common meadows, that instead introduce an error term that propagates through calculations. We introduce a new algebraic structure that can be characterized axiomatically and generalizes involutive meadows, by means of an equational axiomatization, and construct some models based on the external numbers of nonstandard analysis [2] and non-archimedean fields. Again using nonstandard analysis, we also show a model for common meadows based on the real numbers and of involutive meadows based on finite fields. With similar techniques, one could also obtain meadows based on rational numbers [3].
As it turns out, meadows are unions of rings and with an adequate order relation are a lattice.
We finish with a brief discussion on some possibilities concerning future work.
[1] Jan A. Bergstra and Alban Ponse. Division by Zero in Common Meadows, pages 46–61. Springer International Publishing, Cham, 2015.
[2] Bruno Dinis and Imme van den Berg. Neutrices and external numbers: a flexible number system. Monographs and Research Notes in Mathematics. CRC Press, Boca Raton, FL, 2019. , With a foreword by Claude Lobry.
[3] Bruno Dinis and Emanuele Bottazzi. Flexible involutive meadows (submitted) 2023.
(This is joint work with Emanuele Bottazzi. I will also mention some work in progress with João Dias)
*Note that the time is different than usual*
LOCATION: ONLINE
October 6 | Friday | 4:00 pm (Lisbon time)
Pedro Pinto (Technische Universitat Darmstadt)
TITLE :: The strange case of Dykstra’s algorithm
ABSTRACT :: In this talk we discuss a proof mining treatment of the strong convergence of Dykstra’s algorithm.
Halpern’s iterative method is probably the most common approach to strongly approximate fixed points of nonexpansive maps. The canonical proof (pliable to many other results) establishing strong convergence of the iteration relies on a crucial use of sequential weak compactness. It is well-understood how a proof-theoretical approach allows for the elimination of the compactness arguments via bounded collection principles, thus allowing for simple quantitative data in the analysis of such proofs.
Here, we focus on a different iterative method. Generalizing the alternating projection method, Dykstra’s algorithm strongly approximates the optimal solution of the convex feasibility problem. Similarly to Halpern, the strong convergence of Dykstra’s method makes crucial uses of compactness principles substantiated by arithmetical comprehension. Yet, as the iterative schema has no connection with Halpern’s definition and the proof follows a completely different structure, it was not known whether the removal of the compactness arguments would be possible and thus, a priori, we were only guaranteed to obtain quantitative data defined by bar-recursive functionals. Strikingly, still here, it was possible to bypass the use of arithmetical comprehension and bar-recursive functionals. We will discuss the recent quantitative analysis of Dykstra’s convergence proof and explain how it was possible to avoid the compactness principles crucial in the original proof.
References:
[1] F. Ferreira, L. Leustean, P. Pinto, On the removal of weak compactness arguments in proof mining, Advances in Mathematics 354, 55pp, 2019.
[2] U. Kohlenbach, P. Pinto, Fejér monotone sequences revisited, 2023 (preprint available at homepage https://www2.mathematik.tu-darmstadt.de/~pinto/).
[3] P. Pinto, On the finitary content of Dykstra’s cyclic projections algorithm, 2023 (preprint available at homepage).
LOCATION: ONLINE
May 26 | Friday | 4:00 pm (Lisbon time)
Carlos Olarte (LIPN, Université Sorbonne Paris Nord)
TITLE :: A Rewriting Logic Approach to Specification, Proof-search, and Meta-proofs in Sequent Systems
ABSTRACT :: We develop an algorithmic-based approach for proving inductive properties of propositional sequent systems such as admissibility, invertibility, cut-admissibility, and identity expansion. Although undecidable in general, these properties are crucial in proof theory because they can reduce the proof-search effort and further be used as scaffolding for obtaining other meta-results such as consistency. The algorithms take advantage of the rewriting logic meta-logical framework, and use rewrite- and narrowing-based reasoning. They have been fully mechanized in the L-Framework, thus offering both a formal specification language and off-the-shelf mechanization of the proof-search algorithms, together with semi-decision procedures for proving theorems and meta-theorems of the object system. As illustrated with case studies, the L-Framework achieves a great degree of automation when used on several propositional sequent systems, including single conclusion and multi-conclusion intuitionistic logic, classical logic, classical linear logic and its dyadic system, intuitionistic linear logic, and normal modal logics.
Joint work with Elaine Pimentel and Camilo Rocha.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
May 19 | Friday | 4:00 pm (Lisbon time)
Daniel Graça (University of Algarve)
TITLE :: Continuous characterizations of computational complexity classes with ordinary differential equations
ABSTRACT :: In this talk we will show that traditional computational complexity classes such as P, EXPTIME, or PSPACE can be characterized using polynomial ordinary differential equations, and that the same can be done for other classes such as the Grzegorczyk hierarchy and the class of primitive recursive functions. This talk describes work done in collaboration with O. Bournez, R. Gozzi, and A. Pouly.
LOCATION: ONLINE
May 12 | Friday | 4:00 pm (Lisbon time)
Laurentiu Leustean (University of Bucharest & Institute for Logic and Data Science & IMAR)
TITLE :: Proof mining in optimization and nonlinear analysis
ABSTRACT :: The research program of proof mining is concerned with the extraction of hidden finitary content from mathematical proofs. The new information is obtained after a logical analysis, using proof-theoretic tools, and can be both of quantitative nature, such as algorithms and effective bounds, as well as of qualitative nature, such as uniformities in the bounds or weakening the premises.
Thus, even if one is not particularly interested in the numerical details of the bounds themselves, in many cases such explicit bounds immediately show the independence of the quantity in question from certain input data.
This line of research, developed by Kohlenbach in the 90's, has its roots in Kreisel's program on unwinding of proofs, put forward in the 50's.
In this talk we give an introduction to proof mining and present some recent applications in optimization and nonlinear analysis.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
May 5 | Friday | 4:00 pm (Lisbon time)
Pablo Cubides Kovacsics (Universidad de los Andes)
TITLE :: Topological fields with a generic derivation
ABSTRACT :: In the late 70s, M. Singer provided an axiomatization of the class of closed ordered differential fields (CODF). Essentially, his axiomatization states that such a field is real closed and that the derivative has a generic behavior with respect to topology. Several authors have generalized this type of construction to other topological fields. Together with F. Point, and following Singer's ideas, we provide an abstract framework for axiomatizing, given a theory of topological fields T, the corresponding theory of T-models with a generic derivativation. In this talk, I will present this construction and some of its main properties. Towards the end of the talk, I will discuss applications. If time allows, I will mention an open question in this context.
LOCATION: ONLINE
Mathematical Logic Seminar
April 28 | Friday | 4:00 pm (Lisbon time)
René Gazzari (CMAT – Universidade do Minho)
TITLE :: The Calculus of Natural Calculation – An Introduction
ABSTRACT :: See attachment.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
April 21 | Friday | 4:00 pm (Lisbon time)
Isabel Oitavem (Universidade Nova de Lisboa)
TITLE :: Simplicity of Proofs and Combinatory Logic
ABSTRACT :: Related with investigations on simplicity of proofs, we focus on formulas of the form \phi implies \phi, adopting as framework the Pure Positive Implication Propositional Calculus based on Frege's axiomatization of implication. In this context, we search for a shortest proof of \phi implies \phi. There might be particular instances of this formula which admit proofs that are shorter than a shortest proof of \phi implies \phi in general. A first example is the case for \phi itself of the form \psi implies \psi. More examples are obtained by means of combinatory logic. This is joint work with Reinhard Kahle and Paulo Guilherme Santos.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
March 31 | Friday | 4:00 pm (Lisbon time)
Elaine Pimentel (University College London)
TITLE :: From axioms to synthetic inference rules via focusing
ABSTRACT :: One of the advantages of using sequent systems as a framework for logical reasoning is that the resulting calculi are often simple, have good proof theoretical properties (like cut-elimination, consistency, etc) and can be easily implemented, \eg\ using rewriting.
Hence it would be heaven if we could add axioms in mathematical theories to first order logics and reason about them using all the machinery already built for the sequent framework. Indeed, the general problem of extending standard proof-theoretical results obtained for pure logic to certain classes of non-logical axioms has been the focus of attention for quite some time now.
The main obstacle for this agenda is that adding non-logical axioms to systems while still maintaining the good proof theoretical properties is not an easy task. In fact, adding naively axioms to sequent systems often result in non cut-free systems. One way of circumventing this problem is by treating axioms as theories, added to the sequent context. This is already in Gentzen's consistency proof of elementary arithmetic. Now the derivations have only logical axioms as premises, and cut elimination applies.
But we can do better by transforming axioms into inference rules. In this talk, we will propose a systematic way of adding inference rules to sequent systems. The proposal will be based on the notions of focusing and polarities. We will also discuss how our framework escalates to hypersequents and systems of rules.
This is a joint work with Dale Miller, Sonia Marin and Marco Volpe.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
March 24 | Friday | 4:00 pm (Lisbon time)
Bruno Dinis (Universidade de Évora)
TITLE :: What if worlds could vary?
ABSTRACT :: In this talk I introduce an extension of Hybrid Logic, dubbed VHL, in which quantifier domains (over world and domain variables) may vary from world to world. Relying on a novel notion of prenex form, it is possible to introduce a new form of Skolemization, which is a non-trivial refinement of the usual process. These concepts are strongly dependent on the @ operator, and are therefore referred to as @-prenex normal form, and @-Skolemization.
I give an overview of the steps necessary to prove a Herbrand-like theorem for VHL, stating the equivalence between the satisfiability of a set of formulas and the propositional satisfiability of the ground instances of an @-Skolemized version of these formulas.
(joint work with Diana Costa)
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
March 17 | Friday | 4:00 pm (Lisbon time)
Nicholas Pischke (Technical University of Darmstadt)
TITLE :: Proof mining for the dual of a Banach space and extensions
ABSTRACT :: :: I present proof-theoretic metatheorems that allow applications of proof mining to proofs involving the dual of a Banach space and its corresponding norm. This in particular relies on a new approach to treating suprema of certain bounded sets without any additional proof-theoretical strength. As a further extension, I use this system to provide a proof-theoretic metatheorem for gradients of Frechet-differentiable functions and their conjugates.
LOCATION: ONLINE
Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971
Meeting ID: 837 8989 1971
March 10 | Friday | 4:00 pm (Lisbon time)
Paulo Firmino (University of Lisbon)
TITLE :: Functional interpretations over finite types with star types
ABSTRACT :: We define two functional interpretations on intuitionistic logic over finite types with the introduction of star types representing finite non-empty sets. The characteristic principles of the first (the semi-intuitionistic case) are variations of known principles, such as a form of choice, independence of premises and the lesser limited principle of omniscience, which take into account the star type. The second (the intuitionistic case) involves the standard principles of choice and independence of premises and requires a variation of Markov’s principle. We give Soundness and Characterization results, as well as corolaries regarding term extraction.
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 3 | Friday | 4:00 pm (Lisbon time)
Ana Catarina Monteiro (University of Lisbon)
TITLE :: Completeness of the random graph
ABSTRACT :: A graph with a countably infinite many vertices is said to be random if for every two disjoint sets of vertices A and B, there exists a vertex which is related with every vertex in A and none of the vertices in B. The study of random graphs was motivated by the search of the probability of a certain property occur in a graph. Fixing 𝑝 ∈ [0,1], we can think at a random graph as being obtained by starting with a set of isolated vertices and adding edges between them at random, where each edge as probability 𝑝 of occurring. It might not be immediate that we can use logic to study these structures, especially because the main models for random graphs are based essentially in probability, for example, the binomial random graph or the uniform random graph (S. Janson, A. Rucinski, T. Luczak, 2000), but in fact we can. In this seminar, after describing the set of axioms of the random graph, we will prove its completeness by using the Vaught’s test, and take a few conclusions about the set of all sentences true almost surely. For that, several concepts and results in model theory will be recalled.
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 24 | Friday | 4:00 pm (Lisbon time)
Alfredo Freire (University of Aveiro)
TITLE :: Non-tightness in class theory and second-order arithmetic
ABSTRACT :: A theory T is tight if different deductively closed extensions of T (in the same language) cannot be bi-interpretable. Many well-studied foundational theories are tight, including PA (Visser, 2006), ZF, Z_2 (second order arithmetic), and KM (Enayat, 2017). In this presentation, we study subsystems of these latter two theories. We start with a brief exposition of the tightness phenomena and then we prove that restricting the Comprehension schema of Z_2 and KM gives non-tight theories. These results provide evidence that tightness characterizes Z_2 and KM in a minimal way.
This talk is about joint work with Kameryn Williams, Sam Houston University.
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 17 | Friday | 4:00 pm (Lisbon time)
Pantelis Eleftheriou (University of Leeds)
TITLE :: An unbounded version of Zarankiewicz's problem
ABSTRACT :: :: Zarankiewicz's problem for hypergraphs asks for upper bounds on the number of edges of a hypergraph that has no complete sub-hypergraphs of a given size. Let M be an o-minimal structure. Basit-Chernikov-Starchenko-Tao-Tran (2021) proved that the following are equivalent:
(1) "linear Zarankiewicz's bounds" hold for hypergraphs whose edge relation is induced by a fixed relation definable in M
(2) M does not define an infinite field.
We prove that the following are equivalent:
(1') linear Zarankiewicz bounds hold for sufficiently "distant" hypergraphs whose edge relation is induced by a fixed relation definable in M
(2') M does not define a full field (that is, one whose domain is the whole universe of M).
This is joint work (in progress) with Aris Papadopoulos.
LOCATION: ONLINE
Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971
Meeting ID: 837 8989 1971
February 3 | Friday | 4:00 pm (Lisbon time)
Ana Borges (University of Barcelona)
TITLE :: An escape from Vardanyan’s Theorem
ABSTRACT :: :: Vardanyan's Theorem states that quantified provability logic is Π^0_2-complete, and in particular impossible to recursively axiomatize for consistent theories containing a minimum of arithmetic. However, the proof of this fact cannot be performed in a strictly positive signature. We define a (decidable) quantified strictly positive logic called QRC_1 and show that it is a provability logic: there is a Solovay-like completeness theorem relating QRC_1 to Peano Arithmetic.
This is joint work with Joost J. Joosten.
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
January 27 | Friday | 4:00 pm (Lisbon time)
Laura Crosilla (University of Oslo)
TITLE :: On Weyl's predicative concept of set
ABSTRACT :: :: In the book Das Kontinuum (1918), Hermann Weyl presents a coherent and sophisticated approach to analysis from a predicativist perspective. In the first chapter of (Weyl 1918), Weyl introduces a predicative concept of set, according to which sets are built 'from the bottom up' starting from the natural numbers. Weyl clearly contrasts this predicative concept of set with the concept of arbitrary set, which he finds wanting, especially when working with infinite sets. In the second chapter of Das Kontinuum, he goes on to show that large portions of 19th century analysis can be developed on the basis of his predicative concept of set. Das Kontinuum inspired fundamental ideas in mathematical logic and beyond, such as the logical analysis of predicativity of the 1950-60's, Solomon Feferman's work on predicativity and Errett Bishop's constructive mathematics. The seeds of Das Kontinuum are already visible in the early text (Weyl 1910), where Weyl, among other things, offers a clarification of Zermelo's axiom schema of Separation. In this talk, I examine Weyl's predicative concept of set in (Weyl 1918) and discuss its origins in (Weyl 1910).
Bibliography:
Weyl, H., 1910, Über die Definitionen der mathematischen Grundbegriffe, Mathematischnaturwissenschaftliche Blätter, 7, pp. 93-95 and pp. 109-113.
Weyl, H., 1918, Das Kontinuum. Kritische Untersuchungen über die Grundlagen der Analysis, Veit, Leipzig. Translated in English, Dover Books on Mathematics, 2003.
LOCATION: ONLINE
January 20 | Friday | 4:00 pm (Lisbon time)
Imme van Den Berg (Universidade de Évora)
TITLE :: Gaussian elimination for flexible systems of linear inclusions
ABSTRACT :: Flexible systems are linear systems of inclusions in which the elements of the coefficient matrix are external numbers in the sense of nonstandard analysis. External numbers represent real numbers with small, individual error terms. Using Gaussian elimination, a flexible system can be put into a row-echelon form with increasing error terms at the right-hand side. Then parameters are assigned to the error terms and the resulting system is solved by common methods of linear algebra. The solution set may have indeterminacy not only in terms of linear spaces, but also of modules.
Joint work with Nam Van Tran, HCMC University of Technology and Education, Vietnam.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
Online broadcast: https://videoconf-colibri.zoom.us/j/92509383401
Meeting ID: 925 0938 3401
January 13 | Friday | 4:00 pm (Lisbon time)
Sérgio Marcelino (IST – Universidade de Lisboa)
TITLE :: Pros and Cons of Generalizing Truth-Functionality
ABSTRACT :: Why should we consider moving from the standard notion of logical matrix introduced by Łukasiewicz more than a century ago?
We will explore the impact of adopting partial and non-deterministic matrices (PNmatrices) as semantical units.
Partial non-deterministic matrices (PNmatrices) embody a generalized notion of truth-functionality by interpreting the connectives in the language through a multi-function rather than a function.
The usual semantics over logical matrices smoothly generalizes to PNmatrices by reading the multi-function interpreting each connective as giving a (possibly empty) menu of possible outputs to each input. This menu is interpreted non-deterministically, in the sense that valuations are not completely determined by the values they assign to the variables. Instead, every valuation is built by layers and has the freedom to give each complex formula any of the values from the menu associated with the head connective and the inputs determined by the values of the immediate subformulas.
The initial motivation to step into this generalized setting was to obtain finite presentations of logics that could not be captured by finite matrices [1,2]. For many purposes PNmatrices preserve the good properties of finite matrices. These include important bridges with analytical calculi that enable purely symbolic decision procedures to decide the logic induced by a finite PNmatrix, including proof-search and counter model-generation functionalities [3,4]. Moreover, their greater plasticity has been essential for a number of compositionality results for combined logics [5,6]. We will take some time to illustrate this by showing that PNmatrices naturally emerge when we try to close a certain category of matrices for products [7].
Since there is always a flip side, we will also report on the challenges brought by this larger and richer setting. For instance, some naturally associated computational problems become undecidable, such as the problem of determining if the logic induced by a given finite PNmatrix has a theorem, or if two finite PNmatrices induce the same logic [8].
Finally, we discuss the challenges associated with extending the well established techniques of abstract algebraic logic to deal with PNmatrices [9].
[1] A. Avron and I. Lev. Non-deterministic multiple-valued structures. Journal of Logic and Computation, 2005.
[2] M. Baaz, O. Lahav, and A. Zamansky. Finite-valued semantics for canonical labelled calculi. Journal of Automated Reasoning, 2013.
[3] C. Caleiro, S. Marcelino. Axiomatizing non-deterministic many-valued generalized consequence relations. Synthese, 2021
[4] C. Caleiro, S. Marcelino. Analytic calculi for monadic PNmatrices. WoLLIC, 2019
[5] C. Caleiro, S. Marcelino. Disjoint fibring of non-deterministic matrices. WoLLIC, 2017
[6] C. Caleiro, S. Marcelino. Modular semantics for combined many-valued logics. Submitted
[7] C. Caleiro, S. Marcelino. Rediscovering partial non-deterministic logical matrices. Submitted
[8] P. Filipe, S. Marcelino, C. Caleiro. Computational properties of finite PNmatrices. Journal of Logic and Computation, 2022
[9] C. Caleiro, S. Marcelino, U. Rivieccio. Some more theorems on generalized consequence relations. Submitted
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
Online broadcast: https://videoconf-colibri.zoom.us/j/92509383401
Meeting ID: 925 0938 3401
January 6 | Friday | 4:00 pm (Lisbon time)
Luís Cruz-Filipe (University of Southern Denmark)
TITLE :: Logic and Explainable AI in the Legal Domain
ABSTRACT :: In spite of the huge increase in the usage of Artificial Intelligence (AI) in nearly all areas of everyday life, applications to the legal domain are surprisingly absent. This is due to the fact that most current AI systems are black-box constructions, which are incompatible with the ethical requirements underlying most western legal systems. In this talk we discuss this problem and introduce our project on building an expert system within the legal domain based on logical techniques.
Joint work with Jonas Vistrup.
LOCATION: Faculdade de Ciências da Universidade de Lisboa, room C6.2.33
Online broadcast: *Please note the different zoom link*
https://videoconf-colibri.zoom.us/j/92509383401
Meeting ID: 925 0938 3401
December 16 | Friday | 4:00 pm (Lisbon time)
Clarence Protin (Universidade Aberta)
TITLE :: A simple proof assistant for first-order logic and set theory
ABSTRACT :: In this short talk we describe the Pylog software project and its application to Kelley-Morse set theory. Pylog is a minimalistic Python command-line based proof assistant and proof checker based on linearised natural deduction for first-order logic with equality and a comprehension operator.
First-order logic is extended with formula-variables to deal with propositional validities. Axiom schemes are implemented as additional rules.
The main feature of Pylog is that both the interface and the source-code are simple and transparent and easily understandable by the logician and formally-minded mathematician with only the most basic knowledge of Python. This is also useful to the programer who wishes to modify or develop Pylog or incorporate it into more advanced projects.
Pylog is based on the philosophy that (exhaustively) detailed natural deductions proofs (where the classical negation rule is added to the core intuitionistic rules and is used as desired or needed) are at least a step in the right direction for capturing how mathematicians go about writing proofs. The next step is to achieve a kind of micro-automatisation and condensation of the proof in the direction of greater conciseness and readibility, perhaps employing techniques similar to the "tactics" of Coq.
We describe our project of formalising Kelley-Morse set theory as found in the famous appendix of Kelley's General Topology (1955).
At present there is over ten thousand lines of proof covering over eighty theorems. We illustrate the Pylog command-line environment by proving a simple consequence of the axiom of regularity. We then give a description of the next stages of the PyLog project.
Finally we end with some short remarks on mainstream formal mathematics projects and the foundations of mathematics.
LOCATION: ONLINE
Online broadcast: https://videoconf-colibri.zoom.us/j/83789891971
Meeting ID: 837 8989 1971
December 9 | Friday | 4:00 pm (Lisbon time)
Bruno Jacinto (Universidade de Lisboa)
TITLE :: Sets as Properties
ABSTRACT :: According to the iterative conception of set, sets are “built in stages” in a process to be pursued “as far as possible”. It is notoriously difficult to make sense of the “building” analogy unless the mind-dependence of sets is accepted. In this talk I will sketch the sets as properties view, according to which set theory is nothing but a part of cumulative (modal) type theory. I will offer some reasons for thinking that the sets as properties view, broadly based on (Linnebo & Rayo 2012, Degen & Johannsen 2000) delivers a more satisfactory realist understanding of the iterative conception, and its "building" analogy, than those presently available. In addition, I will address Button and Trueman’s (2022) “no bootstrapping" objection to the sets as properties view, and show how my reply paves the way to a neoRussellian form of logicism about set theory.
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
December 2 | Friday | 4:00 pm (Lisbon time)
António Marques Fernandes (IST - Universidade de Lisboa)
TITLE :: Fraenkel-Mostowski Models (Part II)
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
November 25 | Friday | 4:00 pm (Lisbon time)
António Marques Fernandes (IST - Universidade de Lisboa)
TITLE :: Fraenkel-Mostowski Models
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
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
Online broadcast:
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.
Online broadcast:
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.
Online broadcast:
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.
Online broadcast:
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.
Online broadcast:
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
Online broadcast:
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.
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)
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.
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)
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).
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
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.
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
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.
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
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.
6th 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.