finite.txt -- definition of finite sets

This file gives the axioms for defining finite sets of symbols and characters.


1. Finite Sets of Symbols (or Characters or Other Expressions) 

A finite set of symbols can be defined from a single expression of the form:

!  (finite_set <setname> (... element_symbols ...))

using the following axiom:

   (%set %elem)<                       ! <elem> is a member of <set> ...
     (finite_set %set ($1 %elem $2)).  ! if in list of elements for that set

For example, the axiom

   (finite_set day
       (Sunday Monday Tuesday Wednesday Thursday Friday Saturday)).

generates valid expressions such as (day Tue).
Some other examples are as follows:

   (finite_set month (January February March April May June
                      July August September October November December)).
   (finite_set boolean (false true)).

Our convention will be that the set name should be a symbol with the 
set elements usually symbols, but possibly characters.  (By symbol we mean
an expression of the form (<symbol_atom> <charseq>), where <symbol_atom>
is the atom that designates symbols (see file <symbol.txt> and <charseq>
is a sequence of characters (see <char.txt>.)  An example finite set
involving just characters is as follows:

   (finite_set digit "0123456789").

The set of element symbols or characters should be distinct.  A set name
symbol should only be used for one set, but it may be used for other purposes.
We allow the same element expression to be used in different finite sets.
(For example, (color orange) and (fruit orange).)

Note that these and other conventions are not enforced by axiomatic language.
However, some conventions might be supported by axioms themselves.  For
example, one might consider defining finite sets using the following axiom.

!  (%set %elem)<
!    (finite_set %set %elems),
!    (member %elem %elems),
!    (symbol %set).               ! forces set name to be a symbol
!       ! -- see other files for these predicates 

This axiom, of course, requires additional utility axioms to be defined
first.  For now we will disregard this axiom and just use the simpler one
above.  (*** Obsolete:  For one reason, we use the finite_set expression in
the definition of characters, so this axiom yields a circularity in the
definitions, which prevents any valid expressions from being generated!
For example, axioms P < Q . and Q < P . don't generate any valid expressions.)

A more useful, supplemental, axiom is the following:

!  (ERROR! "same element listed twice in finite set")
!     < (finite_set %set ($1 %elem $2 %elem $3)).
!  ERROR! < (ERROR! %msg).            *** move this to file <error.txt>!

   *** Note that we are assuming here that ! can be used as a symbol
       character if it is part of a symbol!

These axioms generate the symbol "ERROR!" as a valid expression if an element
is listed twice in the same set.  Other error checking axioms like this could
probably be defined.  We adopt the convention of generating the "ERROR!"
symbol if some erroneous conditions are satisfied that should not be.  For
now, however, we will not officially include these ERROR! axioms in this file.

Other predicates are generated from these finite_set expressions.
(See files <order.txt> and <index.txt>.)