Computing Reviews
Today's Issue Hot Topics Search Browse Recommended My Account Log In
Review Help
Search
Reconsidering pairs and functions as sets
Brown C. Journal of Automated Reasoning55 (3):199-210,2015.Type:Article
Date Reviewed: Dec 8 2015

In set theory, a pair (x,y) is normally described using Kuratowski’s representation {{x},{x,y}}. The set of all the pairs (x,y) in which x is from the set X and y is from the set Y is the Cartesian product X × Y. When X = Y, the Cartesian product is also represented as the square of the set X. This notation is somewhat ambiguous since in set theory, X to the power Y usually denotes the set of all functions from Y to X. This ambiguity is not a problem for working mathematicians, since the set of pairs X × X and the set of all functions from two to X are equivalent; however, this ambiguity creates serious complications for proof assistant programs.

To make these programs easier to apply, the author proposes changing the standard definition of a pair, defining a pair as a function from the set 2 = {0,1} to X. The author shows that this change can be relatively easily implemented within such well-known proof assistants as Coq. This change also necessitates a related change in how functions are defined, since usually a function f is defined as the set of corresponding pairs (x,f(x)).

This paper in mainly intended for logicians who are familiar with proof assistants, but it will be of interest to general mathematicians as well. It uses a simple example to show the unexpected complexity behind attempts to formalize seemingly simple notions and ideas.

Reviewer:  V. Kreinovich Review #: CR143996 (1602-0127)
Bookmark and Share
  Featured Reviewer  
 
Set Theory (F.4.1 ... )
 
Would you recommend this review?
yes
no
Other reviews under "Set Theory": Date
Set theory for computing: from decision procedures to declarative programming with sets
Cantone D., Omodeo E., Policriti A., Springer-Verlag New York, Inc., New York, NY, 2001.  409, Type: Book (9780387951973)
May 15 2002
Incomplete information: structure, inference, complexity
Demri S., Orlowska E., Orlowska E., Springer-Verlag New York, Inc., Secaucus, NJ, 2002.  450, Type: Book (9783540419044)
Jan 8 2003
Predicate abstraction of ANSI-C programs using SAT
Clarke E., Kroening D., Sharygina N., Yorav K. Formal Methods in System Design 25(2-3): 105-127, 2004. Type: Article
Apr 7 2005
more...

E-Mail This Printer-Friendly
Send Your Comments
Contact Us
Reproduction in whole or in part without permission is prohibited.   Copyright 1999-2024 ThinkLoud®
Terms of Use
| Privacy Policy