Computational Logic and Set Theory

Focusing on the groundbreaking contributions of Professor Jacob T. Schwartz, this text explores computational logic and set theory through the lens of proof verification techniques. It introduces the ÆtnaNova system, a prototype for verifying mathematical proofs in set theory. Key topics include leveraging first-order theories for reasoning in computer science and mathematics, automated proof verification for large software systems, and critical proof-engineering issues. An appendix provides formalized proofs of ordinals, transitive closure properties, induction principles, and Zorn's lemma.