[SCL] Re: Folding unnecessary [was: Re: Update to SCL-related work]

[Pat Hayes]

>Pat Hayes wrote:
>
>>>Pat Hayes wrote: It does provide an answer (which is correct but not ideal)
>>>but your explanations made me hope that perhaps the folding stuff
>>>is not so horrendous as it initially seemed.
>>>
>>>If it can be presented in an understandable and simple way and
>>>really has all the nice effects you describe, would be really neat.
>>>
>>>BTW, could you briefly comment on whether the following approach
>>>is exactly folding or is there something different:
>>>
>>>Suppose we normally convert P(x) in SCL
>>>to Atom_2(P,x) in abstract syntax, which is really
>>>just traditional FOL.
>>>
>>>Then we want to have completely conventional
>>>FOL in SCL as well (without forcing these Atom_N or App etc
>>>to be used in FOL translation) so we also allow to write P(x) in abstract
>>>syntax, i.e traditional FOL.
>>>
>>>The P in the first abstract syntax expression
>>>Atom_2(P,x) is, of course, completely different from
>>>P in the second abstract syntax expression P(x).
>>
>>
>>If you write it this way, yes. But they should not be independent, 
>>is the point, because they are punned from a single symbol which 
>>should play the same role when it occurs in the same kind of 
>>position (as a relation name, in this case.)
>>
>>>In order to make these two P-s equivalent in some sense,
>>>we axiomatise explicitly that for any two abstract syntax expressions
>>>Atom_2(P,x) and P(x),  it always holds that they are equivalent.
>>>
>>>This is simply my intuitive hypothesis of how to understand
>>>folding on top of conventional FOL semantics,
>>>but I am a bit unsure whether it is a correct reading.
>>
>>
>>I think it is right, yes.  Its easy (trivial) for relations, but 
>>functions introduce new complications because one has to guarantee 
>>that any constructible term will have a denotation even if the term 
>>is not explicitly exhibited in the text.  There are cases where the 
>>conditions have to be applied to things that are themselves denoted 
>>by terms but not directly by names in the vocabulary, eg the case 
>>like
>>
>>((((f a) b) c)
>>
>>where f has to be a function whose value is a function whose value 
>>is a relation, but there need be no actual name for this relation. 
>>Nevertheless we have to somehow guarantee that it exists in any 
>>interpretation.
>
>
>I'll try to make it clearer for myself here.
>
>First I'll write SCL: (((f a) b) c) in FOL with
>app/holds:
>
>(1)  (holds2 (app2 (app2 f a) b) c)
>
>Now I write the "folding axiom" for f:
>
>(foreach (x y) (= (f x) (app2 f x)))
>
>Once we have that axiom, the formula (1)
>is equivalent to
>
>(2) (holds2 (app2 (f a) b) c)
>
>and there seems to be nothing more left to be done.

Ah, I see what is missing. There are two aspects to the MT. The fold 
maps ensure that P means the same when it is used purely as a 
relation and when it denotes something. That is straightforward, 
trivial in a purely relational logic (no functions), and your schema 
handles it. The other issue that the semantics is trying to tackle is 
whether or not things are in the universe of discourse, and to put 
them there only when they are required to be there by the text, i.e. 
to construct a minimal satisfying interpretation. Your schema does 
not do that part.

However you have convinced me that the folding construction is 
overkill for the basic model theory.  The new/old way of presenting 
this is much simpler.

>BTW, it seems that the need for two equalities still persists.

Yes, it does if you use schemas. The 'two equalities" is not two 
equalities, but two notions of individual, or if you like two 
universes of discourse.

>Let us take a horrocks sentence again.
>
>(forall (x y) (and (P x) (not (Q y)) (= x y)))
>
>We now add "folding axioms" for P and Q:
>
>(forall (x) (iff (holds2 P x) (P x)))
>(forall (x) (iff (holds2 Q x) (Q x)))
>
>and from these two axioms the (conventional FOL) equality
>in the horrocks sentence allows us to derive that
>
>(forall (x) (iff (P x) (Q x)))
>
>thus making the horrocks sentence unsatisfiable.

Right, but the real issue here is not equality, but the fact that the 
schema automatically puts P and Q into the universe of discourse.

>Should we use weak equality instead (axiomatised in
>a way that does not make first arguments of  holdsN
>replacable, even if they are (weakly) equal), then
>the horrocks sentence is satisfiable.

Weak equality is just equality restricted to a subset of the universe 
(the one which corresponds to the original FO universe). But you 
still get problems:

(forall (x y) (and (P x) (not (Q y)) (= x y)))
(exists (u v) (forall (x y) (and (u x) (not (v y)) (= x y))) )

Now, check out the model theory.  The variables u and v have to 
denote something in the universe, and there is only one thing in the 
universe, so this thing that they denote must have a unique 
relational extension, so the formula is unsatisfiable. Using a weak 
equality is just kind of dodging the issue by imposing an incomplete 
logic that can't detect the inconsistency. But its there in the model 
theory. If you give your weak equality a genuine semantics (with a 
completeness theorem) then you will find that there are 'ghost 
individuals' that are in the domain of quantification but 
undetectable by the weak equality, That escapes the Horrocks sentence 
by giving it non-standard models, allowing interpretations with a 
larger universe than the singleton that the sentence seems to impose 
i.e. by denying what it says. And that isn't the kind of solution 
that Ian would find acceptable.

>What this seems to indicate is that we still need the
>"abstract syntax", which is FOL with appN and holdN.
>This allows us to axiomatise the weak equality in an
>understandable way.
>
>Now, if we forget the equality for a moment,
>it still appears that once the two folding axioms
>are present, the "simplified horrocks sentence"
>
>(forall (x y) (and (P x) (not (Q y)))
>
>does NOT have a one-element domain,
>differently from the conventional FOL
>formula, which does.
>
>The folding axioms
>
>(forall (x) (iff (holds2 P x) (P x)))
>(forall (x) (iff (holds2 Q x) (Q x)))
>
>introduce two constants

Yes, quite; which begs the question of their existence, since all 
constant symbols must denote something in FOL. So these axioms do not 
properly capture the folding construction, after all. They express 
half of it accurately, but they beg the central question. Folding 
does not require a relation symbol to denote an individual: it only 
says that IF it also denotes an individual, then that individual's 
relational extension must be the relation. In other words, it is a 
conditional whose conclusion is your schema. Unfortunately, the 
antecedent of that conditional cannot be expressed in a (simple) 
logic, as it requires one to quantify over things that are not in the 
universe.

BTW, this complication is exactly why I introduced the 'header' idea, 
in order to allow 'outer' quantification in the header to range over 
a larger universe than 'inner' quantification in the body of the 
text. Then indeed your schema could be used in the header without 
having these regrettable Horrocks consequences. BTW, strong equality 
is = in the header, weak equality is = in the body; and the 
abstract-syntax SCL-> FOL translation can be viewed as moving 
everything into the header (and into a purely relational FO logic). 
But all that is rather complicated, I concede, and maybe cannot be 
done right now. It is kind of elegant, however.

>, which have to
>be mapped to two different domain
>elements in order to get a model for
>
>(forall (x y) (and (P x) (not (Q y)))
>
>Now, perhaps you want to say that since
>we have not used variables or terms in the
>predicate position, we do not need to
>introduce the folding axioms. But then
>we fall into the traditional trap:
>the moment somebody adds a formula
>(forall (x) x(.....)) we have to introduce
>the folding axioms

Well, yes, but that is exactly why it is best expressed as part of 
the model theory rather than as axioms. The MT applies to ANY SCL 
text, remember, so nothing needs to be added or introduced.

>and the example
>formula suddenly requires a two-element
>domain. I.e., expected meaning of subformulas
>starts to change when new, seemingly
>irrelevant formulas are added.

SCL used to be that way, but I think now that is not true, ie every 
(sub) expression stands on its own without reference to the textual 
context.

>Hence: IMHO we cannot avoid
>adding the folding axioms in the
>examples above.
>
>>>
>>>If it is (maybe?) then the folding stuff is explainable with just
>>>this schema, without changes to underlying semantics, which
>>>would make it eatable for a complex-semantics-hater
>>>like me :)
>>
>>
>>Well, indeed, one can often express a semantic constraint is a 
>>requirement that a schema be true. I tend to think it is easier to 
>>just state the semantic condition directly, but every man to his 
>>taste. I'll think hard about restating the simplified version in 
>>this style.
>
>It would be great if you could do this. It does not mean that you 
>cannot give standalone
>semantics without axioms like the ones above: in principle, one 
>could include both.

Indeed. The FOL embedding needs this done in any case, in effect, 
however one states the MT.

>
>However,  I think that "ordinary people" would feel much
>more comfortable if the semantics is exactly conventional
>FOL semantics, and all the extra stuff is axiomatised on
>top of it.

OK, fair enough. I think the most recent plan (last email) is very 
much closer to this ideal. Really, the complexity of the folding 
construction is only needed to ensure a minimal model, and we don't 
need to do that most of the time.

I'll stop writing emails and get on with writing HTML. I hope to have 
a draft by the end of the week.

>Otherwise you could still claim that your semantics
>is FOL, but anybody who looks at it sees folding maps and
>all kinds of unconventional stuff, which makes people
>suspicious.

Right.

>At least this is what happens to me: just claiming
>that something is FOL does not help much unless I recognise
>that the semantics really is conventional FOL with no
>strange devices built in.
>
>To summarize: this far my impression is that
>
>(a) The folding idea is nice, if it can be presented with
>     axioms.
>
>(b) The semantics of SCL formulas in some concrete syntax
>      is still different from the FOL formulas looking exactly
>      the same (see the examples above).

I really would like to try to make it possible to treat them as being 
the same, or at any rate *effectively* the same.

>
>(c) The abstract syntax with appN/holdsN is still necessary
>      for clear presentation and axiomatisation of various
>      operations (folding axioms and equality).

Its certainly a useful and elegant device.

>
>It is of course possible that I am still misunderstanding
>the folding stuff and the axioms above are not right
>(even though you said they seem to be right).

I suggest ignoring the folding stuff and see the simpler version Im 
writing now, sketched in my last email.

I'm grateful for your feedback, BTW: once one gets inside something 
like the folding semantics its hard to see what it looks like from 
the outside.

Pat


>
>Regards,
>              Tanel


-- 
---------------------------------------------------------------------
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