Abstract
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.
Article PDF
Similar content being viewed by others
Explore related subjects
Discover the latest articles, news and stories from top researchers in related subjects.Avoid common mistakes on your manuscript.
References
Aczel, P.: On relating type theories and set theories. In: Altenkirch, T., Naraschewski, W., Reus, B. (eds.) TYPES, Lecture notes in computer science, vol. 1657, pp 1–18. Springer (1998)
Agerholm, S., Gordon, M.: Experiments with ZF set theory in HOL and Isabelle. In: Proceedings of the 8th International Workshop on Higher Order Logic Theorem Proving and its Applications, LNCS, pp 32–45. Springer (1995)
Bancerek, G.: The ordinal numbers. Formalized Mathematics 1(1), 91–96 (1990). http://fm.mizar.org/1990-1/pdf1-1/ordinal1.pdf
Bancerek, G.: Sequences of ordinal numbers. Formalized Mathematics 1(2), 281–290 (1990). http://fm.mizar.org/1990-1/pdf1-2/ordinal2.pdf
Bancerek, G.: Algebra of morphisms. Formalized Mathematics 6(2), 303–310 (1997). http://fm.mizar.org/1997-6/pdf6-2/catalg_1.pdf
Bancerek, G., Hryniewiecki, K.: Segments of natural numbers and finite sequences. Formalized Mathematics 1(1), 107–114 (1990). http://fm.mizar.org/1990-1/pdf1-1/ finseq_1.pdf
Byliński, C.: Functions and their basic properties. Formalized Mathematics 1 (1), 55–65 (1990). http://fm.mizar.org/1990-1/pdf1-1/funct_1.pdf
Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5, 56–68 (1940)
DeMarco, M., Lipton, J.: Completeness and cut-elimination in the intuitionistic theory of types. J. Log. Comput. 15(6), 821–854 (2005)
van Heijenoort, J.: From Frege to Gödel. A source book in mathematical logic 1879–1931. Harvard University Press, Cambridge (1967)
Kaiser, J.: Formal Construction of a Set Theory in Coq. Master’s thesis, Universität des Saarlandes (2012)
The Coq development team: The Coq proof assistant reference manual. LogiCal Project (2012). http://coq.inria.fr. Version 8.4
Morse, A.P.: A theory of sets. Academic Press (1965)
Myhill, J.: Some properties of intuitionistic Zermelo-Fraenkel set theory. In: Mathias, A., Rogers, H. (eds.) 1971 Cambridge summer school in mathematical logic, Lecture Notes in Mathematics, vol. 337, pp 206–231. Springer, Berlin (1973)
Obua, S.: Partizan games in Isabelle/HOLZF. In: Barkaoui, K., Cavalcanti, A., Cerone, A. (eds.) ICTAC, Lecture Notes in Computer Science, vol. 4281, pp 272–286. Springer (2006)
Paulson, L.C.: Set theory for verification: I. from foundations to functions. J. Autom. Reason. 11, 353–389 (1993)
Prawitz, D.: Natural deduction: a proof-theoretical study. Dover (2006)
Russell, B.: The principles of mathematics. Cambridge University Press (1903)
Sĉêdrov, A.: Intuitionistic set theory. In: Harrington, A.S.L.A., Morley, M.D., Simpson, S. (eds.) Harvey Friedman’s research on the foundations of mathematics, Studies in Logic and the Foundations of Mathematics, vol. 117, pp 257–284. Elsevier (1985)
Suppes, P.: Axiomatic set theory. Dover (1972)
Trybulec, A.: Tarski Grothendieck set theory. Formalized Mathematics 1(1), 9–11 (1990). http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf
Zermelo, E.: Untersuchungen über die Grundlagen der Mengenlehre I. Mathematische Annalen 65, 261–281 (1908). English translation, “Investigations in the foundations of set theory” in [10], pages 199–215
Zermelo, E.: Über Grenzzahlen und Mengenbereiche. Fundamenta Mathematicae 16, 29–47 (1930)
Author information
Authors and Affiliations
Corresponding author
Rights and permissions
About this article
Cite this article
Brown, C.E. Reconsidering Pairs and Functions as Sets. J Autom Reasoning 55, 199–210 (2015). https://doi.org/10.1007/s10817-015-9340-6
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10817-015-9340-6