@incollection{goedel40, author = {Kurt G\"odel}, title = {The Consistency of the Axiom of Choice and of the Generalized Continuum Hypothesis with the Axioms of Set Theory}, booktitle = {{Kurt G\"odel}: Collected Works}, volume = {II}, editor = {S. Feferman and others}, publisher = {Oxford University Press}, year = 1990}, pages = {33-101}, note = {First published in 1940 by Princeton University Press}} @Book{kunen80, author = {Kenneth Kunen}, title = {Set Theory: An Introduction to Independence Proofs}, publisher = "North-Holland", year = 1980} @ARTICLE{paulson-consistency, author = {Lawrence C. Paulson}, title = {The Relative Consistency of the Axiom of Choice --- Mechanized Using {Isabelle/ZF}}, journal = {LMS Journal of Computation and Mathematics}, year = {2003}, volume = {6}, pages = {198-248}, note = {\url{http://www.lms.ac.uk/jcm/6/lms2003-001/}}, } @INPROCEEDINGS{paulson-reflection, author = {Lawrence C. Paulson}, title = {The Reflection Theorem: A Study in Meta-Theoretic Reasoning}, pages = {377-391}, editor = {Andrei Voronkov}, booktitle = {Automated Deduction --- {CADE}-18 International Conference}, year = 2002, series = {LNAI 2392}, publisher = {Springer}} }