Comment by tromp

Jeremy Avigad made available a 54-page draft chapter on mathematical logic and foundations [1]. Quoting from the abstract:

> The formal foundation of a proof assistant is the formal deductive system with respect to which the correctness of the proof assistant’s implementation is judged. The foundation specifies a language for defining objects and saying things about them, and it determines the means that can be used to prove that such statements are true. This chapter presents some general background in logic that is helpful for thinking and reasoning about formal systems, and it describes the three main families of foundations that are commonly used in proof assistants today.

[1] https://arxiv.org/abs/2009.09541