With the visits of Jouko Väänänen, Juliette Kennedy and Michael Harris, we will have a special Logic Day at Universidad Nacional de Colombia in Bogotá this next Monday, 15 January. This will be almost coincident with the World Logic Day!

404-212 (Edificio Yu Takeuchi – Departamento de Matemáticas)

---

Program

9:00 – Jouko Väänänen (University of Helsinki, University of Amsterdam)

Applications of set theory to infinitary model theory

Abstract: The basic question that I will be talking about is, whether the Scott-analysis of countable models can be extended to uncountable models? I will talk about the history and partial successes involved in trying to solve this problem. I will start with a review of what I call the Scott-analysis. Eventually I am led to the realm of Generalized Baire Spaces and to set theoretical problems arising from it.

10:15 – Juliette Kennedy (University of Helsinki)

Extracting syntax from semantics

Abstract: If a model class is a class of structures of the same similarity type closed under isomorphism, under what conditions can the class be said to have a natural syntax, or a natural logic? How to think about model classes that have no syntax, no notion of formula? More generally, does syntax always supervene on semantics? In this talk we present some old and new results dealing with these questions.

11:30 – Michael Harris (Columbia University, Université de Paris)

Understanding proofs (human and artificial)

Abstract:  The drive to incorporate methods of artificial intelligence in mathematics raises the possibility of the separation of proofs from understanding.  One can easily imagine a  formal proof that can be formally validated but not understood by anyone:  not by humans, either because the proof is written in impenetrable code or simply because it is too complex; not by machines, unless the term “understanding” is radically redefined .  It may be objected that many existing proofs are too long and intricate for any one person to understand.  Nevertheless, it is a common practice to invite the authors to explain such a proof in seminar talks, or for study groups to break down a proof into comprehensible chunks, so that one may speak of a collective (human) understanding.  My talk will try to imagine machine-made proofs that cannot be understood even in this way.  In the process, I will examine strategies by which mathematicians seek to make proofs understandable; how one might determine whether or not these strategies have been successful with a human audience; and what it would mean to test a machine’s understanding of a proof.