SUO: first-order languages and language morphisms (was: sorts, types and constraints)
John, Adam, Mike, Jon et al,
What I had in mind for sorts (I call these entity types, which are distinct
and disjoint from relation types) goes as follows.
A first-order type language (signature style) L = <ent(L), rel(L), var(L),
arity_L, sign_L> consists of entity types (sorts) ent(L), relation types
rel(L), variables var(L), arity function arity_L : rel(L) -> power(var(L)),
and signature function sign_L : rel(L) -> tuple(ent(L)). On entity types we
may place (monadic) sequent-style constraints of the form a1, ..., am |- b1,
..., bn, which include subtype (entailment) constraints a |- b, necessity
constraints |- b , covering constraints (exhaustive cases) |- b1, b2 ,
disjointness constraints (incompatibility types) a1, a2 |- , and incoherent
types a |- .
Between entity and relation types can be two maps in opposite directions: a
simple constraint-preserving entity to relation map e2r : ent(L) -> rel(L)
and a more difficult relation to entity (reification) map reify : rel(L) ->
ent(L) that in some manner preserves relational participants.
Perhaps this language definition would help alleviate Mike's concern about
"the essential distinction of interest between a unary predicate and an
n-ary predicate". From this definition it is reasonably straightforward to
define morphisms of first-order languages (getting a basic Language
category), which can be extended in several ways to "meaning-preserving
morphisms" (see John's response to Jon's note) between structures on the one
hand and theories on the other.
Robert E. Kent
rekent@ontologos.org
----- Original Message -----
From: "John F. Sowa" <sowa@bestweb.net>
To: "Robert E. Kent" <rekent@ontologos.org>;
<standard-upper-ontology@ieee.org>
Sent: Wednesday, October 25, 2000 8:14 PM
Subject: Re: SUO: sorts, types and constraints
> Robert,
>
> The 1998 draft of the KIF standard allows any monadic predicate
> to be used as a type or sort constraint. Following is the KIF
> translation of the sentence "Every cat is on a mat" using
> the 1998 notation for defining type or sort constraints:
>
> (forall ((?x cat)) (exists ((?y mat)) (on ?x ?y) ))
>
> The KIF manual (Section 6.3) defines the semantics of
> statement of this form by their translation to the
> equivalent statements without any such constraints:
>
> (forall (?x) (=> (cat ?x) (exists (?y)(and (mat ?y) (on ?x y) ))))
>
> There is no syntactic distinction in KIF between monadic
> predicates and sorts.
>
> John Sowa
----- Original Message -----
From: "apease" <apease@teknowledge.com>
To: "Robert E. Kent" <rekent@ontologos.org>;
<standard-upper-ontology@ieee.org>
Sent: Wednesday, October 25, 2000 4:45 PM
Subject: Re: SUO: sorts, types and constraints
> Robert,
> For reference, in the current version of SUO-KIF + "starter ontology",
> this would be expressed as
>
> (subclass-of person Organism) ; person is a subclass of organism
>
> (instance-of lives Relation) ; lives is a relation
>
> (nth-domain lives 1 Organism) ; the first argument to the lives relation
> must be an instance of Organism
>
> (nth-domain lives 2 Place) ; the second argument to the lives relation
must
> be an instance of Person
>
> (not
> (exists (?X)
> (and
> (instance-of ?X Organism)
> (instance-of ?X Place))))
> ; There is no such thing that is both an Organism and a Place
>
> (=>
> (instance-of ?O Person)
> (exists (?p)
> (and
> (instance-of ?P Place)
> (lives ?o ?p))))
> ; Every Person lives in some Place
>
> This is a reasonable example for discussion although I don't think any
form
> of these axioms should be in the SUO since parasites live on other
> organisms, and depending on how 'lives' is defined, there would be
homeless
> people that don't have a fixed abode.
>
> Adam
...
> -----------------
> Adam Pease
> Teknowledge
> (650) 424-0500 x571
>
>
----- Original Message -----
From: "Michael Uschold" <mfu@redwood.rt.cs.boeing.com>
To: <Matthew.R.West@is.shell.com>; <sowa@bestweb.net>;
<standard-upper-ontology@ieee.org>
Sent: Sunday, October 22, 2000 12:57 PM
Subject: RE: SUO: RE: Re: Starter Ontology Version 2
>
> John Sowa said:
>
> In logic, the words "relation" and "predicate" are commonly
> used as synonyms. A predicate in predicate calculus can
> represent absolutely anything in the ontology -- including
> things that are often called "objects","activities", "events",
> "agents", "people", "cats", "dogs", and "the universe".
>
> The words "predicate" and/or "relation" are metalanguage
> terms about the language of KIF, predicate calculus, CGs, or
> whatever. They are not part of the subject matter that is
> being modeled.
> ====
>
> John, I think your comments miss the essential distinction of
> interest between a unary prediace and an n-ary predicat where
> n is more than 1. It is rare to refer to a unary predicate as
> a relation. The word 'relate' implies one thing being in some
> relatinship with another thing.
>
> M<ike
----- Original Message -----
From: "John F. Sowa" <sowa@bestweb.net>
To: "Jon Awbrey" <jawbrey@oakland.edu>; <sowa@bestweb.net>; "Jay Halcomb"
<jhalcomb@teknowledge.com>; <standard-upper-ontology@ieee.org>
Sent: Wednesday, October 25, 2000 4:17 PM
Subject: Re: SUO: Re: KIF & Re: Naming Problems
>
> Jon,
>
> That is a fair question, and my answer is based on the
> definition of _proposition_ that I give in Section 5.3
> of the KR book. In fact, it is the kind of definition for
> which category theory, which you often recommend, would be
> the ideal formalism to apply. I did not use category theory
> in the KR book for the simple reason that explaining it and
> developing enough formalism to enable students to use it
> would overwhelm most of the book.
>
> >OK, but a theory is a set of 'sentences',
> >and a sentence is a syntactic construct
> >that is bound to a particular 'alphabet'
> >of primitive tokens as actually scribed.
> >
> >So the concept of a 'theorem' is already an abstract type,
> >whose extension as a sort of scattergram cluster within the
> >framework of a concrete and a particular 'discursive universe',
> >in effable effect, as realized within a particular formal language,
> >is already the sort of object that requires some rather fancy morphism
> >mechanics just say what the heck we might mean by the apparently or the
> >ostensibly natural equivalence of 'same theorem in a different language'.
>
> On p. 289, I define the notion of a "meaning-preserving
> translation f from a language L1 to a language L2". Note
> that the character string "meaning" is just part of the name
> of the kind of translating morphism I am defining, not itself
> a formally defined term.
>
> In summary, such a translation must be invertible, proof
> preserving, vocabulary preserving, and structure preserving.
> And the languages L1 and L2 might be the same language.
> On pp. 291-293, I give examples of such functions which
> maps L1 (predicate calculus with Peano's symbols) to L2
> (Peirce's notation of 1885). I also discuss the mapping
> from L2 to L3 (Peirce's existential graphs).
>
> The function f4 (or its equivalent adapted to other notations)
> is one that I would recommend for mapping between the various
> notations for FOL I discussed in the previous note.
>
> Then a proposition is defined as an equivalence class of
> sentences that is preserved under mappings by f4 to and from
> the various languages.
>
> I'll extract some snippets from Ch. 5 of my KR book and
> put them in another note.
>
> John Sowa