## Abstract

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.

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 language | English |
---|---|

Title of host publication | Intelligent Computer Mathematics. CICM 2020 |

Editors | Christoph Benzmüller, Bruce Miller |

Publisher | Springer |

Pages | 89-104 |

Number of pages | 16 |

ISBN (Electronic) | 9783030535186 |

ISBN (Print) | 9783030535179 |

DOIs | |

Publication status | Published - 2020 |

### Publication series

Name | Lecture Notes in Computer Science |
---|---|

Volume | 12236 |

ISSN (Print) | 0302-9743 |

ISSN (Electronic) | 1611-3349 |

## Keywords

- Formalisation of mathematics
- Set theory
- Theorem proving

## ASJC Scopus subject areas

- Theoretical Computer Science
- Computer Science(all)