**Historical note:** SLM was created in 1989 by Fernando Ferreira (Faculdade de Ciências da Universidade de Lisboa) and Narciso Garcia (Instituto Superior Técnico).

*In 2017/2018, the SLM will be on Fridays from 3pm to 4pm. It will take place at Faculdade de Ciências da Universidade de Lisboa (usually) in room C6.2.33 (building C6, second-floor, room 33).*

Seminars are usually posted on Mondays

March 22 (Thursday), 4pm, room 6.2.33

**BOGDAN DICHER**

CENTRO DE FILOSOFIA, UNIVERSIDADE DE LISBOA

The original sin of proof-theoretic semantics

ABSTRACT :: :

Proof-theoretic semantics is a form of logical inferentialism, holding that the meaning of the logical constants is determined by the rules of inference which govern their behaviour in proofs. In this tradition, it is usually assumed that given a logical calculus, there always *exists* a *unique* relation that qualifies as a consequence relation. We argue that both of these two assumptions are incorrect. Nevertheless, this does not spell the end of the proof-theoretic project and the project is feasible provided one understands its aim as that of determining the meaning of the logical constants relative to a certain reflexive, monotonic, and transitive relation that can be uniquely determined using the Blok-Jonsson theory of abstract consequence relations.

(Joint work with Francesco Paoli — University of Cagliari)

March 15 (Thursday), 4pm, room 6.2.33

**BRUNO DINIS**

CMAFCIO, UNIVERSIDADE DE LISBOA

Intuitionism, nonstandard arithmetic and functional interpretations (part 2)

March 8 (Thursday), 4pm, room 6.2.33

**BRUNO DINIS**

CMAFCIO, UNIVERSIDADE DE LISBOA

Intuitionism, nonstandard arithmetic and functional interpretations

ABSTRACT :: :

In this two-part talk I will present a bounded modified realizability and a bounded functional interpretation for intuitionistic nonstandard arithmetic in finite types with nonstandard principles. These interpretations are sound and complete and allow to fulfill a three part goal: (i) to obtain constructive content for nonstandard arithmetic via the extraction of bounds on witnesses; (ii) to study proof-theoretic properties of nonstandard arithmetic; (iii) to fill a gap in the literature, being in line with nonstandard methods to analyze compactness arguments. The functional interpretation presented in this talk is the intuitionistic counterpart of the functional interpretation presented by Ferreira and Gaspar. In fact, by extending Krivine's negative translation and combining it with our intuitionistic functional interpretation one obtains Ferreira and Gaspar's classical functional interpretation for nonstandard arithmetic. Moreover, restricting the realizability and the functional interpretation to the so-called "purely external fragment" one recovers respectively the bounded modified realizability of Ferreira and Nunes and the bounded functional interpretation of Ferreira and Oliva. Our interpretations also bear similarities with a functional interpretation presented by Van den Berg, Briseid and Safarik but replacing finiteness conditions by majorizability conditions. I will make some remarks concerning the Transfer principle and present versions with truth of both the realizability and the functional interpretation. These versions with truth will allow to introduce the so-called "copies-only method" that allows to give a faster proof of the soundness theorem.

(Joint work with Jaime Gaspar)

March 2 (Thursday), 4pm, room 6.2.33

**ALEX USVYATSOV **

CMAFCIO, UNIVERSIDADE DE LISBOA

**On the fundamental theorem of statistical learning**

ABSTRACT :: : I will discuss the seminal theorem of Vapnik and Chervonenkis on the uniform convergence of relative frequencies of events to their probabilities (a uniform version of the weak law of large numbers). This result is vastly regarded as the foundation of machine learning. However, it has interesting implications in many other areas of mathematics. I will discuss some connections between VC-theory and logic. As promised in one of my previous talks, I will also say something about the proof of the theorem. This talk is completely independent of the previous ones.

February 22 (Thursday), 4pm, room 6.2.33

**GABRIELE PULCINI**

FCT, UNIVERSIDADE NOVA DE LISBOA

**Complementary logic and proof-theoretic many-valuedness**

ABSTRACT :: In the first part of my talk, I'll consider LK°, a cut-free sequent calculus able to faithfully characterize classical (propositional) non-theorems, in the sense that a formula A is provable in LK° if, and only if, it is not provable in LK. I'll show how to enrich LK° with two admissible (unary) cut rules, which allow for a simple and efficient cut-elimination algorithm. I’ll then highlight two facts: 1) complementary cutelimination always returns the simplest proof for any given provable sequent, and 2) provable complementary sequents turn out to be "deductively polarized" by the empty sequent.

In the second part, I'll observe how an alternative sequent system for complementary classical logic can be obtained by slightly modifying Kleene's system G4. I'll show how this move could pave the way for a new approach to many-valuedness and proof-theoretic semantics.

February 9 (Friday), 4:30pm, room 6.2.33

**ALEX USVYATSOV**

UNIVERSIDADE DE LISBOA

**Using o-minimality to compute lower bounds on sample complexity of neural networks (part 2)**

ABSTRACT :: I will discuss the concept of sample complexity in statistical learning theory. Then I will show how definability of many hypothesis classes (for example, essentially all artificial neural networks used in practice) in o-minimal structures, helps to compute tighter lower bounds on sample complexity for these hypothesis classes.

February 9 (Friday), 3pm, room 6.2.33

**LUDOVIC PATEY**

INSTITUT CAMILLE JORDAIN (LYON)**Pigeons do not jump high**

ABSTRACT :: The infinite pigeonhole principle asserts that every set of integers admits an infinite subset in it or its complement. This seemingly trivial principle surprisingly admits highly non-trivial computability-theoretic features, when considering non-computable instances. In particular, one may wonder whether there is an instance of the pigeonhole principle whose solutions are all high. The answer to this question will be given during this talk, although the careful reader might find a subtle clue in the title. This is a joint work with Benoit Monin.

February 2 (Friday), 3pm, room 6.2.33

**ALEX USVYATSOV**

UNIVERSIDADE DE LISBOA

**Using o-minimality to compute lower bounds on sample complexity of neural networks**

ABSTRACT :: I will discuss the concept of sample complexity in statistical learning theory. Then I will show how definability of many hypothesis classes (for example, essentially all artificial neural networks used in practice) in o-minimal structures, helps to compute tighter lower bounds on sample complexity for these hypothesis classes.

January 19 (Friday), 3pm, room 6.2.33.

**JOSÉ ESPÍRITO SANTO**

UNIVERSIDADE DE LISBOA

**A refined interpretation of intuitionistic logic by means of atomic polymorphism**

ABSTRACT :: In this seminar, an alternative embedding of IPC into atomic system F will be presented. Its translation of proofs is based, not on instantiation overflow, but instead on the admissibility of the elimination rules for disjunction and absurdity (where these connectives are defined according to the Russell- Prawitz translation). As compared to the embedding based on instantiation overflow, the alternative embedding works equally well at the levels of provability and preservation of proof identity, but it produces shorter derivations and shorter simulations of reduction sequences. Lambda-terms are employed in the technical development so that the algorithmic content is made explicit, both for the alternative and the original embeddings. The investigation of preservation of proof-reduction steps by the alternative embedding enables the analysis of generation of "administrative'' redexes. These are the key, on the one hand, to understand even better the difference between the two embeddings; on the other hand, to understand whether the final word on the embedding of IPC into atomic system F has been said.

(This is joint work with Gilda Ferrreira.)

January 12 (Friday), 3pm, room 6.2.33.

**PEDRO PINTO**

UNIVERSIDADE DE LISBOA

**Collection in Proof Mining: a general principle**

ABSTRACT :: Proof mining is the research program that aims to analyse proofs of mathematical theorems in order to extract hidden quantitative information – such as rates of convergence, rates of metastability and rates of asymptotic regularity. Proof theoretical tools like Kohlenbach’s monotone functional interpretation ([1]), a variant of Gödel’s Dialectica, are of standard use. A newer functional interpretation was introduced by Ferreira and Oliva in 2005 ([2]), dubbed the bounded functional interpretation (BFI). In recent work, a general principle was developed to analyse certain proofs that rely on a weak sequential compactness argument. By using a principle of bounded collection, we are able to consider an alternative simpler proof in a setting suited for an analysis with the BFI.

REFERENCES :: [1] Browder, Felix. *Convergence of approximants to fixed **points of nonexpansive nonlinear mappings in Banach spaces*. Archive for Rational Mechanics and Analysis, 24(1):82-90, 1967.

[2] Ferreira, Fernando, and Paulo Oliva. *Bounded functional interpretation*. Annals of Pure and Applied Logic 135.1-3: 73-112, 2005.

[3] Kohlenbach, Ulrich. *Applied proof theory: proof interpretations and their use in mathematics*. Springer Science & Business Media, 2008.

[4] Kohlenbach, Ulrich. *On quantitative versions of theorems due to FE Browder and R. Wittmann*. Advances in Mathematics, 226(3):2764-2795, 2011.

[5] Wittmann, Rainer. *Approximation of fixed points of nonexpansive mappings*, Arch. Math 58: 486-491, 1992.

November 24 (Friday), 3pm, room 6.2.33.

**EMANUELE FRITTAION**

UNIVERSIDADE DE LISBOA

**On Goodman realizability**

ABSTRACT :: Goodman's theorem (after Nicholas D. Goodman) asserts that adding the axiom of choice to intuitionistic arithmetic in all finite types yields a system which is conservative over Heyting arithmetic. This is in contrast with classical arithmetic in all finite types. In fact, the combination of choice with classical logic results in a system as strong as full second-order arithmetic.

There are several proofs of this result. The most direct proof was given by Goodman in his paper "Relativized realizability in intuitionistic arithmetic of all finite types", J. Symbolic Logic 43 (1978) and is based on a realizability interpretation which combines Kleene recursive realizability with Kripke semantics. I will discuss this notion of realizability and then present a modified version of Goodman realizability that shows that intuitionistic arithmetic in all finite types augmented with both choice and extensionality is also conservative over Heyting arithmetic. The only proof of this result is due to Michael Beeson.

November 17 (Friday), 3pm, room 6.2.33.

**JEAN-YVES BÉZIAU**

UNIVERSITY OF BRAZIL, RIO DE JANEIRO AND ÉCOLE NORMALE SUPÉRIEURE, PARIS

**What is a substructural logic?**

ABSTRACT :: This talk is about the nature and definition of the notion of "substructural logic" from the point of view of universal logic. I will discuss the connections and differences between a general approach of logical systems based on sequent systems and the Polish logic methodology based on consequence operator or consequence relation, analyzing some phenomena like cut. I will study various examples of logics, in particular I will examine in which sense intuitionistic logic can be considered as a substructural logic or not.

October 27 (Friday), 4:30pm, room 6.2.33.

**PABLO CUBIDES KOVACSICS**

UNIVERSITÉ DE CAEN

**Polynomially bounded C-minimal valued fields**

ABSTRACT :: After introducing C-minimal expansions of valued fields, the aim of the talk is to show that every C-minimal valued field having a value group which is $Q$-linearly bounded is uniformly polynomially bounded. As a corollary, we obtain that any C-minimal expansion of valued fields like C_p, Falg((tQ)) and, in general, of any valued field having Q as its value group, is uniformly polynomially bounded. This is a joint work with Françoise Delon.

[Supported by the ERC project TOSSIBERG (Grant Agreement 637027)]

October 27 (Friday), 3pm, room 6.2.33.

**ZORAN OGNJANOVIC**

MATHEMATICAL INSTITUTE OF THE SERBIAN ACADEMY OF SCIENCES AND ARTS

**An introduction to logics with probability operators**

ABSTRACT :: The problems of representing, and working with, uncertain knowledge are ancient problems dating, at least, from Leibnitz. In the last decades there is a growing interest in the field connected with applications to computer science and artificial intelligence. Researchers from those areas have studied uncertain reasoning using different methods. Some of the proposed formalisms for handling uncertain knowledge are based on logics with probability operators. The aim of this presentation is to provide an introduction to such formal systems. The main focus is related to mathematical techniques for infinitary probability logics used to obtain results about proof-theoretical and model-theoretical issues: axiomatizations, completeness, compactness, decidability.

October 20 (Friday), 3pm, room 6.2.33.

**LAURENTIU LEUSTEAN**

UNIVERSITY OF BUCHAREST AND SIMION STOILOW INSTITUTE OF MATHEMATICS OF THE ROMANIAN ACADEMY

**Proof mining in convex optimization and nonlinear analysis**

ABSTRACT :: The research program of proof mining in mathematical logic – first suggested by G. Kreisel in the 1950s as ‘unwinding of proofs’ and developed by U. Kohlenbach in the 1990s and afterwards – is a field of study that aims to analyze, using proof-theoretic tools, the proofs of existing mathematical theorems in order to obtain their hidden quantitative content. The new information is both of quantitative nature, such as algorithms and effective bounds, as well as of qualitative nature, such as uniformities in the bounds. In this talk we give an introduction to proof mining and present some recent applications in convex optimization and nonlinear analysis.

October 6 (Friday), 3pm, room 6.2.33.

**ALEXANDER USVYATSOV**

UNIVERSIDADE DE LISBOA

**Continuous model theory and Banach space geometry: an introduction. (Part 3)**

ABSTRACT :: These talks are intended as a soft and not too technical introduction to model theory of metric structures, including a short history and motivating questions, with a particular emphasis on fundamentals of continuous first order logic. I will also mention a few successful applications to Banach space theory, as well as more recent promising directions. In the last talk, I will introduce examples of continuos structures and theories: the Hilbert space, probability algebras, and, if time permits, the Hilbert space with a generic unitary operator. Coming back to applications in Banach space geometry that I mentioned in the first lecture, I also hope to briefly discuss the concept of stability in continuous logic.

September 29 (Friday), 3pm, room 6.2.33.

**ALEXANDER USVYATSOV**

UNIVERSIDADE DE LISBOA

**Continuous model theory and Banach space geometry: an introduction. (Part 2)**

ABSTRACT :: These talks are intended as a soft and not too technical introduction to model theory of metric structures, including a short history and motivating questions, with a particular emphasis on fundamentals of continuous first order logic. I will also mention a few successful applications to Banach space theory, as well as more recent promising directions. In the second talk, I will formally define first-order continuous logic and discuss some basic properties. I also plan on introducing examples of continuous structures and theories: the Hilbert space, probability algebras, and, if time permits, the Hilbert space with a generic unitary operator. The second talk is essentially independent of the first.

September 22 (Friday), 3pm, room 6.2.33.

**ALEXANDER USVYATSOV**

UNIVERSIDADE DE LISBOA

**Continuous model theory and Banach space geometry: an introduction**

ABSTRACT :: These two talks are intended as a soft and not too technical introduction to model theory of metric structures, including a short history and motivating questions, with a particular emphasis on fundamentals of continuous first order logic. I will also mention a few successful applications to Banach space theory, as well as more recent promising directions.

# 2016/2017

July 25 (Tuesday), 3pm, room 6.2.33. *Seminar hors-série.*

**RUY DE QUEIROZ**

UNIVERSIDADE FEDERAL DE PERNAMBUCO

**Propositional equality, identity types, and computational paths**

ABSTRACT :: In structural proof theory the notion of canonical proof is rather basic, and it is usually taken for granted that a canonical proof of a sentence must be unique up to certain minor syntactical details. When setting up a proof theory for equality one is faced with a somewhat unexpected situation where there may not be a unique canonical proof of an equality statement. Indeed, in a (1994) proposal for the formalisation of proofs of propositional equality in the Curry-Howard style, we have already uncovered such a peculiarity. Totally independently, and in a different setting, Hofmann & Streicher (1994) have shown how to build a model of Martin-Löf's Type Theory (with the so-called Identity Type) in which uniqueness of canonical proofs of identity statements does not hold. The intention here is to show that, by considering proofs of equality as sequences of rewrites and substitution, it comes a rather natural fact that two distinct proofs may be canonical and yet none is to be preferred over the other. By looking at proofs of equality as rewriting (or computational) paths this approach is in line with the recently proposed connections between type theory and homotopy theory via identity types, since elements of identity types will be, concretely, paths (or homotopies), with unbounded iteration of this (paths between paths, etc.). By introducing terms representing paths, the notion of 'paths between paths' becomes rather natural, and thus a syntactical counterpart to the notion of homotopy emerges quite straightforward. Recent results giving a categorical interpretation of identity types as types of computational paths will also be touched upon, time permitting.

July 7 (Friday), 3pm, room 6.2.38.

**PEDRO PINTO**

UNIVERSIDADE DE LISBOA

**A quantitative analysis of a theorem by F.E.Browder guided by the bounded functional interpretation**

ABSTRACT :: In [2], Kohlenbach did an analysis of the proof of Browder's theorem (in [1]) via the monotone functional interpretation. I will be following the same outline but guided by the bounded functional interpretation ([3], [4]). Although the bounds obtained are the same, this example provides a first look at how the bounded functional interpretation works in practice.

[1] Browder, Felix E, Convergence of approximants to fixed points of nonexpansive nonlinear mappings in Banach spaces, Archive for Rational Mechanics and Analysis, vol. 24 (1967), no. 1, pp. 82-90.

[2] Kohlenbach, Ulrich, On quantitative versions of theorems due to F.E. Browder and R. Wittmann, Advances in Mathematics, vol. 226 (2011), no. 3, pp. 2764-2795.

[3] Ferreira, Fernando and Oliva, Paulo, Bounded functional interpretation, Annals of Pure and Applied Logic, vol. 135 (2005), no. 1-3, pp. 73-112.

[4] Ferreira, Fernando, Injecting uniformities into Peano arithmetic, Annals of Pure and Applied Logic, vol. 157 (2009), no. 2, pp. 122-129.

June 30 (Friday), 3pm, room 6.2.33.

**MANUEL MARTINS**

UNIVERSIDADE DE AVEIRO

**Equational Hybrid Propositional Type Theory**

ABSTRACT :: Equational Hybrid Propositional Type Theory is a combination of propositional type theory, equational logic and hybrid modal logic. The structures used to interpret the language contain a hierarchy of propositional types, an algebra and a Kripke frame. In this talk we present a calculus for this logic that combines the axiomatics of its three components. The completeness proof is based on the three proofs Henkin published last century: (i) Completeness in type theory (ii) The completeness of the ﬁrst-order functional calculus and (iii) Completeness in propositional type theory. The challenge was to deal with all the heterogeneous components in an integrated system.

(This is joint work with Maria Manzano and Antonia Huertas)

June 23 (Friday), 3pm, room 6.2.33.

**EZGI SU**

UNIVERSIDADE DE LISBOA

**A unifying approach for (reflexive) autoepistemic logic, nonmonotonic S4F and ASP**

ABSTRACT :: Autoepistemic logic is an important form of nonmonotonic reasoning, introduced by Moore in order to allow an agent to reason about his own knowledge. It extends classical propositional logic by an epistemic modal operator L. Schwarz has shown that autoepistemic logic (AEL) and reflexive autoepistemic logic (RAEL) are the nonmonotonic variants of respectively the modal logics KD45 and SW5. In this talk, we implement the same strategy, embedding nonmonotonic S4F into a monotonic bimodal logic MLF*, to AEL and RAEL. This way, we propose a unifying mechanism for these major forms of nonmonotonic reasoning. Pearce’s equilibrium logic (EL) is a general-purpose nonmonotonic formalism, principally proposed as a semantical framework for answer set programming (ASP). Farinas et al. has recently embedded EL into a monotonic bimodal logic called MEM. Finally, in this talk, we discuss the relations between these two approaches, and try to find out the potential capability for capturing MEM under MLF*.

June 9 (Friday), 3pm, room 6.2.33.

**EZGI SU**

UNIVERSIDADE DE LISBOA

**An S4F-related monotonic modal logic**

ABSTRACT :: This paper introduces a novel monotonic modal logic, allowing us to capture the nonmonotonic variant of the modal logic S4F: we add a second new modal operator into the original language of S4F, and show that the resulting formalism is strong enough to characterise the logical consequence of (nonmonotonic) S4F, as well as its minimal model semantics. The latter underlies major forms of nonmonotonic logic, among which are (reflexive) autoepistemic logic, default logic, and nonmonotonic logic programming. The paper ends with a discussion of a general strategy, naturally embedding several nonmonotonic logics of a similar floor structure on which a (maximal) cluster sits.

June 2 (Friday), 3pm, room 6.2.33.

**MÁRIO EDMUNDO**

UNIVERSIDADE DE LISBOA

**Integration in non-archimedean real closed fields with archimedean value group (part 5)**

ABSTRACT :: In this seminar we present (some of) the recent the work of Tobias Kaiser (Univ. Passau) establishing, for the categories of semi-algebraic functions, globally sub-analytic functions and more generally constructible functions on non archimedean real closed fields with archimedean value group, a full Lebesgue like integration theory.

May 26 (Friday), 3pm, room 6.2.33.

**MÁRIO EDMUNDO**

UNIVERSIDADE DE LISBOA

**Integration in non-archimedean real closed fields with archimedean value group (part 4)**

ABSTRACT :: In this seminar we present (some of) the recent the work of Tobias Kaiser (Univ. Passau) establishing, for the categories of semi-algebraic functions, globally sub-analytic functions and more generally constructible functions on non archimedean real closed fields with archimedean value group, a full Lebesgue like integration theory.

May 19 (Friday), 3pm, room 6.2.33.

**MÁRIO EDMUNDO**

UNIVERSIDADE DE LISBOA

**Integration in non-archimedean real closed fields with archimedean value group (part 3)**

ABSTRACT :: In this seminar we present (some of) the recent the work of Tobias Kaiser (Univ. Passau) establishing, for the categories of semi-algebraic functions, globally sub-analytic functions and more generally constructible functions on non archimedean real closed fields with archimedean value group, a full Lebesgue like integration theory.

May 12 (Friday), 3pm, room 6.2.33.

**ANDREW ARANA**

UNIVERSITY OF PARIS 1 PANTHÉON-SORBONNE AND IHPST

**Meaning and interpretation in mathematics**

ABSTRACT :: We articulate the view that mutually interpretable statements have identical meanings. We then argue against this view by showing that it would make unintelligible an important mathematical practice, namely that of purity of methods.

May 5 (Friday), 3pm, room 6.2.33.

**FERNANDO FERREIRA**

UNIVERSIDADE DE LISBOA

**A herbrandized functional interpretation**

ABSTRACT :: We introduce and study a functional interpretation that accumulates existential witnesses into finite sets. This semi-intuitionistic interpretation is able to realize the principles LLPO, WKL and the so-called FAN theorem. [This seminar is partly a repetition of material given in the first four SLM seminars of this year.]

April 28 (Friday), 3pm, room 6.2.33.

**MÁRIO EDMUNDO**

UNIVERSIDADE DE LISBOA

**Integration in non-archimedean real closed fields with archimedean value group (part 2)**

April 7 (Friday), 3pm, room 6.2.33.

**MÁRIO EDMUNDO**

UNIVERSIDADE DE LISBOA

**Integration in non-archimedean real closed fields with archimedean value group**

March 31 (Friday), 3pm, **room 6.2.38**.

**MICHÈLE FRIEND**

THE GEORGE WASHINGTON UNIVERSITY

**Rational Reconstructions. Making Sense of Proofs with Inconsistent Premises**

ABSTRACT :: Most mathematicians are classical or constructivist reasoners, so they think that contradictions lead to trivial theories, and the latter are disasters. Modern Western mathematicians make proofs. Often, these are only partly formal. Some of them use sets of premises that belong to theories that are inconsistent with each other. Some of them even use sets of premises that are inconsistent with each other in the stronger sense that it is possible to derive a contradiction from the premises. Even worse, few mathematicians seem perturbed by this. How do we explain the lack of concern? First note that almost none of these proofs use an ex contradictione quodlibet proof or sub-proof, since this would explicitly bring disaster. We could use a paraconsistent logic to reconstruct the reasoning, but this would be disingenuous towards the beliefs and practices of working mathematicians. As an alternative, we can use a proof reconstruction strategy called ‘chunk and permeate’, developed by Brown (2004, 2016). The proof is divided into several consistent chunks, and only some information from one chunk permeates to the next chunk. I explain the strategy in more detail. One problem that is still outstanding in the strategy is how to individuate consistent chunks. So far, this has been done intuitively. Following a suggestion by Abramsky et. al. (2015), we propose to make this less of an intuitive exercise by using bundle theory to represent chunks. In the conclusion, we discuss the limitations of this proposed solution to the outstanding problem. We then extend the method to include scientific reasoning. Finally, we draw some conclusions about the limitations of the method.

March 24 (Friday), 3pm, room 6.2.33.

**ANTÓNIO FERNANDES**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**Analytic determinacy (part 5 and last)**

ABSTRACT :: The purpose of this talk (eventually a series of talks) is to exhibit a proof (by Donald Martin) that analytic determinacy holds under a certain large cardinal hypothesis. In fact we intend to convey a little bit more than just the content of this proof, we will try to enlighten the deep connection between determinacy, which is a game related concept, and the theory of definable sets of reals.

March 17 (Friday), 3pm, room 6.2.33.

**ANTÓNIO FERNANDES**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**Analytic determinacy (part 4)**

ABSTRACT :: The purpose of this talk (eventually a series of talks) is to exhibit a proof (by Donald Martin) that analytic determinacy holds under a certain large cardinal hypothesis. In fact we intend to convey a little bit more than just the content of this proof, we will try to enlighten the deep connection between determinacy, which is a game related concept, and the theory of definable sets of reals.

March 10 (Friday), 3pm, room 6.2.33.

**ANTÓNIO FERNANDES**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**Analytic determinacy (part 3)**

ABSTRACT :: The purpose of this talk (eventually a series of talks) is to exhibit a proof (by Donald Martin) that analytic determinacy holds under a certain large cardinal hypothesis. In fact we intend to convey a little bit more than just the content of this proof, we will try to enlighten the deep connection between determinacy, which is a game related concept, and the theory of definable sets of reals.

March 3 (Friday), 3pm, room 6.2.33.

**ANTÓNIO FERNANDES**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**Analytic determinacy (part 2)**

February 24 (Friday), 3pm, room 6.2.33.

**ANTÓNIO FERNANDES**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**Analytic determinacy**

February 17 (Friday), 3pm, room 6.2.33.

**REINHARD KAHLE**

CMA & DM, FCT, UNIVERSIDADE NOVA DE LISBOA

**Hilbert's Larger Programme**

ABSTRACT :: In the foundations of mathematics, David Hilbert's name is associated, i.a., with the programmatic idea to carry out consistency proofs for formalized mathematical theories. It is well-known that Gödel's Incompleteness Theorems set limits to this programme which can only be exceeded by transcending the finitistic standpoint which was advocated by Hilbert for the time being. In our talk we relate this narrower Hilbert Programm with his original, much wider mathematico-philosophical concerns. We are able to identify a Larger Hilbert Programme which was successful from the beginning of proof theory till this day; these successes justify outright the philosophical status of mathematical logic as foundational base of mathematics. This talk is dedicated to the memory of Amílcar Sernadas, 1952-2017, who expressed a great admiration for Hilbert and whose work fits squarely in Hilbert's Larger Programme.

February 10 (Friday), 3pm, room 6.2.33.

**EMANUELE FRITTAION**

UNIVERSIDADE DE LISBOA

**Size-Change Termination in Reverse Mathematics (Part 4)**

ABSTRACT :: In [2] the authors address the reverse mathematics of Podelski and Rybalchenko termination theorem for transition based program. In a joint work with Silvia Steila, Keita Yokoyama, and Florian Pelupessy, we tackle the reverse mathematics of size-change termination (SCT), another tool in program analysis which supports automated termination proofs. Part of this work has been published in [1]. The project contributes to the reverse mathematics of termination analysis. We discuss two aspects of SCT: the (1) SCT criterion and the (2) SCT soundness. (1) gives a characterization of SCT that makes size-change termination suitable for automation. As usual, Ramsey's theorem for pairs turns out to play an essential role. (2) is simply the statement that "every SCT program terminates”. One of the motivations for studying (2) is that the (program for the) Peter-Ackermann function is easily (in fact provably in RCA0) seen to be SCT. [1] Emanuele Frittaion, Silvia Steila and Keita Yokoyama. The strength of the SCT criterion. Preprint at https://arxiv.org/abs/1611.05176. [2] Silvia Steila and Keita Yokoyama. Reverse mathematical bounds for the termination theorem. Annals of Pure Applied Logic, 167(12):1213–1241, 2016.

February 3 (Friday), 3pm, room 6.2.33.

**EMANUELE FRITTAION**

UNIVERSIDADE DE LISBOA

**Size-Change Termination in Reverse Mathematics (Part 3)**

ABSTRACT :: In [2] the authors address the reverse mathematics of Podelski and Rybalchenko termination theorem for transition based program. In a joint work with Silvia Steila, Keita Yokoyama, and Florian Pelupessy, we tackle the reverse mathematics of size-change termination (SCT), another tool in program analysis which supports automated termination proofs. Part of this work has been published in [1]. The project contributes to the reverse mathematics of termination analysis. We discuss two aspects of SCT: the (1) SCT criterion and the (2) SCT soundness. (1) gives a characterization of SCT that makes size-change termination suitable for automation. As usual, Ramsey's theorem for pairs turns out to play an essential role. (2) is simply the statement that "every SCT program terminates”. One of the motivations for studying (2) is that the (program for the) Peter-Ackermann function is easily (in fact provably in RCA0) seen to be SCT. [1] Emanuele Frittaion, Silvia Steila and Keita Yokoyama. The strength of the SCT criterion. Preprint at https://arxiv.org/abs/1611.05176. [2] Silvia Steila and Keita Yokoyama. Reverse mathematical bounds for the termination theorem. Annals of Pure Applied Logic, 167(12):1213–1241, 2016.

January 27 (Friday), 3pm, room 6.2.33.

**EMANUELE FRITTAION**

UNIVERSIDADE DE LISBOA

**Size-Change Termination in Reverse Mathematics (Part 2)**

ABSTRACT :: In [2] the authors address the reverse mathematics of Podelski and Rybalchenko termination theorem for transition based program. In a joint work with Silvia Steila, Keita Yokoyama, and Florian Pelupessy, we tackle the reverse mathematics of size-change termination (SCT), another tool in program analysis which supports automated termination proofs. Part of this work has been published in [1]. The project contributes to the reverse mathematics of termination analysis. We discuss two aspects of SCT: the (1) SCT criterion and the (2) SCT soundness. (1) gives a characterization of SCT that makes size-change termination suitable for automation. As usual, Ramsey's theorem for pairs turns out to play an essential role. (2) is simply the statement that "every SCT program terminates”. One of the motivations for studying (2) is that the (program for the) Peter-Ackermann function is easily (in fact provably in RCA0) seen to be SCT. [1] Emanuele Frittaion, Silvia Steila and Keita Yokoyama. The strength of the SCT criterion. Preprint at https://arxiv.org/abs/1611.05176. [2] Silvia Steila and Keita Yokoyama. Reverse mathematical bounds for the termination theorem. Annals of Pure Applied Logic, 167(12):1213–1241, 2016.

January 20 (Friday), 3pm, room 6.2.33.

**EMANUELE FRITTAION**

UNIVERSIDADE DE LISBOA

**Size-Change Termination in Reverse Mathematics (Part 1)**

January 13 (Friday), 3pm, room 6.2.33.

**EZGI SU**

UNIVERSIDADE DE LISBOA

**Epistemic equilibrium logic (part 2)**

ABSTRACT :: We add epistemic modal operators to the language of here-and-there (HT) logic, and deﬁne epistemic here and-there (EHT) models. We then successively deﬁne epistemic equilibrium models and autoepistemic equilibrium models. The former are obtained from EHT models by the standard ‘minimisation of truth’ of equilibrium logic; they provide an epistemic extension of that logic. The latter are obtained from the former by maximising the set of epistemic possibilities; they provide a new semantics for epistemic speciﬁcations (an epistemic extension of ASP). For both deﬁnitions we characterise strong equivalence by means of logical equivalence in EHT logic.

January 6 (Friday), 3pm, room 6.2.33.

**EZGI SU**

UNIVERSIDADE DE LISBOA

**Equilibrium logic (part 1)**

ABSTRACT :: Here-and-there (HT) logic is a three-valued monotonic logic which is intermediate between classical logic and intuitionistic logic. Equilibrium logic is a non-monotonic formalism whose semantics is given through a minimisation criterion over HT models. It is closely aligned with answer set programming (ASP), which is a relatively new paradigm for declarative programming. To spell it out, equilibrium logic provides a logical foundation for ASP: it captures the answer set semantics of (non-epistemic) ASP, and extends the restricted syntax of answer set programs to more general propositional theories, i.e., finite sets of propositional formulas. The underlying HT logic characterises an important notion of ASP, namely strong equivalence. In this talk, we will give a brief introduction of these formalisms with a focus on equilibrium logic.

December 16 (Friday), 3pm, room 6.2.33.

**ANA BORGES**

IST, UNIVERSIDADE DE LISBOA

**The strength of countable saturation**

ABSTRACT :: The countable saturation principle is common in nonstandard arguments. We will show that it is a consequence of the theory for nonstandard Heyting arithmetic presented in the last seminar. We use the herbrandised functional interpretation to show this. The second part of the seminar will be dedicated to the behaviour of the countable saturation principle in a classical setting. We will see that Peano arithmetic together with a version of the axiom of choice, idealization, and the countable saturation principle has exactly the strength of second order arithmetic. These results are due to Benno van den Berg et al [1]. [1] van den Berg, B., Briseid, E., and Safarik, P. The strength of countable saturation. arXiv:1605.02534, 2016.

December 9 (Friday), 3pm, room 6.2.33.

**ANA BORGES**

IST, UNIVERSIDADE DE LISBOA

**The herbrandised functional interpretation for nonstandard arithmetic**

ABSTRACT :: We present a functional interpretation for nonstandard Heyting arithmetic based on previous work by Van den Berg, Briseid and Safarik [1]. This interpretation enables the transformation of proofs in nonstandard arithmetic of internal statements into proofs in standard arithmetic of those same statements. The witnesses for external, existential statements of the interpreting formulas are functions whose output is a finite sequence. Syntactically, the terms representing these functions are called end-star terms. It is possible to define a preorder of end-star terms. The interpretation is monotone over this preorder: if a certain end-star term is a witness for an existential statement, then any “bigger” term also is. Using this property, we are able to prove a soundness theorem for the interpretation, which eliminates principles recognisable from nonstandard analysis. From this theorem, we get as corollary the conservativity of nonstandard arithmetic over standard arithmetic, as well as a term extraction theorem. [1] B. van den Berg, E. Briseid, and P. Safarik. A functional interpretation for nonstandard arithmetic. Annals of Pure and Applied Logic 163(2012), pp. 1962-1994.

December 2 (Friday), 3pm, room 6.2.33.

**MÁRIO EDMUNDO**

UNIVERSIDADE DE LISBOA

**Topology of definable sets in products of definable group-intervals**

ABSTRACT :: Eleftheriou, Peterzil and Ramakrishnan showed that definable groups in arbitrary o-minimal structures are definable in products of definable group-intervals. Thus understanding the topology of definable sets in products of definable group-intervals is crucial to complete our understanding of definable groups (in particular, by extending the proof of Pillay's conjecture to the general case). In this talk we will present a couple of results in this direction (joint work with Mamino, Prelli, Ramakrishnan and Terzo).

November 25 (Friday), 3pm, room 6.2.33.

**WAGNER SANZ**

UNIVERSIDADE DE GOIÁS (BRAZIL)

**Cut as a semantical principle**

ABSTRACT :: The rule of Cut in the sequent calculus is a cornerstone of proof-theory. Its eliminability in a calculus guarantees a series of nice properties of this calculus, like consistency via subformula principle, etc. It has been usually treated as a syntactical property. We defy such an assumption. The points we intend to claim are the following: (i) Cut is a semantical principle; (ii) The notion of hypothesis is intimately related to Cut; (iii) A nice semantics for intuitionistic propositional logic is obtained if we admit the concept of hypothesis as a primary concept; (iv) Kripke semantics is intensionally wrong; (v) the tableaux rules are an immediate reading of the semantical clauses.

November 18 (Friday), 3pm, room 6.2.33.

**BRUNO DINIS**

UNIVERSIDADE DE LISBOA

**Strong normalization and bar recursion (3)**

ABSTRACT :: In this talk we present a new method for proving strong normalization for higher type rewrite systems, due to Ulrich Berger [1], which makes use of a strict continuous domain-theoretic semantics. In order to understand Berger's method we start by showing, using essentially William Tait's method of strong computability [4], that a $\lambda$-calculus formulation of Gödel's T is strongly normalizing. The fact that Gödel's T is strongly normalizing is well-known and extensively studied in the literature. We give a brief introduction to Clifford Spector's bar recursion [3] and to some domain-theoretic notions and tools necessary to carry out the proof that Gödel's T extended with bar recursors is also strongly normalizing. Finally, we will discuss the possibility of adapting Berger's method to show a strong normalization theorem for an extension with bar recursors of a theory of Fernando Ferreira and Gilda Ferreira, presented in [2]. [1] U. Berger, Continuous Semantics for Strong Normalization. In S. B. Cooper, B. Löwe and L. Torenvliet, editors, New Computational Paradigms: First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, Springer Berlin Heidelberg, pp.23-34 (2005). [2] F. Ferreira and G. Ferreira, A herbrandized functional interpretation of classical first-order logic (manuscript). [3] C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In F. D. E. Dekker, editor, Recursive Function Theory: Proc. Symposia in Pure Mathematics. 5. American Mathematical Society. pp. 1-27 (1962). [4] W. Tait, Normal form theorem for barrecursive functions of finite type. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pp. 353-367. North-Holland, Amsterdam (1971).

November 11 (Friday), 3pm, room 6.2.33.

**BRUNO DINIS**

UNIVERSIDADE DE LISBOA

**Strong normalization and bar recursion (2)**

ABSTRACT :: In this talk we present a new method for proving strong normalization for higher type rewrite systems, due to Ulrich Berger [1], which makes use of a strict continuous domain-theoretic semantics. In order to understand Berger's method we start by showing, using essentially William Tait's method of strong computability [4], that a $\lambda$-calculus formulation of Gödel's T is strongly normalizing. The fact that Gödel's T is strongly normalizing is well-known and extensively studied in the literature. We give a brief introduction to Clifford Spector's bar recursion [3] and to some domain-theoretic notions and tools necessary to carry out the proof that Gödel's T extended with bar recursors is also strongly normalizing. Finally, we will discuss the possibility of adapting Berger's method to show a strong normalization theorem for an extension with bar recursors of a theory of Fernando Ferreira and Gilda Ferreira, presented in [2]. [1] U. Berger, Continuous Semantics for Strong Normalization. In S. B. Cooper, B. Löwe and L. Torenvliet, editors, New Computational Paradigms: First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, Springer Berlin Heidelberg, pp.23-34 (2005). [2] F. Ferreira and G. Ferreira, A herbrandized functional interpretation of classical first-order logic (manuscript). [3] C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In F. D. E. Dekker, editor, Recursive Function Theory: Proc. Symposia in Pure Mathematics. 5. American Mathematical Society. pp. 1-27 (1962). [4] W. Tait, Normal form theorem for barrecursive functions of finite type. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pp. 353-367. North-Holland, Amsterdam (1971).

November 4 (Friday), 3pm, room 6.2.33.

**BRUNO DINIS**

UNIVERSIDADE DE LISBOA

**Strong normalization and bar recursion**

ABSTRACT :: In this talk we present a new method for proving strong normalization for higher type rewrite systems, due to Ulrich Berger [1], which makes use of a strict continuous domain-theoretic semantics. In order to understand Berger's method we start by showing, using essentially William Tait's method of strong computability [4], that a $\lambda$-calculus formulation of Gödel's T is strongly normalizing. The fact that Gödel's T is strongly normalizing is well-known and extensively studied in the literature. We give a brief introduction to Clifford Spector's bar recursion [3] and to some domain-theoretic notions and tools necessary to carry out the proof that Gödel's T extended with bar recursors is also strongly normalizing. Finally, we will discuss the possibility of adapting Berger's method to show a strong normalization theorem for an extension with bar recursors of a theory of Fernando Ferreira and Gilda Ferreira, presented in [2]. [1] U. Berger, Continuous Semantics for Strong Normalization. In S. B. Cooper, B. Löwe and L. Torenvliet, editors, New Computational Paradigms: First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, Springer Berlin Heidelberg, pp.23-34 (2005). [2] F. Ferreira and G. Ferreira, A herbrandized functional interpretation of classical first-order logic (manuscript). [3] C. Spector, Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles in current intuitionistic mathematics. In F. D. E. Dekker, editor, Recursive Function Theory: Proc. Symposia in Pure Mathematics. 5. American Mathematical Society. pp. 1-27 (1962). [4] W. Tait, Normal form theorem for barrecursive functions of finite type. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, pp. 353-367. North-Holland, Amsterdam (1971).

November 3 (Thursday), 2pm, room 6.2.33. *Seminar hors-série.*

**JOOST JOOSTEN**

UNIVERSITAT DE BARCELONA

**Ordinal analysis based on iterated reflection, first order and beyond**

ABSTRACT :: Iteratively adding reflection principles or consistency statements to a weak base theory yields a paradigm for ordinal analysis: how often should we iterate to adequately approach a target theory? We revisit some basic early results obtained by Schmerl and then expose Beklemishev's uniform approach to computing these proof theoretical ordinals using provability logics. Towards the end of the talk we discuss the current state of the art looking at fragments of second order arithmetic and weak fragments of set theory.

October 28, 3pm, room 6.2.33

**JOÃO ENES**

UNIVERSIDADE DE LISBOA

**Predicative ordinal notations (II)**

ABSTRACT :: In this talk we will present the standard ordinal notation system for ordinals less than $\varepsilon_0$. We will introduce the Veblen hierarchy of functions based on the class of additively indecomposable ordinals. This will allow us to go beyond $\varepsilon_0$ and present a notation system for ordinals less than the Feferman-Schütte ordinal $\Gamma_0$.

October 21, 3pm, room 6.2.33

**JOÃO ENES**

UNIVERSIDADE DE LISBOA

**Predicative ordinal notations (I)**

ABSTRACT :: In this talk we will present the standard ordinal notation system for ordinals less than $\varepsilon_0$. We will introduce the Veblen hierarchy of functions based on the class of additively indecomposable ordinals. This will allow us to go beyond $\varepsilon_0$ and present a notation system for ordinals less than the Feferman-Schütte ordinal $\Gamma_0$.

October 14, 3pm, room 6.2.33

**FERNANDO FERREIRA**

UNIVERSIDADE DE LISBOA

**Modified realizability and functional interpretations: some logical and mathematical observations (conclusion)**

ABSTRACT :: We review some basic and well-known facts about the possibility of extracting computational information from proofs in classical, intuitionistic and semi-intuitionistic systems. Intuitionistic reasoning is tailored to have a clear constructive content and Kleene’s (numerical) realizability was a way of establishing precisely what this means for intuitionistic proofs in arithmetic. We review the variant of modified realizability due to Kreisel and see it as a form of a functional interpretation. An emphasis throughout is on the fact that there are some semi-intuitionistic principles which are amenable to computational extraction. Even Kreisel’s modified realizability displays not only the constructive content of intuitionistic logic but goes a bit further since it also realizes a certain (non-intuitionistic) principle of independence of premises. This principle is a characteristic principle of modified realizability. We explain what are these characteristic principles and compare them with so-called side principles, which are also amenable to computational extraction. Markov’s principle is a characteristic principle of Gödel’s functional dialectica interpretation. We review the dialectica interpretation and also analyze Markov’s principle via the so-called Friedman’s trick. We make a short comparison between both treatments of Markov’s principle. We introduce a new interpretation (the H-interpretation: H for herbrandized) and see that LLPO (the lesser limited principle of omniscience) is one of its characteristic principles. The extraction of computational information now takes the form of bounds, not of precise witnesses. We discuss this issue and a monotonicity condition now so central in several recently defined functional interpretations. Finally, we extend the H-interpretation to the second-order arithmetical setting in such a way that WKL (weak König’s lemma) turns out to be a characteristic principle. Some open questions and some projects will be discussed during the talk.

October 7, 3pm, room 6.2.33

**FERNANDO FERREIRA**

UNIVERSIDADE DE LISBOA

**Modified realizability and functional interpretations: some logical and mathematical observations (still continuation)**

ABSTRACT :: We review some basic and well-known facts about the possibility of extracting computational information from proofs in classical, intuitionistic and semi-intuitionistic systems. Intuitionistic reasoning is tailored to have a clear constructive content and Kleene’s (numerical) realizability was a way of establishing precisely what this means for intuitionistic proofs in arithmetic. We review the variant of modified realizability due to Kreisel and see it as a form of a functional interpretation. An emphasis throughout is on the fact that there are some semi-intuitionistic principles which are amenable to computational extraction. Even Kreisel’s modified realizability displays not only the constructive content of intuitionistic logic but goes a bit further since it also realizes a certain (non-intuitionistic) principle of independence of premises. This principle is a characteristic principle of modified realizability. We explain what are these characteristic principles and compare them with so-called side principles, which are also amenable to computational extraction. Markov’s principle is a characteristic principle of Gödel’s functional dialectica interpretation. We review the dialectica interpretation and also analyze Markov’s principle via the so-called Friedman’s trick. We make a short comparison between both treatments of Markov’s principle. We introduce a new interpretation (the H-interpretation: H for herbrandized) and see that LLPO (the lesser limited principle of omniscience) is one of its characteristic principles. The extraction of computational information now takes the form of bounds, not of precise witnesses. We discuss this issue and a monotonicity condition now so central in several recently defined functional interpretations. Finally, we extend the H-interpretation to the second-order arithmetical setting in such a way that WKL (weak König’s lemma) turns out to be a characteristic principle. Some open questions and some projects will be discussed during the talk.

September 30, 3pm, room 6.2.33

**FERNANDO FERREIRA**

UNIVERSIDADE DE LISBOA

**Modified realizability and functional interpretations: some logical and mathematical observations (continuation)**

ABSTRACT :: We review some basic and well-known facts about the possibility of extracting computational information from proofs in classical, intuitionistic and semi-intuitionistic systems. Intuitionistic reasoning is tailored to have a clear constructive content and Kleene’s (numerical) realizability was a way of establishing precisely what this means for intuitionistic proofs in arithmetic. We review the variant of modified realizability due to Kreisel and see it as a form of a functional interpretation. An emphasis throughout is on the fact that there are some semi-intuitionistic principles which are amenable to computational extraction. Even Kreisel’s modified realizability displays not only the constructive content of intuitionistic logic but goes a bit further since it also realizes a certain (non-intuitionistic) principle of independence of premises. This principle is a characteristic principle of modified realizability. We explain what are these characteristic principles and compare them with so-called side principles, which are also amenable to computational extraction. Markov’s principle is a characteristic principle of Gödel’s functional dialectica interpretation. We review the dialectica interpretation and also analyze Markov’s principle via the so-called Friedman’s trick. We make a short comparison between both treatments of Markov’s principle. We introduce a new interpretation (the H-interpretation: H for herbrandized) and see that LLPO (the lesser limited principle of omniscience) is one of its characteristic principles. The extraction of computational information now takes the form of bounds, not of precise witnesses. We discuss this issue and a monotonicity condition now so central in several recently defined functional interpretations. Finally, we extend the H-interpretation to the second-order arithmetical setting in such a way that WKL (weak König’s lemma) turns out to be a characteristic principle. Some open questions and some projects will be discussed during the talk.

September 23, 3pm, room 6.2.33

**FERNANDO FERREIRA**

UNIVERSIDADE DE LISBOA

**Modified realizability and functional interpretations: some logical and mathematical observations**

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

*The regular SLM meetings are finished for the 2015/2016 academic year. The seminars will resume in the end of September.*

June 8, 3pm, room 6.2.38

*NOTE THE CHANGE OF DAY AND ROOM*

**MARCELO E. CONIGLIO**

INSTITUTE OF PHILOSOPHY AND HUMAN SCIENCES CENTRE FOR LOGIC, EPISTEMOLOGY AND THE HISTORY OF SCIENCE UNIVERSIDADE DE CAMPINAS, BRAZIL

**Towards an hyperalgebraic theory of non-algebrizable logics: the case of mbC**

ABSTRACT :: Multialgebras (or hyperalgebras) have been very much studied in the literature. In the realm of Logic, they were considered by Avron and his collaborators under the name of non-deterministic matrices (or Nmatrices) as a useful semantics tool for characterizing some logics (in particular, several logics of formal inconsistency or LFIs) which cannot be characterized by a single finite matrix. In particular, these LFIs are not algebraizable by any method, including Blok and Pigozzi general theory. Carnielli and Coniglio introduced a semantics of swap structures for LFIs, which are Nmatrices defined over triples in a Boolean algebra, generalizing Avron's semantics. In this talk we develop the first steps towards the possibility of defining an algebraic theory of swap structures for LFIs, by adapting concepts of universal algebra to multialgebras in a suitable way. This is a joint work with Aldo Figallo-Orellano and Ana Claudia Golzio.

June 2, 3pm, room 6.2.33

**FILIPE CASAL**

INSTITUTO SUPERIOR TÉCNICO and CMAF-CIO, UNIVERSIDADE DE LISBOA

**Many-Sorted Equivalence of Shiny and Strongly Polite Theories**

ABSTRACT :: The Nelson-Oppen method allows the modular combination of quantifier-free satisfiability procedures of first-order theories into a quantifier-free satisfiability procedure for the union of the theories provided that these theories satisfy some conditions. In this talk, we will present the Nelson-Oppen techniques for stably infinite, shiny and strongly polite theories, and analyse the relationship between shiny and strongly polite theories in the many-sorted case. We show that, for theories with a decidable quantifier-free satisfiability problem, the set of many-sorted shiny theories coincides with the set of many-sorted strongly polite theories. Capitalizing on this equivalence, we obtain a Nelson-Oppen combination theorem for many-sorted shiny theories. Joint work with João Rasga.

May 19, 3pm, room 6.2.33

**LUÍS PEREIRA**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**O Teorema de Galvin-Hajnal em Aritmética Cardinal (4)**

ABSTRACT :: Este é o quarto e último seminário dedicado a uma apresentação de algumas técnicas utilizadas em aritmética cardinal. Nos três primeiros seminários viu-se como se demonstra a fórmula de Galvin-Hajnal no caso particular de cofinalidade mensurável. Neste seminário ver-se-á como adaptar algumas das noções mais importantes apresentadas nos seminários anteriores para demonstrar a fórmula de Galvin-Hajnal no caso geral de cofinalidade incontável.

May 12, 3pm, room 6.2.33

**LUÍS PEREIRA**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**O Teorema de Galvin-Hajnal em Aritmética Cardinal (3)**

ABSTRACT :: Neste seminário começaremos por recordar algumas noções apresentadas nos seminários anteriores. Em seguida veremos a construção de teoria de modelos dos ultraprodutos e utilizaremos um truque para a aplicar ao universo da teoria de conjuntos. Finalmente, veremos as aplicações à aritmética cardinal desta construção.

May 5, 3pm, room 6.2.33

**LUÍS PEREIRA**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**O Teorema de Galvin-Hajnal em Aritmética Cardinal (2)**

ABSTRACT :: Nestas duas palestras iremos ver a demonstração da fórmula de Galvin-Hajnal num caso particular, fácil e instrutivo, devido a Vopenka. Na primeira palestra começarei por rever noções básicas sobre números ordinais e cardinais e a noção de cofinalidade. Seguidamente, iremos ver algumas demonstrações, com técnicas elementares, de resultados clássicos da aritmética cardinal. Acabaremos revendo os resultados de independência obtidos imediatamente após a introdução da técnica de forcing por Paul Cohen (que lhe valeu a Medalha Fields em 1966) e resultados que se podem obter com técnicas clássicas que foram motivados pelos resultados anteriores. Na segunda palestra, após revisão das noções mais importantes referidas na primeira palestra, começarei por introduzir alguns grandes cardinais, tais como inacessível e mensurável. Após isso, apresentarei os conceitos básicos da construção de teoria de modelos dos ultraprodutos e finalmente acabaremos com a aplicação dessa técnica na demonstração da fórmula de Galvin-Hajnal.

**LUÍS PEREIRA**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**O Teorema de Galvin-Hajnal em Aritmética Cardinal**

ABSTRACT :: Nestas duas palestras iremos ver a demonstração da fórmula de Galvin-Hajnal num caso particular, fácil e instrutivo, devido a Vopenka. Na primeira palestra começarei por rever noções básicas sobre números ordinais e cardinais e a noção de cofinalidade. Seguidamente, iremos ver algumas demonstrações, com técnicas elementares, de resultados clássicos da aritmética cardinal. Acabaremos revendo os resultados de independência obtidos imediatamente após a introdução da técnica de forcing por Paul Cohen (que lhe valeu a Medalha Fields em 1966) e resultados que se podem obter com técnicas clássicas que foram motivados pelos resultados anteriores. Na segunda palestra, após revisão das noções mais importantes referidas na primeira palestra, começarei por introduzir alguns grandes cardinais, tais como inacessível e mensurável. Após isso, apresentarei os conceitos básicos da construção de teoria de modelos dos ultraprodutos e finalmente acabaremos com a aplicação dessa técnica na demonstração da fórmula de Galvin-Hajnal.

April 21, 3pm, room 6.2.33

**REINHARD KAHLE**

CMA and DM, FCT, UNIVERSIDADE NOVA DE LISBOA

**Schwichtenberg's Paradox in Dialogical Logic**

ABSTRACT :: Schwichtenberg observed that a naive understanding of the BHK (Brouwer-Heyting-Kolmogorov) interpretation leads to a trivial “proof" of Fermat's last theorem, as its forall clause only requires that one can verify the statement of Fermat's last theorem for all numerical instances. For a formalized version of BHK, Artemov resolved this problem by making use of an idea of Gödel. In this talk, we will show that the corresponding paradox for dialogical logic cannot be resolved in the same, but that it is an intrinsic problem for this framework. As conclusion we will argue that dialogical logic has to be considered as some kind of semantics rather than a framework allowing for derivations.

April 14, 3pm, room 6.2.33

**BRUNO DINIS**

UNIVERSIDADE DE LISBOA

**Do all Prawitz formulas enjoy instantiation overflow?**

ABSTRACT :: Instantiation overflow ensures that, in the atomic polymorphism system Fat, we can instantiate universal formulas by any formula of the system, not necessarily atomic. In a recent paper [1] the notion of Prawitz formula was introduced in order to study the phenomenon of instantiation overflow. It was shown that all formulas of level 0 and 1 have instantiation overflow and that there exists a Prawitz formula of level n with the same property, for each natural number n. It was however left open if all Prawitz formulas have instantiation overflow. In this talk I will present this problem and present new ideas on this matter. (This is joint work with Gilda Ferreira.) [1] B. Dinis and G. Ferreira - Instantiation overflow, to appear in Reports on Mathematical Logic.

April 7, 3pm, room 6.2.33

**IMME VAN DEN BERG**

UNIVERSIDADE DE ÉVORA

**Complete arithmetical solids and nonstandard analysis**

ABSTRACT :: Together with Bruno Dinis we developed an axiomatics for the external numbers of nonstandard analysis. The axioms are similar to, but somewhat weaker than the axioms for the real numbers and deal with algebraic rules, Dedekind completeness and the Archimedean property. A structure satisfying these axioms is called a complete arithmetical solid. We show that such a structure must have a built-in nonstandard model for the real number system.

March 31, 3pm, room 6.2.33

**PEDRO PINTO**

FACULDADE DE CIÊNCIAS, UNIVERSIDADE DE LISBOA

**A result relating the monotone functional interpretation and the bounded functional interpretation (part 4 and last)**

ABSTRACT:: Bounded functional interpretation was introduced by F. Ferreira and P. Oliva in [1] as an interpretation of Heyting arithmetic that greatly differs from Gödel's Dialectica interpretation. By a composition with a negative translation is possible to obtain a bounded interpretation of Peano arithmetic. In this talk we start by presenting a direct bounded functional interpretation of Peano arithmetic, [2]. Next we show a result by Kohlenbach relating his monotone interpretation and the bounded interpretation, [3]. More precisely, we show that over the model of the strongly majorizable functionals a solution for the bounded interpretation is also a solution for the monotone interpretation, although the latter uses the existence of an underlying precise witness. [1] F. Ferreira and P. Oliva, Bounded functional interpretation, Annals of Pure and Applied Logic 135, 73–112 (2005) [2] F. Ferreira, Injecting uniformities into Peano arithmetic, Annals of Pure and Applied Logic 157, 122–129 (2009) [3] U. Kohlenbach, A note on the monotone functional interpretation, Math. Log. Quart. 57, No.6, 611–614 (2011)

March 17, 3pm, room 6.2.33

**PEDRO PINTO**

FACULDADE DE CIÊNCIAS, UNIVERSIDADE DE LISBOA

**A result relating the monotone functional interpretation and the bounded functional interpretation (part 3)**

ABSTRACT:: Bounded functional interpretation was introduced by F. Ferreira and P. Oliva in [1] as an interpretation of Heyting arithmetic that greatly differs from Gödel's Dialectica interpretation. By a composition with a negative translation is possible to obtain a bounded interpretation of Peano arithmetic. In this talk we start by presenting a direct bounded functional interpretation of Peano arithmetic, [2]. Next we show a result by Kohlenbach relating his monotone interpretation and the bounded interpretation, [3]. More precisely, we show that over the model of the strongly majorizable functionals a solution for the bounded interpretation is also a solution for the monotone interpretation, although the latter uses the existence of an underlying precise witness. [1] F. Ferreira and P. Oliva, Bounded functional interpretation, Annals of Pure and Applied Logic 135, 73–112 (2005) [2] F. Ferreira, Injecting uniformities into Peano arithmetic, Annals of Pure and Applied Logic 157, 122–129 (2009) [3] U. Kohlenbach, A note on the monotone functional interpretation, Math. Log. Quart. 57, No.6, 611–614 (2011)

March 10, 3pm, room 6.2.33

**PEDRO PINTO**

FACULDADE DE CIÊNCIAS, UNIVERSIDADE DE LISBOA

**A result relating the monotone functional interpretation and the bounded functional interpretation (part 2)**

ABSTRACT:: Bounded functional interpretation was introduced by F. Ferreira and P. Oliva in [1] as an interpretation of Heyting arithmetic that greatly differs from Gödel's Dialectica interpretation. By a composition with a negative translation is possible to obtain a bounded interpretation of Peano arithmetic. In this talk we start by presenting a direct bounded functional interpretation of Peano arithmetic, [2]. Next we show a result by Kohlenbach relating his monotone interpretation and the bounded interpretation, [3]. More precisely, we show that over the model of the strongly majorizable functionals a solution for the bounded interpretation is also a solution for the monotone interpretation, although the latter uses the existence of an underlying precise witness. [1] F. Ferreira and P. Oliva, Bounded functional interpretation, Annals of Pure and Applied Logic 135, 73–112 (2005) [2] F. Ferreira, Injecting uniformities into Peano arithmetic, Annals of Pure and Applied Logic 157, 122–129 (2009) [3] U. Kohlenbach, A note on the monotone functional interpretation, Math. Log. Quart. 57, No.6, 611–614 (2011)

March 3, 3pm, room 6.2.33

**PEDRO PINTO**

FACULDADE DE CIÊNCIAS, UNIVERSIDADE DE LISBOA

**A result relating the monotone functional interpretation and the bounded functional interpretation**

25 de fevereiro, 16:30, sala 6.2.33

**ANA BORGES**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**Two functional interpretations of arithmetic: the ‘dialectica’ interpretation of Gödel and the monotone interpretation of Kohlenbach (conclusion)**

ABSTRACT:: In this talk we present two functional interpretations of arithmetic: Gödel's functional or `dialectica' interpretation and Kohlenbach's monotone functional interpretation, which is a modification of the first. On the way, we describe weakly extensional Heyting arithmetic in all finite types, Bezem's strong majorizability notion and Howard’s majorizability theorem.

18 de fevereiro, 16:30, sala 6.2.33

**ANA BORGES**

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

**Two functional interpretations of arithmetic: the ‘dialectica’ interpretation of Gödel and the monotone interpretation of Kohlenbach**

ABSTRACT:: In this talk we present two functional interpretations of arithmetic: Gödel's functional or `dialectica' interpretation and Kohlenbach's monotone functional interpretation, which is a modification of the first. On the way, we describe weakly extensional Heyting arithmetic in all finite types, Bezem's strong majorizability notion and Howard’s majorizability theorem.

11 de fevereiro, 16:30, sala 6.2.33**JOÃO ENES**

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA**Functional interpretation and inductive definitions (4)**

ABSTRACT:: In this talk we present the work by Jeremy Avigad and Henry Towsner [1] where they provide a functional interpretation of classical theories of positive arithmetic inductive definitions, along the lines of Gödel's "Dialectica" interpretation of first-order arithmetic, which reduces them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

[1] J. Avigad and H. Towsner. Functional interpretation and inductive definitions. J. Symbolic Logic, 74(4):1100–1120, 2009.

4 de fevereiro, 16:30

**LUIZ CARLOS PEREIRA**

Departamento de Filosofia, PUC-Rio/UERJ

**Revisiting Translations**

ABSTRACT:: In the late twenties and early thirties of last century several results were obtained connecting different logics and theories. These results assumed the form of translations/interpretations of one logic/theory into another logic/theory. In 1925 Kolmogorov defined a translation from classical logic into minimal logic aiming to show that “classical mathematics” can be translated into “intuitionistic mathematics”. In 1929 Glivenko proved two fundamental results connecting provability in classical propositional logic to provability in intuitionistic propositional logic. In 1933, Gödel and Gentzen independently defined an interpretation of Classical/Peano Arithmetic (PA) into Heyting’s arithmetic (HA). A preparatory step in Gödel’s interpretation establishes that classical propositional logic cannot be distinguished from intuitionistic propositional logic with respect to theorems in the fragment {~, &}. In 1933 Gödel also defined an interpretation of intuitionistic propositional logic into the classical modal logic S4. A minimum requirement for all these translations is that they preserve deducibility: Given two logics L1 and L2 and a translation T of L2 into L1, then S |-L2 A if and only if T[S] |-L1 T[A]. The aim of the present paper is to examine the following ideas and results concerning translations between logics and theories:

[1] The first result establishes that given two logics L1 and L2 and a translation of L2 into L1, then, given any intermediate logic L3 between L1 and L2, the same translation can be used to translate L2 into L3. It is also shown that this translation cannot be used to translate L3 into L1.

[2] The second group of results and ideas discusses the constructive behavior of different fragments of classical logic.

[3] In 1979, R. Statman showed a translation from intuitionistic propositional logic into its implicational fragment. This reduction is polynomial and proves that the implicational fragment of minimal Logic is PSPACE-complete. The methods that Statman used are based on proof-theory and Natural Deduction in Prawitz Style. The sub-formula principle for a propositional Natural Deduction system NL for a logic L states that whenever α is provable from Γ in L, there is a derivation of α from a set of assumptions {δ1, . . . , δk} ⊆ Γ built up only with sub-formulas of α and/or {δ1, . . . , δk}. We show that any propositional logic L, with a Natural Deduction system that satisfies the sub-formula principle has a translation to purely minimal implicational logic.

[4] The fourth group of results and ideas aims to discuss a view proposed by Dag Prawitz on the relation between intuitionistic and classical logic.

Work in collaboration with Edward Hermann Haeusler (Departamento de Ciência da Computação, PUC-Rio).

21 de janeiro, 16:30, sala 6.2.33

**JOÃO ENES**

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA

**Functional interpretation and inductive definitions (3)**

ABSTRACT:: In this talk we present the work by Jeremy Avigad and Henry Towsner [1] where they provide a functional interpretation of classical theories of positive arithmetic inductive definitions, along the lines of Gödel's "Dialectica" interpretation of first-order arithmetic, which reduces them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

[1] J. Avigad and H. Towsner. Functional interpretation and inductive definitions. J. Symbolic Logic, 74(4):1100–1120, 2009

14 de janeiro, 16:30, sala 6.2.33

**JOÃO ENES
FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA**

**Functional interpretation and inductive definitions (2)**

ABSTRACT:: In this talk we present the work by Jeremy Avigad and Henry Towsner [1] where they provide a functional interpretation of classical theories of positive arithmetic inductive definitions, along the lines of Gödel's "Dialectica" interpretation of first-order arithmetic, which reduces them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

[1] J. Avigad and H. Towsner. Functional interpretation and inductive definitions. J. Symbolic Logic, 74(4):1100–1120, 2009

14 de janeiro, 16:30, sala 6.2.33

**JOÃO ENES
FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA**

**Functional interpretation and inductive definitions (1)**

ABSTRACT:: In this talk we present the work by Jeremy Avigad and Henry Towsner [1] where they provide a functional interpretation of classical theories of positive arithmetic inductive definitions, along the lines of Gödel's "Dialectica" interpretation of first-order arithmetic, which reduces them to theories of finite-type functionals defined using transfinite recursion on well-founded trees.

[1] J. Avigad and H. Towsner. Functional interpretation and inductive definitions. J. Symbolic Logic, 74(4):1100–1120, 2009

3 de dezembro, 16:30, sala 6.2.33

**CRISTINA SERNADAS**

IST - UNIVERSIDADE DE LISBOA & CMAFCIO

**On probability and logic**

ABSTRACT:: Probabilistic entailment over the unchanged classical propositional language is shown to collapse into the classical entailment. Motivated by this result, a decidable conservative enrichment is proposed of propositional logic by providing the appropriate semantics to a new language constructor that allows the constraining of the probability of a formula. A sound and weakly complete axiomatization is provided by capitalizing on the decidability of Tarski’s theory of ordered real-closed fields. Joint work with Amilcar Sernadas and João Rasga.

**26 de Novembro, 16h30, sala 6.2.33**

**Imme Van Den Berg**

**Universidade de Évora – CIMA**

Logical aspects of axiomatic systems for external numbers (continuation)

ABSTRACT:: The external numbers of nonstandard analysis are the set of cosets with respect to all possible convex subgroups, called neutrices, of a nonstandard model of the reals; most of the neutrices are external sets.

The algebraic properties of external numbers were described by Koudjeti and Van den Berg in about 1995 and in some recent articles by Dinis and Van den Berg. They gave rise to so-called solids, which are extensions of ordered fields having a restricted distributivity law, however necessary and sufficient conditions can be given for distributivity to hold. The axioms for a solid do not characterize the external numbers, for a model can be found based on non-archimedean fields.

It is to be observed that attempts to extend Nelson's Internal Set Theory IST, or bounded versions of it, to deal with external numbers lead to classes and that an axiomatics characterizing the external numbers would characterize the reals, hence should depend on second-order logic.

To avoid serious foundational properties we remain within first-order logic, and extend the algebraic axioms of a solid with among others some axiom-schemes on generalized completeness and the archimedean property. We show consistency and show that, up to isomorphism, models are the set of cosets with respect to families of subgroups of a field between the nonstandard rationals and the nonstandard reals.

**NOVEMBER 12, 4:30pm, room 6.2.33**

**IMME VAN DEN BERG**

UNIVERSIDADE DE ÉVORA - CIMA

**Logical aspects of axiomatic systems for external numbers**

ABSTRACT:: The external numbers of nonstandard analysis are the set of cosets with respect to all possible convex subgroups, called neutrices, of a nonstandard model of the reals; most of the neutrices are external sets.

The algebraic properties of external numbers were described by Koudjeti and Van den Berg in about 1995 and in some recent articles by Dinis and Van den Berg. They gave rise to so-called solids, which are extensions of ordered fields having a restricted distributivity law, however necessary and sufficient conditions can be given for distributivity to hold. The axioms for a solid do not characterize the external numbers, for a model can be found based on non-archimedean fields.

It is to be observed that attempts to extend Nelson's Internal Set Theory IST, or bounded versions of it, to deal with external numbers lead to classes and that an axiomatics characterizing the external numbers would characterize the reals, hence should depend on second-order logic.

To avoid serious foundational properties we remain within first-order logic, and extend the algebraic axioms of a solid with among others some axiom-schemes on generalized completeness and the archimedean property. We show consistency and show that, up to isomorphism, models are the set of cosets with respect to families of subgroups of a field between the nonstandard rationals and the nonstandard reals.

**5 de Novembro, 16h30, sala 6.2.33**

**Gilda Ferreira**

CMAFCIO, ULisboa

**The computational content of atomic polymorphism (continuation)**

Abstract: The predicative variant of Girard's system F [3], known as the atomic polymorphic calculus or system F_at [1,2], has the exact same types as F, but a severe restriction on the range of the type variables: only atomic universal instantiations are allowed. It is known that system F_at is expressive enough to embed full intuitionistic propositional calculus (via a sound and faithful embedding) and has some nice proof-theoretic properties such as the strong normalization property, the subformula property and the disjunction property. In the present talk we report work in progress concerning the computational strength of F_at. Apparently, the functions representable in F_at are exactly the extended polynomials and thereof, in terms of computational content, atomic polymorphism yields no gain over simply typed lambda-calculus [4] except for some uniformity: integers have a unique representation instead of being indexed on a fixed type.

[1] F. Ferreira. Comments on Predicative Logic. Journal of Philosophical Logic, 35:1-8, 2006.

[2] F. Ferreira and G. Ferreira. Atomic Polymorphism. Journal of Symbolic Logic, 78(1):260{274, 2013.

[3] J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

[4] H. Schwichtenberg. Defi

nierbare Funktionen im lambda-kalkül Mit Typen. Arch. math. Logik, 17:113-114, 1976.

**OCTOBER 29, 4:30pm, room 6.2.33**

**LUÍS CAIRES**

NOVA Laboratory for Computer Science and Informatics

UNIVERSIDADE NOVA DE LISBOA

**Curry-Howard Interpretations of Typed Concurrent Computation**

ABSTRACT:: While type systems for traditional programming models have been for long rooted on pure logical principles, the connections between interactive and concurrent programming models and their logically motivated type disciplines started to be better understood only recently. In this talk, we review this line of research, based on linear logic interpretations, concluding with some recent developments related to non-deterministic computation.

OCTOBER 22, 4:30pm, room 6.2.33

**GILDA FERREIRA**

UNIVERSIDADE DE LISBOA

The computational content of atomic polymorphism

ABSTRACT:: The predicative variant of Girard's system F [3], known as the atomic polymorphic calculus or system F_at [1,2], has the exact same types as F, but a severe restriction on the range of the type variables: only atomic universal instantiations are allowed. It is known that system F_at is expressive enough to embed full intuitionistic propositional calculus (via a sound and faithful embedding) and has some nice proof-theoretic properties such as the strong normalization property, the subformula property and the disjunction property. In the present talk we report work in progress concerning the computational strength of F_at. Apparently, the functions representable in F_at are exactly the extended polynomials and thereof, in terms of computational content, atomic polymorphism yields no gain over simply typed lambda-calculus [4] except for some

uniformity: integers have a unique representation instead of being indexed on a fi xed type.

[1] F. Ferreira. Comments on Predicative Logic. Journal of Philosophical Logic, 35:1-8, 2006.

[2] F. Ferreira and G. Ferreira. Atomic Polymorphism. Journal of Symbolic Logic, 78(1):260{274, 2013.

[3] J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and Types. Cambridge University Press, 1989.

[4] H. Schwichtenberg. Defi nierbare Funktionen im lambda-kalkül Mit Typen. Arch. math. Logik, 17:113-114, 1976.

**OCTOBER 15, 4:30pm, room 6.2.33**

**JOÂO RASGA**

IST - UNIVERSIDADE DE LISBOA

**Preservation of admissible rules when meet-combining logics**

ABSTRACT:: Admissible rules are shown to be conservatively preserved by the meet-combination of a wide class of logics. A basis is obtained for the resulting logic from bases given for the component logics. Structural completeness and decidability of the set of admissible rules are also shown to be preserved, the latter with no penalty on the time complexity. Examples are provided for the meet-combination of intermediate and modal logics. The talk reports on joint work with Cristina Sernadas and Amílcar Sernadas.

**OCTOBER 8, 4:30pm, room 6.2.33**

**BRUNO DINIS**

UNIVERSIDADE DE LISBOA

Interpreting weak König's lemma in nonstandard theories (continuation)

ABSTRACT:: A number of nonstandard versions of Gödel's system T were recently developed. These systems are based on Nelson's IST version of nonstandard analysis. Not without surprise, these developments pointed out relations between constructive notions and nonstandard ones. A particular notion with constructive relevance is the well known weak König's lemma which establishes the existence of an infinite path in any infinite binary tree. In this talk we will show how weak König's lemma can be interpreted in the nonstandard theories of [1] and [2]. (Joint work with Fernando Ferreira.)

[1] B. van den Berg, E. Briseid, and P. Safarik., A functional interpretation for nonstandard arithmetic. Annals of Pure and Applied Logic, 163(12), 1962--1994, 2012.

[2] F. Ferreira and J. Gaspar., Nonstandardness and the bounded functional interpretation. Annals of Pure and Applied Logic, 166, 701--712, 2015.

SLM :: SESSION #1 :: THURSDAY, OCTOBER 1, 4:30pm ROOM 6.2.33

**BRUNO DINIS**

UNIVERSIDADE DE LISBOA

**Interpreting weak König's lemma in nonstandard theories**

ABSTRACT:: A number of nonstandard versions of Gödel's system T were recently developed. These systems are based on Nelson's IST version of nonstandard analysis. Not without surprise, these developments pointed out relations between constructive notions and nonstandard ones. A particular notion with constructive relevance is the well known weak König's lemma which establishes the existence of an infinite path in any infinite binary tree. In this talk we will show how weak König's lemma can be interpreted in the nonstandard theories of [1] and [2]. (Joint work with Fernando Ferreira.)

[1] B. van den Berg, E. Briseid, and P. Safarik., A functional interpretation for nonstandard arithmetic. Annals of Pure and Applied Logic, 163(12), 1962--1994, 2012.

[2] F. Ferreira and J. Gaspar., Nonstandardness and the bounded functional interpretation. Annals of Pure and Applied Logic, 166, 701--712, 2015.

2014/2015 - ano XXVI

SLM :: SESSION #17 :: THURSDAY, JULY 9, 4:30PM

**PEDRO PINTO
UNIVERSIDADE DE LISBOA**

**Elementary geometry and elementary arithmetic**

ABSTRACT::

The elementary (i.e., first-order) versions of geometry and arithmetic have quite different metamathematical properties. (Tarskian) elementary geometry is complete, decidable, and has a finitistic consistency proof whereas, as it is well-known, this is not the case with elementary (Peano) arithmetic. Moreover, elementary geometry is interpretable in elementary arithmetic, but not the other way around. We finish this talk with a brief comment on the metamathematics of the geometry as used by Euclid, reconstitued in a modern framework.

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA

ROOM: C6.2.38

SLM :: #15 :: THURSDAY, JUNE 25, 4:30PM

BRUNO DINIS

UNIVERSIDADE DE LISBOA

TITLE:: On instantiation overflow

ABSTRACT::

Since 2006 it is known that the restriction of Jean-Yves Girard's system F to atomic universal instantiations ( the atomic polymorphic system F_at) embeds the full intuitionistic propositional calculus. This embedding is possible due to the intriguing phenomenon of instantiation overflow. Instantiation overflow ensures that (in F_at) we can instantiate certain universal formulas by any formula of the system, not necessarily atomic. Until now only three types in F_at were identified with such property: the types that result from the Prawitz translation of the propositional connectives (bottom, and, or) into F_at (or Girard's system F). Are there other types in F_at with instantiation overflow? In this talk we show that the answer is yes and we isolate a class of formulas with such property.

[Trabalho em conjunto com Gilda Ferreira.]

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA

ROOM: C6.2.38

SLM :: #14 :: THURSDAY, JUNE 18, 4:30PM

GILDA FERREIRA

UNIVERSIDADE DE LISBOA

TITLE:: Atomic polymorphism: an overview

ABSTRACT::

Girard-Reynolds polymorphic lambda calculus, also known as system F, is an elegant system introduced in the early seventies with only two generators of types (formulas): implication and second-order universal quantification. Its impredicative feature - second-order quantifications may instantiate arbitrary types - explains the remarkable expressive power of F but also the difficulty of reasoning about the system.

In the present talk we are interested in a predicative variant of system F, known as the atomic polymorphic calculus, or system F_at. F_at has the exact same types (formulas) as F, but a severe restriction on the range of the type variables: only atomic universal instantiations are allowed. We present F_at and give an overview of some proof-theoretic properties of the system such as the strong normalization property, the subformula property, the sound and faithful embedding of the full intuitionistic propositional calculus into F_at, the disjunction property, etc. Moreover, we claim that F_at is the proper setting for the intuitionistic propositional calculus, avoiding this way the connectives bottom and disjunction, whose natural deduction elimination rules have been subject to harsh criticism, and avoiding the ad hoc commuting conversion needed in the usual presentation of the latter calculus.

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA

ROOM: C6.2.38

SLM ::12 THURSDAY, MAY 28, 4:30PM

MÁRIO EDMUNDO

UNIVERSIDADE ABERTA

TITLE:: Model theoretic approach to sub analytic geometry, both real and p-adic, with number theoretic applications II (continuation, still)

ABSTRACT::

In part I of the mini-course we will present the model theoretic proof of Gabrielov theorem of the complement in real sub analytic geometry. This model theoretic proof (due to Denef and van den Dries) is based on quantifier elimination (QE) method is shorter and more explicit then the original proof, it used Weierstrass preparation theorem and Tarski-Seidenberg QE for the real field. If time allows we will also present a (more geometric) proof of Tarski QE result.

In part II we will present the model theoretic proof (again due to Denef and van den Dries) of Hironaka's p-adic analogue of Gabrielov theorem. As before this other method is shorter, more explicit and based on Weierstrass preparation and Macintyre QE for the p-adic field.

In part III we will talk about the number theoretic applications of the above, respectively: (i) the recent new proof of Manin-Mumford (and in fact, extending the method, of Andre-Ort type conjectures) (Pila-Zanier, Pila-Wilkie, Peterzil-Starchenko); (ii) the old proof of rationality of the Poincaré series of closed analytic/algebraic sets of p-adic integers.

We hope to present the subject in a way accessible to everyone (including the speaker!), but with details and small exercises for the basic steps. Details and small exercises will probably not show up in part III.

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA

ROOM: C8.2.11

SLM :: SESSION #11 :: THURSDAY, MAY 21, 4:30PM

MÁRIO EDMUNDO

UNIVERSIDADE ABERTA

TITLE:: Model theoretic approach to sub analytic geometry, both real and p-adic, with number theoretic applications II (still continuation)

ABSTRACT::

In part I of the mini-course we will present the model theoretic proof of Gabrielov theorem of the complement in real sub analytic geometry. This model theoretic proof (due to Denef and van den Dries) is based on quantifier elimination (QE) method is shorter and more explicit then the original proof, it used Weierstrass preparation theorem and Tarski-Seidenberg QE for the real field. If time allows we will also present a (more geometric) proof of Tarski QE result.

In part II we will present the model theoretic proof (again due to Denef and van den Dries) of Hironaka's p-adic analogue of Gabrielov theorem. As before this other method is shorter, more explicit and based on Weierstrass preparation and Macintyre QE for the p-adic field.

In part III we will talk about the number theoretic applications of the above, respectively: (i) the recent new proof of Manin-Mumford (and in fact, extending the method, of Andre-Ort type conjectures) (Pila-Zanier, Pila-Wilkie, Peterzil-Starchenko); (ii) the old proof of rationality of the Poincaré series of closed analytic/algebraic sets of p-adic integers.

We hope to present the subject in a way accessible to everyone (including the speaker!), but with details and small exercises for the basic steps. Details and small exercises will probably not show up in part III.

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA

ROOM: C8.2.11

2014/2015 - ano XXVI

SLM :: SESSION #10 :: THURSDAY, MAY 14, 4:30PM

MÁRIO EDMUNDO

UNIVERSIDADE ABERTA

TITLE:: Model theoretic approach to sub analytic geometry, both real and p-adic, with number theoretic applications II (continuation)

ABSTRACT::

In part I of the mini-course we will present the model theoretic proof of Gabrielov theorem of the complement in real sub analytic geometry. This model theoretic proof (due to Denef and van den Dries) is based on quantifier elimination (QE) method is shorter and more explicit then the original proof, it used Weierstrass preparation theorem and Tarski-Seidenberg QE for the real field. If time allows we will also present a (more geometric) proof of Tarski QE result.

In part II we will present the model theoretic proof (again due to Denef and van den Dries) of Hironaka's p-adic analogue of Gabrielov theorem. As before this other method is shorter, more explicit and based on Weierstrass preparation and Macintyre QE for the p-adic field.

In part III we will talk about the number theoretic applications of the above, respectively: (i) the recent new proof of Manin-Mumford (and in fact, extending the method, of Andre-Ort type conjectures) (Pila-Zanier, Pila-Wilkie, Peterzil-Starchenko); (ii) the old proof of rationality of the Poincaré series of closed analytic/algebraic sets of p-adic integers.

We hope to present the subject in a way accessible to everyone (including the speaker!), but with details and small exercises for the basic steps. Details and small exercises will probably not show up in part III.

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA

ROOM: C8.2.11

2014/2015 - ano XXVI

SLM :: SESSION #7 :: THURSDAY, APRIL 23, 4:30PM

**MÁRIO EDMUNDO
UNIVERSIDADE ABERTA **

**Model theoretic approach to sub analytic geometry, both real and p-adic, with number theoretic applications (I, still continuation)**

ABSTRACT::

In part I of the mini-course we will present the model theoretic proof of Gabrielov theorem of the complement in real sub analytic geometry. This model theoretic proof (due to Denef and van den Dries) is based on quantifier elimination (QE) method is shorter and more explicit then the original proof, it used Weierstrass preparation theorem and Tarski-Seidenberg QE for the real field. If time allows we will also present a (more geometric) proof of Tarski QE result.

In part II we will present the model theoretic proof (again due to Denef and van den Dries) of Hironaka's p-adic analogue of Gabrielov theorem. As before this other method is shorter, more explicit and based on Weierstrass preparation and Macintyre QE for the p-adic field.

In part III we will talk about the number theoretic applications of the above, respectively: (i) the recent new proof of Manin-Mumford (and in fact, extending the method, of Andre-Ort type conjectures) (Pila-Zanier, Pila-Wilkie, Peterzil-Starchenko); (ii) the old proof of rationality of the Poincaré series of closed analytic/algebraic sets of p-adic integers.

We hope to present the subject in a way accessible to everyone (including the speaker!), but with details and small exercises for the basic steps. Details and small exercises will probably not show up in part III.

ROOM: C8.2.11

SLM :: SESSION #8 :: THURSDAY, APRIL 30, 4:30PM ROOM: C8.2.11

MÁRIO EDMUNDO

UNIVERSIDADE ABERTA

**Model theoretic approach to sub analytic geometry, both real and p-adic, with number theoretic applications (I, finalization)**

ABSTRACT::

In part I of the mini-course we will present the model theoretic proof of Gabrielov theorem of the complement in real sub analytic geometry. This model theoretic proof (due to Denef and van den Dries) is based on quantifier elimination (QE) method is shorter and more explicit then the original proof, it used Weierstrass preparation theorem and Tarski-Seidenberg QE for the real field. If time allows we will also present a (more geometric) proof of Tarski QE result.

In part II we will present the model theoretic proof (again due to Denef and van den Dries) of Hironaka's p-adic analogue of Gabrielov theorem. As before this other method is shorter, more explicit and based on Weierstrass preparation and Macintyre QE for the p-adic field.

In part III we will talk about the number theoretic applications of the above, respectively: (i) the recent new proof of Manin-Mumford (and in fact, extending the method, of Andre-Ort type conjectures) (Pila-Zanier, Pila-Wilkie, Peterzil-Starchenko); (ii) the old proof of rationality of the Poincaré series of closed analytic/algebraic sets of p-adic integers.

We hope to present the subject in a way accessible to everyone (including the speaker!), but with details and small exercises for the basic steps. Details and small exercises will probably not show up in part III.

FACULDADE DE CIÊNCIAS DA UNIVERSIDADE DE LISBOA

ROOM: C8.2.11