<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
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.<br class="">
<br class="">
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: <a href="https://urldefense.com/v3/__https://listserv.gu.se/sympa/subscribe/nordiclogic__;!!IBzWLUs!ApnzhNt8RTIXnZMlC8xOjxnwJFA8CSy3_y2Qyeg6nsWQ54qGBQA41bdz6v73bYkwd84FIsdQ9Xrv-g$" class="">https://listserv.gu.se/sympa/subscribe/nordiclogic</a> .<br class="">
<br class="">
Val Goranko and Graham Leigh<br class="">
NOL seminar organisers <br class="">
<br class="">
--------------------------------------<br class="">
Nordic Online Logic Seminar<br class="">
<br class="">
Next talk: <b class="">Monday, February 28, 16.00-17.30 CET (UTC+1)</b>, on Zoom (details are provided to the seminar subscribers)<br class="">
Title: <b class="">Formalization of Mathematics and Dependent Type Theory</b><br class="">
Speaker: <b class="">Thierry Coquand</b>, professor in computer science at the University of Gothenburg, Sweden<br class="">
<br class="">
Abstract:<br class="">
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).<br class="">
<br class="">
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.
</body>
</html>