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