SUO: Re: Sorted languages/logics
Chris et al,
We are probably touching on a fundamental difference between my
"nonstandard" approach to first-order languages, models and theories and the
standard approach that you outline - Pat Hayes comments [The basic idea of
'model theory' as it is often called (a better term would be 'interpretation
theory')] notwithstanding. I actually use structures (models) and not
interpretations as the basic building block of my model theory, with a
first-order type language being one pole (the type half) of the structure
(one can define interpretation morphisms, but in a secondary way). This is
more abstract (and internal) and there is no syntax-semantics distinction -
in some sense, everything is semantic. That is why I use the consistent
terminology "entity type" and "relation type" in my notion of first-order
language.
Robert E. Kent
rekent@ontologos.org
----- 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: SUO: 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