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

[Pat Hayes]

>Pat Hayes wrote:
>
>>>        b) We could axiomatise that Atom_2(P,x) is always
>>>             equivalent to P(x). This is, of course, perfectly possible:
>>>            it would be an axiom schema similar to what we have to
>>>           use to define equality.
>>>
>>>           I suspect that this would be similar to the folding
>>>           semantics (is it?) but would have an important advantage
>>>           of - by virtue of being axiomatised - not changing the
>>>           underlying semantics a bit.
>>>
>>>            I do not think that it makes sense to axiomatise this,
>>>            but, well, we could do it if we really wanted to.
>>>        
>>>To summarise: I think you have made a good point,
>>>but the folding semantics is not an answer.
>>>
>>>Instead, there is a trivial, correct answer
>>
>>
>>I don't think that it is correct, is the point. 
>>None of your options above seem acceptable, and 
>>all are more complex for a user than the SCL 
>>logic we already have (which, as you say, is 
>>almost embarrassingly simple, both in its 
>>syntax and its proof theory.)
>>
>Well, the trivial answer definitely is correct, 
>but I agree that it has unpleasant side effects
>in terms of syntax.
>
>>Here's my current 'acid test'. If two people 
>>both want to use a symbol P, but one wants to 
>>use it as an individual name and the other 
>>wants to use it as a relation name, can they 
>>use the language to communicate with one 
>>another? That is, can each of them use the 
>>symbol in their way to draw arbitrary 
>>first-order inferences from information send to 
>>them by the other, so that they can agree on 
>>the conclusions?
>
>This is certainly crucial, I agree.
>
>>And can they do this without having to 
>>negotiate, use syntax declarations, or 
>>translate from one syntax into another? Right 
>>now, SCL allows all of this. I don't think ECL 
>>does.
>>
>ECL does this, of course, but it does not allow to write conventional FOL.
>It simply forces the Atom_N etc wrappers into the FOL translation.
>
>Should we allow ECL to be used in the conventional FOL way,
>without this App/Holds wrapping, then either the acid test fails or
>we have to introduce extra syntax: both are bad. That is the reason
>I did not allow the conventional FOL way, of course.
>
>>Well, I tend to agree, but I don't think that 
>>your approach does provide an answer, at least 
>>to my questions.
>>
>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. If one deskolemizes 
this by replacing (= (x y) z) with (x y z), the 
complications are revealed by the intertangled 
quantifiers expressing the functionality of the 
relations. Notice that y here, corresponding to 
the term (f a) which denotes a function and is 
also the value of a function, is bound by the 
outer existential and also plays a central role 
in an embedded universal:

(exists (x y z)(and (x c) (y b x) (f a y)
(forall (u v w)(implies (and (= u v)(f u w))(f v w)))
(forall (u v w)(implies (and (= u v)(y u w))(y v w)))
))

But I think your email crossed mine which 
outlined a new way to present the MT which avoids 
almost all this complication in the main 
exposition and reduces it to an appendix (which 
can be ignored if all one is interested in is 
satisfiability.)

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

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