> I've long imagined that Codd would have defined it (as you also did) via
> a cartesian product but some others like to use cardinality, eg., adding
> a "count" operation to their theory.  My guess is that they see this as
> something many implementations would want anyway.

>>Marshall wrote:

>>>...
>>>Hmmm. Can we express keyness otherwise? I can't think how.
>>>...

>>I've long imagined that Codd would have defined it (as you also did) via
>>a cartesian product but some others like to use cardinality, eg., adding
>>a "count" operation to their theory.  My guess is that they see this as
>>something many implementations would want anyway.

> I don't know why exactly but I have this vague aversion
> to using aggregate operators in constraints. I think I'm doing
> premature optimization, and should probably slap my own
> wrist for it, but I can't shake the feeling that given two ways to
> write a constraint, one using an aggregate, and one not, one
> should use the form without the aggregate.

> Of course, I can imagine how enforcing constraints with aggregates
> could be trivially easy. And aggregates, especially count, being
> as transparent as they are, I'm probably doubly in the wrong.

> Now that you mention it, a constraint that said that the count of
> a relation projected over the candidate key attributes equals
> the count of the unprojected relation would enforce uniqueness;
> that is, would also serve as a key constraint.

> (Happily I managed to avoid the word "keyness" in this post.)

>   forall R(a): exists S(b): a = b

> In the context of relations with named attributes, it is not necessary
> to declare or make up logic variable names, the way we have to when we
> are using sets of ordered pairs. We can use the existing attribute
> names as the names of the logic variables. However that raises the
> question of what happens when we want to quantify over an attribute
> more than once in a given formula. In that case let a primed attribute
> name be considered a second instance of a logic variable quantified
> over the attribute.
> So if we want to say that for every row of R
> with attribute a there exists a row of R with an unequal value
> for attribute a, we can say:

>   forall R(a): exists R(a'): a != a'

> What about candidate keys? Suppose we have a relation R with

>    A -> B

> that is the same as expressing that A is a candidate key.

>   R(a, b)
>   {a} -> {b} =def=
>     forall R(a, b): forall R(a', b'): a = a' => b = b'

> " For all rows (a,b) in R, and for all rows (a', b') in R,
>   if a = a', then b = b' "

> How does that look if R has many columns?

>   R{A, B}
>   A = {a1, ... an}
>   B = {b1, ... bn}

>   A -> B =def=
>     forall R(a1, ... an, b1, ... bn)
>       forall R(a1', ... an', b1', ... bn')
>         (a1 = a1' and ... and an = an') =>
>         (b1 = b1' and ... and bn = bn')

> Ugh, I wish that were simpler. But conceptually it's not too
> complex.

> It's always interesting and enlightening to consider the zero-case.
> Let's look at the B = {} case, and see how it turns out.

>   R{A, B}
>   A = {a1, ... an}
>   B = {}

>   A -> B =
>     forall R(a1, ... an)
>       forall R(a1', ... an')
>         (a1 = a1' and ... and an = an') => ()

> Hmm, what's that () doing? It's an empty conjunction, so we can
> replace it with true, which is the identity for and. But what does
> "implies true" really mean? Let's transform it.

> We know that (P => Q) <=> (!P or Q), so

>     forall R(a1, ... an)
>       forall R(a1', ... an')
>         !(a1 = a1' and ... and an = an') or true

> So we have a condition that ends with "or true" which is to say
> it is always true! In other words, the constraint collapses away
> and we are left with nothing. Which, when you think about it, is
> exactly what you would want: if A -> B, and B is empty, that just
> means that A is unique, and that's true by the definition of
> relation. So there shouldn't be anything to check.

>   R{A, B}
>   A = {}
>   B = {b1, ... bn}

>   A -> B =
>     forall R(b1, ... bn)
>       forall R(b1', ... bn')
>         () => (b1 = b1' and ... and bn = bn')

> transforming that last line:

>         !true or (b1 = b1' and ... and bn = bn')

> simplifying:

>         b1 = b1' and ... and bn = bn'

> What does that mean? For every two rows of R, every attribute
> is the same. That is to say, R has at most one row. Which again
> is exactly what you would expect from a uniqueness constraint
> on zero attributes.