[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Hi. I saw in the types-announce[2] mailing list about a talk by Thierry Coquand as part of the Nordic Online Logic Seminar. I'm sort of new to logic and type theory and was trying to find papers that would help me understand the talk better. The abstract was: > 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[1]? [1]: https://urldefense.com/v3/__http://us.metamath.org/downloads/metamath.pdf__;!!IBzWLUs!GgCWS35KVAXOBGITv9G363gRbkyb18vD4--hSnWLV-gywkE2s4FtPjLKBnsWe-MrlCqCOSshYmI$ [2]: http://lists.seas.upenn.edu/pipermail/types-announce/2022/010050.html Thanks and regards, Julin Shaji