## Stream: Miscellaneous

### Topic: Help finding papers for NOL talk

#### Julin S (Feb 20 2022 at 05:50):

Saw here about a talk by Thierry Coquand that is to happen on February 28 as part of Nordic Online Logic Seminars. The talk title is 'Formalization of mathematics and dependent type theory'.

The talk description for it is:

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.

Could anyone help me find the papers/works that this abstract may be referring
to (and anything else that can be helpful to better understand the talk)?

I tried searching for these on google scholar but couldn't pinpoint the papers.

• 1962 paper by Tarksi
• Tarski's paper (N. Megill, system Metamath)
• dependent type theory (N. G. de Bruijn)

Could metamath be this?

#### Paolo Giarrusso (Feb 20 2022 at 08:11):

That's the same metamath I'd think; while de Bruijn's system is probably Automath

#### Enrico Tassi (Feb 20 2022 at 12:00):

is the talk online? I could not find it.

#### Sam van G (Feb 20 2022 at 12:02):

If I understood correctly, it's happening on Zoom in eight days, and you can register to the mailing list to receive the Zoom link.

#### Julin S (Feb 22 2022 at 04:19):

Does anyone know which is the 1962 paper by Tarski mentioned in the abstract? I guess it's something really famous, but couldn't find it.

#### Sam van G (Feb 22 2022 at 10:04):

Julin S said:

Does anyone know which is the 1962 paper by Tarski mentioned in the abstract? I guess it's something really famous, but couldn't find it.

Sam van G said:

Thanks!

#### Julin S (Feb 22 2022 at 17:06):

I got the article but it shows that we need to cough up 34,95 € just to see the document.
(Sounds way too much)