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

[pat hayes]

>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?

I have no idea what this question means. The notion of predicate 
position is definable within the abstract syntax. Does that make it 
abstract enough?

>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 rather hard to follow, since it uses a large amount of auxiliary 
terminology.

>, 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.

I very much doubt that latter. You use "and" quite a lot in the 
English, for example.

>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?

The term 'predicate position' was used only in informal emails within 
the group, but it has a fairly crisp definition. It refers to a 
component of the abstract syntax, to wit, the relational term which 
is the head of an atomic sentence.

I have no idea what this has to do with symmetry or even if this 
answers your question. I am not sure what your question is, in fact.

Pat
-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes