[TYPES/announce] Nordic Online Logic Seminar: next talk on February 28 by Thierry Coquand

[Graham Leigh]

The Nordic Online Logic Seminar (NOL Seminar) is organised monthly over Zoom, with expository talks on topics of interest for the broader logic community. The seminar is open for professional or aspiring logicians and logic aficionados worldwide.

See the announcement for the next talk below. If you wish to receive the Zoom ID and password for it, as well as further announcements, please subscribe here: https://urldefense.com/v3/__https://listserv.gu.se/sympa/subscribe/nordiclogic__;!!IBzWLUs!ApnzhNt8RTIXnZMlC8xOjxnwJFA8CSy3_y2Qyeg6nsWQ54qGBQA41bdz6v73bYkwd84FIsdQ9Xrv-g$  .

Val Goranko and Graham Leigh
NOL seminar organisers

--------------------------------------
 Nordic Online Logic Seminar

Next talk: Monday, February 28, 16.00-17.30 CET (UTC+1), on Zoom (details are provided to the seminar subscribers)
Title: Formalization of Mathematics and Dependent Type Theory
Speaker: Thierry Coquand, professor in computer science at the University of Gothenburg, Sweden

Abstract:
The first part will be about representation of mathematics on a computer.Questions that arise there are  naturally reminiscent of issues that arise when teaching formal proofs in a basic logic course, e.g. how to deal with free  and bound variables, and instantiation rules. As discussed in a 1962 paper of Tarski, these issues are "clearly experienced both in teaching an elementary course in mathematical logic and in formalizing the syntax of predicate logic for some theoretical purposes." I will present two quite different approaches to this problem: one inspired by Tarski's paper (N. Megill, system Metamath) and one using dependent type theory (N.G. de Bruijn).

The second part will then try to explain how notations introduced by dependent type theory suggest new insights for old questions coming from Principia Mathematica (extensionality, reducibility axiom) through the notion of universe, introduced by Grothendieck for representing category theory in set theory, and introduced in dependent type theory by P. Martin-Löf.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://LISTS.SEAS.UPENN.EDU/pipermail/types-announce/attachments/20220216/ff1a4f50/attachment-0001.htm>