SUO: variables, of a sort

["Robert E. Kent" <rekent@ontologos.org>]

All,

 

As I indicated earlier [http://ltsc.ieee.org/logs/suo/msg01793.html] the variables in the current, rather nonstandard logical language, that I am using (my own design), are not quite the same as the sorted variables in the "standard" sorted logical language as described by Chris [http://ltsc.ieee.org/logs/suo/msg01792.html]. There are two main differences:

 

1. The set of variables is local and part of the language; different languages can have different sets of variables. One reason for this is that they are mainly used within the language to develop logical expressions. Another reason is that they do not play a central role in morphisms of languages, but only a subsidiary role.

 

2. Over the scope of the entire language, they are not required to have a single sort (entity type). They are only required to have a distinct sort within the expression of a relation. The advantage of this is the added flexibility when using relations within expressions. The disadvantage is that when forming Boolean combinations one must do a type check for compatibility.

 

Philosophically, I view every logical expression as a(n implicit) relation, and I want the collection of all expressions of a logical language L to represent a logical language Expr(L) that extends the original language - replace rel(L) with expr(L). This is an important goal and criteria that I have kept in mind when designing this version of language.

 

Again the definition of my nonstandard first-order type language (signature style) is as follows.

L = <ent(L), rel(L), var(L), arity_L, sign_L>

1. a set of entity types (sorts) ent(L).

2. a set of relation types rel(L).

3. a set of variables var(L).

4. an arity function arity_L : rel(L) -> power(var(L)), that maps a relation type to a set of variables.

5. a signature function sign_L : rel(L) -> tuple(ent(L)) that maps a relation type to a tuple of entity types, where arity(sign_L(rho)) = arity_L(rho) for each relation type rho in rel(L).

 

So if arity_L(rho) = {v_1, ..., v_n}, then sign_L(rho) is a function sign_L(rho) : arity_L(rho) -> ent(L), where sign_L(rho)(v_i) = some alpha_i in ent(L) for i = 1, ..., n.

 

For example, the relation declaration

    'carry(p : Person, o : Object)'

would have arity

    arity_L(carry) = {p, o}

and signature

    sign_L(carry)(p) = Person

    sign_L(carry)(o) = Object

 

From the standpoint of practical use, does anyone have any comments or suggestions?

 

Robert E. Kent
rekent@ontologos.org