A simplified framework for first-order languages and its formalization in Mizar

Marco B. Caminati

A strictly formal, set-theoretical treatment of classical first-order logic is given. Since this is done with the goal of a concrete Mizar formalization of basic results (Lindenbau…