[SCL] another argument for the _complete_ SCL abstract syntax package

[Robert E. Kent]

SCLers,

I am in the midst of axiomatizing the FOL namespace for the IFF, which will
provide a bridge between the current IFF axiomatization for sorted logic and
the FOL aspect of the SCL. In this axiomatizing effort, as I can imagine in
the more practical-minded generation of program code for SCL, the value of
having _all_ components of the SCL abstract syntax (synthetic/constructor
operations, analytic/selector partial operations, analytic/selector domain
booleans, axioms for invertibility) has repeatedly come to light. To
paraphrase the current SCL document:

"It is important to observe that, because the (synthetic/constructor)
operations in a generator set for a formula class Fla(L) for L are all
one-to-one and disjoint in their ranges, every element of Fla(L) will have
exactly one decomposition under the inverses of those operations, and that
all such decompositions are finite."

The "inverses of those operations" are the analytic/selector operations, the
"disjoint ... ranges" is the analytic/selector domain partition, and correct
axiomatization (analogous to correct programming) requires a disjunction
over the analytic/selector domain partition of implications whose antecedent
will "test on domain" with the analytic/selector domain booleans before
applying the associated analytic/selector operations in the consequent.
These comments will make most sense to the folks directly involved in the
relevant axiomatization or programming.

Robert E. Kent
rekent at ontologos.org