Is ZF a hack? Comparing the complexity of some (formalist interpretations of) foundational systems for mathematics

DOI10.1016/j.jal.2005.10.011zbMath1114.03007OpenAlexW1510554082MaRDI QIDQ865658

Freek Wiedijk

Publication date: 20 February 2007

Published in: Journal of Applied Logic (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jal.2005.10.011

zbMATH Keywords

ZFChigher-order logiccalculus of constructionscategory theoryset theorytype theoryNew FoundationsMartin-Löf type theoryformalization of mathematicslogical frameworksHOLIsabelleZFNFAutomathfoundation of mathematicsZermelo-Fraenkel

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35)

Related Items

Formalizing an analytic proof of the prime number theorem, To be or not to be constructive, that is not the question, Unnamed Item, A formalization of multi-tape Turing machines, MECHANIZING PRINCIPIA LOGICO-METAPHYSICA IN FUNCTIONAL TYPE-THEORY, Formalising foundations of mathematics, Proof assistants: history, ideas and future, Operating system verification---an overview, Expander2: Program Verification Between Interaction and Automation

Uses Software

• Coq
• Isabelle
• HOL Light
• Twelf
• Automath

Cites Work

• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• A new implementation of Automath
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item