**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 2016/2017, 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

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