SUO: universal quantification and string division
All,
Pat Hayes gave the following example in a recent message:
> If a given relation symbol can have any (finite) number of arguments,
> how does one express a pattern of quantification on those arguments
> in a single expression? For example, suppose I want to say that R is
> functional in its last position, ie that
> (forall (?x ?y ?z)(implies (and (R ?x ?y)(R ?x ?z)) (= ?y ?z) ))
> when R has two arguments, but also
> (forall (?x ?x' ?y ?z)(implies (and (R ?x ?x' ?y)(R ?x ?x' ?z)) (= ?y
?z) ))
> when R has three arguments, and also
> (forall (?x ?x' ?x'' ?y ?z)(implies (and (R ?x ?x' ?x'' ?y)(R ?x ?x'
> ?x'' ?z)) (= ?y ?z) ))
> when R has four arguments, and so on.
> Obviously, I want to be able to say this for *any* number of
> arguments; and that is exactly what sequence quantifiers enable us to
> do:
>
> (forall (@x ?y ?z)(implies (and (R @x ?y)(R @x ?z)) (= ?y ?z) ))
>
> is equivalent in meaning to an infinite conjunction of universal
> quantifications all using normal variables.
The monoid of strings is not strong enough for an abstract theory of
automata -- in addition to concatenation (string multiplication) we also
need a string division operator with suitable axioms. Can this idea of
string division be helpful for defining the semantics of a universal
quantification over (with) row variables?
Let U be an underlying set (universe of discourse),
let U^n be the set of n-tuples of U-elements,
let U* = Union U^n be the set of U-strings,
let R (polyadic relation) be any subset of U-strings,
let w be any particular U-string.
Define the division R/w to be the set of all U-strings whose concatenation
of the right with w results in a string in R -- u is in R/w iff u*w is in R.
Define the following universal Boolean operator all-right(w)(r) on polyadic
relations:
all-right(w)(R) = 1, if R/w = U*
all-right(w)(R) = 0, otherwise.
That is, all-right(w)(R) is true when for all strings u it is true that u*w
is in R.
Make the similar definition for an operator all-left.
In general, we would need to replace R with an arbitrary expression.
Again, this is another bookmark, since I don't have time right now to check
whether this works meaningfully; that is, I don't know whether all-right is
meaningfully all right ;^).
Robert E. Kent
rekent@ontologos.org