From oleg-at-okmij.org Thu Dec 23 21:54:56 2004 Subject: The Axiom of Choice Message-ID: <20041224055456.52EA2A975@Adric.metnet.navy.mil> Date: Thu, 23 Dec 2004 21:54:56 -0800 (PST) Status: RO I was reading yesterday a wonderfully written Interlude in the book "Alfred Tarski, Life and Logic" (Anita Burdman Feferman, Solomon Feferman). I think I have finally understood the Axiom of Choice. It is a black-box API for a set. Suppose we have a set S -- and we know it is definitely a set, rather than a large class. The typical set API includes a membership predicate. Some say that the membership predicate is the whole representation of a set (if the domain of that predicate is a set as well). But that representation is wanting: all it gives us is the ability to test if a particular element of the domain is in our set, or not. We can't even find any element of our set, unless we correctly `guess' it. We can't even tell, in general, if our set is empty (if the membership predicate is `const False' and the domain is infinite, we will never find out for sure that our set is truly empty). One approach to that dilemma is white-box. We should be able to see how our set S has been constructed, via primitive operations (union, product, sum, selection, powerset) applied to the empty set or to the set of all natural numbers. We can then find an element of our set, or determine if the set is empty. Another approach is black-box. We can't see how our set is constructed. However, we are given a method that returns an element of the set. So, the Axiom of Choice is the extension of the set API with an extra function: Set e -> Maybe e. The Axiom of Choice lets us deal with sets extensionally. In that sense, the Axiom of Choice is quite natural (I never had any problem with it). In Datalog terms: a set Foo is represented by an unary predicate foo(X). Without the axiom of choice, this predicate is assumed unsafe -- that is, X must be fully instantiated by the time the predicate is called. So, we must use foo/1 only in the context domain(X), foo(X) where domain/1 enumerates the domain, e.g. domain(zero). domain(succ(N)) :- domain(N). The axiom of choice lets us assume that the predicate foo/1 is safe, so foo(X) can be used in any mode, whether X is bound or not. Come to think of it, the `msplit'* contraption can also be considered the manifestation of the Axiom of Choice. [*] Backtracking, Interleaving, and Terminating Monad Transformers (Functional Pearl), with Chung-chieh Shan, Daniel P. Friedman and Amr Sabry. ICFP'05. Addendum. Recently Neelakantan Krishnaswami in a message ``Re: FP-style map over set'' posted on a newsgroup comp.lang.functional on Mon, 28 Nov 2005 23:45:27 +0000 (UTC) introduced a choose function as an indispensable part of a set API. The function enables equational, algebraic reasoning about sets. The following is an extended excerpt from his message