# Publication details

##
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

@TECHREPORT{Brown2013,
title = {Reconsidering Pairs and Functions as Sets},
author = {Chad E. Brown},
year = {2013},
month = {Aug},
institution = {Saarland University},
note = {Technical Report of Article Submitted to Journal of Automated Reasoning},
}

Login to edit

Webmaster,
Wed Sep 16 10:47:00 2009