|
One small advantage for my nonstandard language
definition, concentrated in the different notion of a variable
(perhaps these need a better name), is the independence from relational
position; so that the two inverse relations 'isMemberOf(Person, Organization)'
and 'hasMember(Organizarion, Person)' are one, with no need for the constraint
'inverse(isMemberOf, hasMember)'.
Robert E. Kent
----- Original Message -----
Sent: Thursday, October 26, 2000 12:23
PM
Subject: SUO: Re: Sorted
languages/logics
Chris,
In spirit your (and Enderton's) language (lexicon)
definition (shall we call this the standard definition?) and my (nonstandard)
language definition are in accord. However, they differ in the variables.
Although mine are sorted, they are strongly attached to relational parts, have
single sorts for each relation type, but may have multiple sorts when ranging
over all relations. The reason for a nonstandard definition is to be able to
defined categories of languages, models and theories that have good
properties. So my next question would be: what are the standard definitions
for lexicon morphisms and what properties do these
enjoy?
Robert
-----
Original Message -----
From: "Chris Menzel" <cmenzel@philebus.tamu.edu>
To: "Robert E. Kent" <rekent@ontologos.org>
Cc: "IEEE Standard Upper Ontology List" <standard-upper-ontology@ieee.org>
Sent: Thursday, October 26, 2000 11:16 AM
Subject: Sorted
languages/logics
> Robert wrote:
> > 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)).
>
> I'm a bit
uncertain of the content of your definition here, Robert,
> partly
because of the terminology you choose and also because the
> definition
is rather compressed and abstract (not that that is a bad
>
thing!). On terminology, I find it useful to reserve the words
>
"sort", "constant", "predicate", and "function symbol" for syntax and
>
the words "type", "entity" (or "object", or "individual"), "relation",
>
and "function" for the corresponding semantic notions. I think
this
> comports more or less with standard usage, but of course the
point is
> to use consistent terminology that helps us to avoid
confusions of
> syntax and semantics, whatever the actual
choices.
>
> Now, I think your definition agrees pretty well with
what I mean by a
> sorted language/logic; I'm just not certain of its
details. I also
> tend to think of things a little more concretely
and less
> algebraically than you do above. So let me just offer
my alternative,
> and then we can compare notes if need be. For
the record, I pretty
> much follow Enderton's text here (_A Mathematical
Introduction to
> Logic_). The definition is just a generalization
of the standard
> definition of a single-sorted
language.
>
> BASIC LEXICON
>
> Let S be a nonempty
set, whose members are called "sorts". The
> lexicon of a sorted
language L based on S will consist in the
> following:
>
> *
The usual logical stuff -- quantifiers (I'll use "forall"
and
> "exists" to make things concrete), boolean connectives
("not",
> "and", "=>", etc), parens
>
> * For
each s in S, a denumerable set Var_s of variables of sort
s.
> Var_s and Var_s' are disjoint unless s =
s'.
>
> * For each sort s, a possibly empty set of constants of
sort s.
>
> * For each sort s, an equality predicate of sort
<s,s>
>
> * For each n-tuple <s1,...,sn> of sorts, a
(possibly empty) set of
> predicates of sort
<s1,...,sn>.
>
> * For each n+1-tuple <s1,...,sn,sn+1>
of sorts, a (possibly empty) set
> of function symbols of
sort <s1,...,sn,sn+1>.
>
> TERMS AND
FORMULAS
>
> Terms and formulas are defined recursively as follows
(I'll continue
> to use KIF-ish syntax for the sake of
concreteness):
>
> If t1, ..., tn are terms of sorts s1,
..., sn, respectively, and f is
> a function symbol of sort
<s1,...,sn,sn+1>, then (f t1 ... tn) is a
> term of sort
sn+1.
>
> If P is a predicate of sort <s1,...,sn>, and t1,
..., tn are terms of
> sorts s1, ..., sn, respectively, then (P t1 ...
tn) is an (atomic)
> formula.
>
> Boolean combinations and
quantified formulas are defined as usual.
>
>
INTERPRETATIONS
>
> An interpretation I of a many-sorted language
L consists in
>
> * An assignment of a nonempty set (intuitively,
a type) T_s to each
> sort s in S. (Formally, the types needn't be
pairwise disjoint,
> though one might well impose this as an additional
constraint.)
>
> * An assignment of a member of T_s to each
constant or variable of
> sort s.
>
> * An assignment of a
function from T_s1 x ... x T_sn into T_sn+1 for
> each function symbol
of type <s1,...,sn,sn+1>.
>
> * An assignment of a subset of
T_s1 x ... x T_sn to each predicate of
> sort
<s1,...,sn>.
>
> TRUTH
>
> Atomic formulas and
boolean combinations are evaluated in the usual
> way in
I.
>
> Let v be a variable of sort s, and let A be any formula of
L. Then
> the universally quantified formula `(forall (v) A)' is
true in I iff,
> for every object e in T_s, A is true in I', where I' is
just like I
> except that I'(v) = e. Similarly for existentially
quantified
> formulas.
>
> PROOF THEORY
>
> All
the usual axioms of FOL restricted to types in the obvious ways
> and
the standard rules of inference.
>
>
> Robert
continues:
> > 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 |- .
>
> I'm not *certain* I
understand you here, but it just like you are
> talking about the
introduction of axioms of various kinds.
>
>
-chris
>
> --
>
> Christopher
Menzel
# web: philebus.tamu.edu/~cmenzel
> Philosophy, Texas A&M University
# net: chris.menzel@tamu.edu
> College Station, TX 77843-4237 #
vox:
(979) 845-8764
|