FOM: A semantics for SOL

[Matt Insall]

I have a certain notion of semantics for SOL, which I am not certain is the
same as what Harvey is considering when he speaks of semantic SOL.  Please
tell me if the following is a reasonable description such a semantics.  It
appears to me to differ from either type of semantics presented in, for
example, Enderton's ``A Mathematical Introduction to Logic''.



Let S be a (relational) language of second order logic.  It has a countable
collection of variables, including countably many individual variables, as
well as countably many relation variables of each finite arity.  It may have
any number of individual constant symbols and relation constant symbols.
The connectives of S are `or', `and', `implies', `not', `iff'.  It has two
quantifier types, (Ax) and (Ex), for any variable x.  The structures of S
are tuples (A,c^A,R^A), where A is a class of objects, c^A is an arbitrary
function from the individual constant symbols of S into the class A and R^A
is an arbitrary function from the relation constant symbols into a class B
(described below) of finitary relations based on A for which if r is an
n-ary relation constant symbol, then R^A maps r to an n-ary relation which
is a member of B.  An interpretation I of the variables of S in a structure
(A,c^A,R^A) is a function from the class of variables of S into the class B
whose members are the members of A, together with all of the finitary
relations on A, or between members and relations on A, etc:  B is the union
of B_0,...,B_n,..., where B_0=A and for each natural number k, B_{k+1} is
the union of B_k with the class of subsets of B_k.  I stipulate that an
interpretation I must map any variable to an object in B of the appropriate
arity:  If a variable of S is intended to represent an element of the
domain, then the function I maps that variable to an element of A.  If a
variable of S is intended to represent an n-ary relation, then the function
I maps that variable to a subset of (B_k)^n, for some k.  (If n=2 and k=3,
for instance, then the function I maps that relation variable to a binary
relation on B_3, which is an element of the class of subsets of (B_3)x(B_3).
Each element of (B_3)x(B_3) is of the form {{a},{a,b}}, where a and b are
members of B_3.  Since for any a and b in B_3, {a} and {a,b} are members of
the power class of B_3, it follows that the ordered pair {{a},{a,b}} is a
member of B_5.  Thus every binary relation on B_3 which is a set is a subset
of B_6, and hence each such binary relation on B_3 is a member of B_7.
Therefore, if the function I maps a given binary relation variable r to a
binary relation on B_3 which is a set, then it maps r to an element of B_7.)

Now, a semantics for S will require a clear description of the language,
beyond the information I gave in the first four lines in the paragraph
above.  Here, an atomic formula is an expression of the form rx_1...x_n,
where r is either an n-ary relation constant symbol or an n-ary relation
variable, and x_1,...,x_n are variables or constant symbols (either relation
or individual constants or variables).  The remaining formulas are
constructed recursively from the atomic formulas in the usual manner (in
fact, in exactly the same manner as is done for a language of FOL).

Let (A,c^A,R^A) be a structure for S, and let I be an interpretation of the
variables of S in (A,c^A,R^A).  For an atomic formula rx_1...x_n of S, the
interpretation I satisfies rx_1...x_n in (A,c^A,R^A) if and only if one of
the following pertains
(i)  r is an n-ary relation constant and for each k, either x_k is a
variable and the function I maps x_k to b_k (in B) or x_k is a constant
symbol and the function c^A maps x_k to b_k (in B), and the tuple
(b_1,...,b_n) is in the relation to which r is mapped by R^A
(ii)  r is an n-ary relation variable and for each k, either x_k is a
variable and the function I maps x_k to b_k (in B) or x_k is a constant
symbol and the function c^A maps x_k to b_k (in B), and the tuple
(b_1,...,b_n) is in the relation to which r is mapped by the interpretation
I.

More generally, satisfaction of a formula p by an interpretation I in a
structure (A,c^A,R^A) is defined recursively in terms of satisfaction of
atomic formulas, just as in the FOL case.


[Note that the language appears to allow some forms of self-referential
semantics, which will be reduced or eliminated if my classes upon which my
structures are based come from a well-founded model of a class theory, such
as NBG.  What I mean by this is that formulas such as the atomic formula
rrr, where r is a binary relation symbol, will not be satisfied in any
structure by any interpretation if there are no membership cycles.  However,
for those who are willing to study non-well-founded classes, I believe this
leaves open the possibility that some such formulas would be realizable in
certain structures.  Personally, I prefer well-founded models of class
theory, and I am convinced that they can accomodate construction of models
that are not well-founded, if someone is inclined to study them.]









Dr. Matt Insall
http://www.umr.edu/~insall