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.
Could metamath be this?
That's the same metamath I'd think; while de Bruijn's system is probably Automath
is the talk online? I could not find it.
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.
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.
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.
I found it here: https://link.springer.com/article/10.1007/BF01972461
Sam van G said:
I found it here: https://link.springer.com/article/10.1007/BF01972461
Thanks!
I got the article but it shows that we need to cough up 34,95 € just to see the document.
(Sounds way too much)
I am thankful that we have access to it.
For the Tarski paper, I thought the year would have to be 1962. Didn't even check other years and missed this 1964 one.
You might want to search for alternative sources. Since none of that money would go to the authors, many recommend sci-hub.
Last updated: Dec 05 2023 at 11:01 UTC