[SCL] Is the notion of predicate position abstract or abstractable?

[Robert E. Kent]

SCL Folk,

Examples in the SCL specification (and other realms) are very important in
getting our abstractions correct. I have been bothered for some time about
our desire for abstraction in the SCL (witness the SCL abstract syntax
discussion) and the notion in the SCL spec regarding "predicate position",
which seems intuitively to be a rather concrete notion. The question
bothering me can be summarized as "Is the notion of predicate position
either abstract as it stands or in some sense abstractable? The nice example
about symmetric binary relations has been used in the SCL spec to illustrate
the advantage of quantifying over the "predicate position". To wit:

----------------------------------------
(forall (?x ?y ?r)
    (implies (symmetric ?r)
             (implies (?r ?x ?y)
                      (?r ?y ?x))))
----------------------------------------

Now consider the following more abstract expression of this axiom.

----------------------------------------
Background generic framework:
----------------------------------------
Binary relations are abstract objects. They are elements of some
set-theoretic class Rel of all small binary relations. As such, two binary
relation can be identified, or they can be isomorphic to each other through
some bijection on Rel, and neither of these may hold. Binary relations can
be identified through their components. Each binary relation has a first set
and a second set, which correspond to the elements that can occur in the
first place or second place, respectively, in a concrete expression such as
"r(a,b)". The two set components of binary relation are realized by two
set-theoretic class functions
set1 : Rel --> Set
set2 : Rel --> Set
where Set is the set-theoretic class of all small sets. Every binary
relation has an associated extent set consisting of all those pairs that
satisfy the relation. This component is realized by the set-theoretic class
function
ext : Rel --> Set
and an inclusion function
incl : Rel --> Ftn
where Ftn is the set-theoretic class of all functions between small sets,
and for any relation the source set of the inclusion of the relation is the
extent and the target set is the set-theoretic binary product of the first
and second sets of the relation. Any two binary relations are identical when
their (set1, set2, ext) triples are equal. For any two sets there is a twist
function between the binary product of the first set and the second set and
the binary product of the second set and the first set. A binary relation is
an endorelation when the first and second component sets are equal.
----------------------------------------
Specific formalization:
----------------------------------------
A binary relation is *symmetric* when it is an endorelation and its
inclusion function is invariant under right composition with the twist
function of its two set components.
----------------------------------------

Now this expression for symmetry is rather large, and the above KIF-like
expression is certainly more economical. But, I want to make two points --
well one point and one question. First, this rather large abstract natural
language expression for symmetry can be formalized, in a formalization that
is most definitely in the metalevel, with much of the formalization being
part of a generic framework usable for other notions, but at the same time
the formalization does not use quantifiers or logical connectives. Second,
does the notion of "predicate position" exist in this abstract (either
natural language or formal logic) expression of symmetry? And if so, what is
its manifestation?

Robert E. Kent
rekent at ontologos.org