Julin S (Feb 20 2022 at 05:50): 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.
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.
I found it here: https://link.springer.com/article/10.1007/BF01972461
Julin S (Feb 22 2022 at 17:05):Sam van G said:
I found it here: https://link.springer.com/article/10.1007/BF01972461
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)
I am thankful that we have access to it.
Julin S (Feb 22 2022 at 17:53):For the Tarski paper, I thought the year would have to be 1962. Didn't even check other years and missed this 1964 one.
Paolo Giarrusso (Feb 22 2022 at 17:58):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