Technical reports

Experimenting with Isabelle in ZF Set Theory

P.A.J. Noel

September 1989, 40 pages

DOI: 10.48456/tr-177

Abstract

The theorem prover Isabelle has been used to axiomatise ZF set theory with natural deduction and to prove a number of theorems concerning functions. In particular the axioms and inference rules of four theories have been derived in the form of theorems of set theory. The four theories are:

λ_βη, a form of typed lambda calculus with equality,

O_0, a form of simple type theory,

an intuitionistic first order theory with propositions interpreted as the type of their proofs,

PPλ, the underlying theory of LCF.

Most of the theorems have deen derived using backward proofs, with a small amount of automation.

Full text

PDF (2.2 MB)

BibTeX record

@TechReport{UCAM-CL-TR-177,
  author =	 {Noel, P.A.J.},
  title = 	 {{Experimenting with Isabelle in ZF Set Theory}},
  year = 	 1989,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-177.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-177},
  number = 	 {UCAM-CL-TR-177}
}