[FOM] Eliminability of AC

[Vaughan Pratt]

While I can't help with "well-known" in Joe Shipman's question about 
open problems that might need Choice, here's a very simply stated one, 
simple enough hopefully to make it of interest to more than just 
logicians and set theorists, that's been open for quite a while, with at 
least one contributor to this list who was producing deep results when I 
was still in college having spent some time on it (so it's at least 
"well-known" to that very limited extent).

Problem:  Is every T_1 comonoid discrete?

All countable T_1 comonoids are discrete, but the problem has been open 
for 13 years for the uncountable case, making it a reasonable candidate 
for an open problem that may require Choice to extend it to the 
uncountable case.

Definition of comonoid.  A *comonoid* (X,O) is a set X and a family O of 
"open" subsets of X that includes X and the empty set, such that for any 
subset S of X^2 whose rows and columns are in O, the diagonal of S is 
also in O.  Here a *row* of S is a set of the form {y in X | (x,y) in S} 
for some x in X, and dually for columns, while the *diagonal* of S is 
the set {x in X | (x,x) in S}.

(S can be pictured as a black-and-white XxX painting, a square matrix of 
1's and 0's, a binary relation on X, a directed graph with set X of 
vertices, an "open" subset of X^2, etc.)

Definition of T_1.  A comonoid (X,O) is *T_1* when for all distinct x,y 
in X, O contains a subset of X containing x but not y, and another 
containing y but not x.

(For comonoids that are topological spaces this coincides with the 
standard notion of T_1, as well as with the equivalent definition 
"discrete specialization order."  However the condition that all 
singletons be closed, while equivalent to the above for topological 
spaces, is not known to be equivalent to it for comonoids, though it 
would be equivalent in the event of a positive answer to the open problem.)

Definition of discrete.  The *discrete* comonoid on X is (X,2^X), just 
as for topological spaces.

Additional remarks:

*  If one thinks of a comonoid as a kind of topological space, it can be 
shown that O must be closed under finite union and finite intersection, 
making (X,O) "almost" a topological space, failing only the condition 
that O be closed under arbitrary union.  Defining "continuous function" 
by the evident analogy with topology spaces, another definition of 
comonoid is that (X,O) is a comonoid just when every binary operation 
f(x,y) on X^2 that is continuous separately in x and y is jointly 
continuous in x and y in the sense that f(x,x) is continuous on X.

*  Every directed CPO (DCPO) in the sense of Scott is both a topological 
space and a comonoid.  Every T_1 DCPO is discrete, but not every 
topological space, e.g. the continuum c with say the order topology. 
But c is not a comonoid, witness S the plane c^2 less all but one point 
(say the origin) of its diagonal, otherwise this problem would not be 
open since c is not discrete.

Vaughan Pratt

joeshipman at aol.com wrote:
> Any arithmetical statement provable in ZFC is provable in ZF; AC is 
> also eliminable from proofs of Pi^1_2 statements by Shoenfield 
> Absoluteness. What is the simplest example of a well-known open problem 
> in "ordinary mathematics" (that is, one of interest to mathematicians 
> in general and not primarily of interest to logicians and set 
> theorists) where there is a possibility some form of Choice is needed 
> for any proof?