Publication details

Saarland University Computer Science

Reconsidering Pairs and Functions as Sets

Chad E. Brown

Technical Report, Saarland University, Technical Report of Article Submitted to Journal of Automated Reasoning, August 2013

We give representations for ordered pairs and functions in set theory with the property that ordered pairs are functions from the finite ordinal 2. We conjecture that these representations are useful for formalized mathematics since certain isomorphic sets are identified. The definitions, theorems and proofs have been formalized in the proof assistant Coq using only the simply typed features of Coq. We describe the development within the context of an intuitionistic simply typed (higher-order) version of (well-founded) Zermelo-Fraenkel set theory without the axiom of infinity.

Download PDF        Show BibTeX               


Login to edit


Webmaster, Wed Sep 16 10:47:00 2009