# Re: [isabelle-dev] cardinality primitives in Isabelle/HOL?

```
> On 28 Dec 2018, at 19:36, Lawrence Paulson <l...@cam.ac.uk> wrote:
>
> Tons of useful stuff here.
>
> Some syntactic ambiguities, particularly around the =o relation, which is
> also defined as Set_Algebras.elt_set_eq.```
```
True. The same holds for +o and *o (which are less widely used in the ordinals
library).

I'm not sure what a good naming is in these cases. "=o" makes sense for me as
"equality on ordinals". It would be ok for me to play with capitalization or
other abbreviations of ordinals, e.g., "=O" or "=ord". Maybe Andrei can
comment, as he picked the current notation.

I don't know what "=o" stands for in the case of Set_Algebras.elt_set_eq (is
this a reference to the Oh-notation?) and why there is need for an alternative
notation for ∈. I believe the better textbooks are those that write "f ∈ O(g)"

Along similar lines, I find the notation "f <o g" in Set_Algebras extremely
confusing, because it is a function and not a relation. Thus, we get  terms
like "k <o g =o O(h)", which for me are hard to parse. Maybe something with a
minus (e.g., "-o"?) would be better here?

>
> I don’t suppose there’s any chance of using quotients to define actual
> cardinals and use ordinary equality?

Not really. "(=o) :: 'a rel ⇒ 'b rel ⇒ bool" is too polymorphic for this to
work properly.  (The relation arguments are ordinals represented by
well-orders.) One can quotient modulo a restricted relation "(=o) :: 'a rel ⇒
'a rel ⇒ bool", but then the equality on the quotient type won't allow us to
compare "|UNIV :: nat set| :: nat rel" to "|UNIV :: real set| :: real rel".

> And it still makes sense to introduce the actual notion of equipollence and
> similar relations.

This is the usual trade-off between many similar definitions with dedicated
reasoning support (transitivity, congruence, and monotonicity rules and such)
or a few core ones. Possibly an abbreviation is sufficient in this case.

Dmitriy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
```