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.