[Prev][Next][Index]
Re: Grammars and Uncountable Sets
The set traits in LSL were written specifically to axiomatize the
properties of the abstract data type with constructors "emptySet" and "insert".
Since the sets constructed from finitely many applications of these operators
are themselves finite, the set traits were written to axiomatize the properties
of finite sets.
You are right that the relation trait can be used to reason about (both
countable and uncountable) infinite sets. But the set theory provided by the
relation trait is fairly weak, consisting essentially of the axioms defining a
boolean set algebra. If this is all you need, it might be more natural to
handcraft another version of the set trait, minus the "generated by", that
could be used to reason about set algebras without placing any restriction on
the sizes of the sets in those algebras.
The main difficulty in going beyond finite sets or set algebras lies in
devising axioms that ensure the existence of infinite sets without introducing
inconsistencies. Consider, for example, the problem of writing an axiom
describing the set of even natural numbers. The "natural" definition
n \in Even <=> n = 0 \/ (n - 2) \in Even
is consistent, but it is hard to find syntactic grounds that distinguish this
definition from the (incorrect and) inconsistent
n \in Even <=> ~(n \in Even)
There are well known axiomatizations of set theory (e.g., Zermelo-Frankel
or Godel-Bernays) that solve this problem, but at the expense of considerably
more machinery than is present in either the set or relation trait. So
simplicity is another reason why the set traits in LSL were written as they
were.
Reference(s):