Adding an Abstraction Barrier to ZF Set Theory

Research output: Chapter in Book/Report/Conference proceedingConference contribution

113 Downloads (Pure)


Much mathematical writing exists that is, explicitly or implicitly, based on set theory, often Zermelo-Fraenkel set theory (ZF) or one of its variants. In ZF, the domain of discourse contains only sets, and hence every mathematical object must be a set. Consequently, in ZF with the usual encoding of an ordered pair ⟨a,b⟩, formulas like {a} ∈ ⟨a,b⟩ have truth values, and operations like 풫(⟨a,b⟩) have results that are sets. Such `accidental theorems' do not match how people think about the mathematics and also cause practical difficulties when using set theory in machine-assisted theorem proving. In contrast, in a number of proof assistants, mathematical objects and concepts can be built of type-theoretic stuff so that many mathematical objects can be, in essence, terms of an extended typed λ-calculus. However, dilemmas and frustration arise when formalizing mathematics in type theory.

Motivated by problems of formalizing mathematics with (1) purely set-theoretic and (2) type-theoretic approaches, we explore an option with much of the flexibility of set theory and some of the useful features of type theory. We present ZFP: a modification of ZF that has ordered pairs as primitive, non-set objects. ZFP has a more natural and abstract axiomatic definition of ordered pairs free of any notion of representation. This paper presents axioms for ZFP, and a proof in ZF (machine-checked in Isabelle/ZF) of the existence of a model for ZFP, which implies that ZFP is consistent if ZF is. We discuss the approach used to add this abstraction barrier to ZF.
Original languageEnglish
Title of host publicationIntelligent Computer Mathematics. CICM 2020
EditorsChristoph Benzmüller, Bruce Miller
Number of pages16
ISBN (Electronic)9783030535186
ISBN (Print)9783030535179
Publication statusPublished - 2020

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


  • Formalisation of mathematics
  • Set theory
  • Theorem proving

ASJC Scopus subject areas

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Adding an Abstraction Barrier to ZF Set Theory'. Together they form a unique fingerprint.

Cite this