[SCL] Simplified SCL model theory presentation

[Pat Hayes]

Guys, greetings

Spurred by Tanel's inability to understand the 'folding semantics' 
write-up, here's an alternative way to present the model theory. (In 
some ways this goes back to old ideas of Chris' from, when was it, 2 
years ago now?)  Note, this does NOT change the syntax or the notion 
of satisfiability (or, hence, proof theory) of SCL, only the 
presentation of the MT. So let me know if y'all think this might be 
easier to follow than the 'folding maps' stuff.

This might be very similar to the 'moderately folded' semantics that 
Robert described recently: I havnt yet checked this in detail.

Background first. There is a central issue here, a tension between 
two semantic requirements which pull in opposite directions.

A. SCL interpretations have to be able to give relation and function 
extensions to any name, since any name can be used as a relation or a 
function.
B. However, if some name is in fact ONLY used as a relation (in some 
piece of SCL text) and not as an individual name, then the MT should 
not *require* that it denote an individual in all interpretations of 
that text.
C. Similarly, if some name is never used as a relation or a function, 
then there is no need to assign a relational or functional meaning to 
it, and any such assignment is 'irrelevant' extraneous structure in 
an interpretation. So it would be better if an interpretation was not 
*obliged* to exhibit this extraneous structure.

C does not affect satisfiability but is still desireable, since there 
are meta-results in model theory which could be harmed by irrelevant 
clutter.

Chris' old MT basically followed A by making all names refer and 
giving everything both a relational and functional extension; but 
ignored B and C. This is certainly the simplest one to describe.  The 
'folding maps' MT in the current draft tries to respect B and C but 
needs to use a recursive construction on the universe to ensure that 
'enough' extensions are provided to give a denotation for every 
possible term, to satisfy A. (It has to be a recursion because it 
depends on the particular syntax in the text being interpreted. ) 
This recursion makes the MT more awkward and less similar to a 
conventional FOL MT and, apparently, harder to follow.

So here's the idea: use the old, simpler, construction but allow the 
universe of quantification to be a subset of the 'full universe'. 
This deals adequately with A and B but not with C.  So to handle C, 
we have a notion of a 'pruned interpretation' which is a different 
kind of interpretation with all extraneous structure removed, ie what 
is here called 'folded'.  The folding recursions which clutter up the 
current MT are only needed here, to define the minimal structure, so 
can be ignored unless someone is really interested in MT details.
Key lemmas include
*Irrelevance Lemma: if J prunes into I then J|=T iff I|=T. In other 
words, the surplus structure is irrelevant.
*GOFOL Lemma: If T is GOFOL text then I is a conventional FO 
interpretation of T iff there is an SCL interpretation J of T which 
prunes into I.
In other words, for GOFOL text, SCL exactly mirrors conventional FO 
interpretations.

The main MT is then as follows:  An SCL interpretation I of a text T 
wrt a vocabulary V is a set U with a distinguished nonempty subset D 
and three mappings Rel:U -> 2|(D*), Fun:U -> (D* ->D), I: V -> U 
(n.b. , U not D) which satisfies:

If a is a denoting name in T (ie a name in a denoting position, i.e. 
as an argument) then I(a) is in D
I(Atom_[x x1 ... xn]) = T iff <I(x1)...I(xn)> in Rel(I(x))
I(Term_[x x1 ... xn]) = Fun(I(x))(I(x1)...I(xn) )
.....
(conventional MT from this point on but with D (not U) being the 
domain of the quantifiers.)

This handles A because everything in U has both a relational and a 
complete functional extension, for every arity (this was Chris' old 
CL MT construction).  This is almost a conventional MT. The only 
textual sensitivity that it uses is in the first condition.  We need 
only the idea of a denoting name for this.  (This is exactly the 
names that Tanel would use his second kind of equality on.)  All 
function extensions are total on D for every arity, so we can state 
all the truth-conditions straightforwardly without worrying about 
empty terms (nod to Chris at this point.)

It also handles B (ie the Horrocks sentence issue) because in a GOFOL 
text, relation and function names are not denoting and so their 
denotations aren't required to be in the universe D. (They are in U, 
but that's larger than the universe.) This is kind of trivial, and 
hardly needs stating formally, but we can illustrate it with an 
example.

It doesn't handle C, since there is lots of irrelevant structure. 
Symbols used only in relation or function position don't need 
individuals attached and can be mapped directly to their extensions, 
and individuals that play no relational or functional role don't need 
extensions.  So we can define a 'pruning' that throws all this 
irrelevant stuff away and produces a leaner meaner kind of 
interpretation, which we can even consider to be the 'official' 
interpretation structure. This will require being careful along the 
lines of the fold mappings and the syntactic recursions following the 
text; but we can handle this in an appendix for model theorists, 
where we go into the folding recursions. The appendix also should 
prove the basic result about pruning not affecting satisfiability, 
which is why you don't have to even think about it unless you are 
interested in more than just satisfiability.

I'll get this HTMLized asap.  Comments welcomed at any time, of course.

Pat

PS. This also provides a neat way to characterize the two SCL-> FOL 
embedding styles. The direct way to embed SCL into FOL is 
context-sensitive, since it translates an atom (P...) differently 
depending on whether or not P occurs in a denoting position in the 
text, ie whether or not I(P) is required to be in D. The 'uniform' 
style amounts to the claim that U=D, and so translates everything the 
same way; but at the cost of possibly putting things into the 
universe that wouldnt have been there in the original text. If this 
cost is bearable, fine. If not, you have to either be sensitive to 
the text or else to introduce an explicit predicate to encode the 
original D and restrict all your quantifiers to it.


-- 
---------------------------------------------------------------------
IHMC	(850)434 8903 or (650)494 3973   home
40 South Alcaniz St.	(850)202 4416   office
Pensacola			(850)202 4440   fax
FL 32501			(850)291 0667    cell
phayes at ihmc.us       http://www.ihmc.us/users/phayes