# Mathematical Logic

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

EMANUELE FRITTAION

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.

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.

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

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.

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.

ALEXANDER USVYATSOV

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.

ALEXANDER USVYATSOV

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.

ALEXANDER USVYATSOV

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

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.

PEDRO PINTO

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.

MANUEL MARTINS

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)

EZGI SU

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

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

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

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.

MÁRIO EDMUNDO

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.

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.

FERNANDO FERREIRA

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

MÁRIO EDMUNDO

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

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.

MÁRIO EDMUNDO

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

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.

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.

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.

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.

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.

ANTÓNIO FERNANDES

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

Analytic determinacy (part 2)

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.

ANTÓNIO FERNANDES

INSTITUTO SUPERIOR TÉCNICO, UNIVERSIDADE DE LISBOA

Analytic determinacy

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.

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

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

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

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

Size-Change Termination in Reverse Mathematics (Part 1)

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 13 (Friday), 3pm, room 6.2.33.

EZGI SU

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Modified realizability and functional interpretations: some logical and mathematical observations

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.

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

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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

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

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

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

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

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.

ROOM: C6.2.38

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

BRUNO DINIS

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

ROOM: C6.2.38

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

GILDA FERREIRA

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.

ROOM: C6.2.38

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

MÁRIO EDMUNDO

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.

ROOM: C8.2.11

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

MÁRIO EDMUNDO

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.

ROOM: C8.2.11

2014/2015 - ano XXVI

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

MÁRIO EDMUNDO

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.

ROOM: C8.2.11

2014/2015 - ano XXVI

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

MÁRIO EDMUNDO

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

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.