[SCL] Re: Folding unnecessary [was: Re: Update to SCL-related work]
Pat Hayes
phayes at ihmc.us
Mon May 24 09:32:24 CDT 2004
>Hi,
>
>Pat Hayes wrote:
>
>>Tanel, a quick amplification of a point in the last email:
>>
>>>It runs deeper than this. Its a problem with
>>>the size of the universe. Its true that
>>>without equality there is no way to
>>>axiomatically enforce a finite universe, so
>>>the examples all use equality, but the
>>>meta-theoretic point they illustrate holds
>>>true even for the logic without equality. What
>>>we want is that if some SCL text is GOFOL,
>>>then its FO models are among its SCL models.
>>>The Horrocks sentences illustrate the
>>>objection that with the former SCL semantics,
>>>this is not the case (because the relations
>>>had to be in the universe). It would still be
>>>a valid objection in the logic without
>>>equality. That is what was unacceptable (and
>>>is now fixed), not a specific equality issue.
>>
>>
>>To illustrate, consider the single FO sentence in SCL notation
>>
>>(P a)
>>
>>and its embedding into FOL using the ECL format:
>>
>>Atom_2(P, a)
>>
>>and consider the FO-valid inference rule of
>>existential generalization (in an ND system),
>>which applies to the latter to produce the
>>valid FO consequence
>>
>>(exists (x) Atom_2(x, a) )
>>
>>which is NOT a correct translation of any FO
>>consequence of the original sentence. So the
>>translation fails to accurately capture FO
>>logic.
>>
>>This exhibits the issue without using equality,
>>and illustrates why it is essentially a matter
>>of what is in the universe. By using the
>>relation names as true FO names in a classical
>>FO framework, we have required them to denote
>>something in the universe of quantification.
>>
>Well, you are certainly right. But I doubt that
>the folding semantics - at least in
>the way it is currently presented in the SCL draft - is the solution.
Can you say why you think this? Although it may
not be as well expressed as it could be, it seems
to me that it handles the matter reasonably well.
It allows 'standard' FO models for text which is
indeed classical FO, but also allows models for
the most liberal SCL syntax, all in a single
uniform language which does not require users to
do any 'declaring' or use any variant syntax. It
supports exactly all patterns of conventional
valid FO reasoning on any SCL expression (eg, one
can apply ND quantifier rules to any term in any
argument position, and equality substitution
anywhere) and it allows users who wish to
restrict their universes to keep their universes
restricted. (I agree with you that this last
point seems kind of silly in a Web context, but
it doesnt seem silly to a vocal group of folk
within the Sem Web community, and I want to give
them some breathing space. In any case, many
recent decideability results depend on subtle
model-theoretic properties such as the finite-
and tree-model properties, so the more we can
allow people to preserve their FO universes, the
better. Folding does not increase the size of the
universe, it only adds extension mappings.)
The other point about this MT (whatever we call
it) is that although the semantics is more
complicated, the actual language is simplified.
So from the 'users' point of view, things are
simpler with the folding semantics, and can be
summarized very succinctly: you can write any
expressions you want in any position, and you can
use any valid FO= valid reasoning pattern. What
could be simpler? Most users aren't interested in
MTheory details in any case. All the other
options require some kind of special care or
cognitive burden from users (don't violate the
signature, don't confuse two kinds of
application, distinguish this kind of equality
from that kind...)
>I have some notes and a longish (yet trivial) suggestion on the issue.
>
>1) Probably the size of the domain of formulas does not really matter,
> as long as the satisfiability property is exactly the same.
I tend to agree, but there are many who sharply
disagree, and are highly sensitive to this issue.
We need to give the world a standard that will
not be immediately attacked by half the
authorities as unusable.
> In particular, the very moment you introduce integers or strings
> or lists, the domain becomes infinite, and never returns to finite
> spheres. Horrocks sentences fail immediately, also for GOFOL,
> etc.
>
> Now, do we really expect to use SCL much in the contexts where
> no integers, strings or lists are defined?
Maybe not, but some will respond that these
things are in other domains (datatype domains,
not the universe of individuals) Im not saying I
agree with this philosophy, but we need to allow
people who feel strongly about this to work
within the SCL framework.
>2) We deviate from traditional FOL the very moment we declare that
> you are allowed to quantify over predicates and function symbols.
We deviate from traditional FO *syntax*, yes, of
course. Part of the point of the folding idea is
to suggest that this is not, in fact, necessarily
a deviation from the traditional FO semantics: it
can be viewed as what happens when you preserve
the FO semantics but allow divergences of opinion
about signatures. The preservation is clearly
illustrated by the fact that the FO inference
patterns are preserved exactly in the resulting
logic (though they can interact in new ways
because of the lack of signatures, eg one can do
this:
(forall (x) (= x x)) axiom 1
(= P P) UInstance 2
(P a b) Assumption 3
(and (P a b)(= P P)) & intro 4
(exist (x) ( and (x a b) (= x P)) EGeneralization 5
(implies (P a b) (exist (x) ( and (x a b) (= x P)) ) Imp Introduction [3]
Every step here is pure FO reasoning. The result
is 'peculiar' only because the derivation does
not conform to the usual syntactic restrictions
on signature roles for the symbol 'P": it is used
first as an individual name and later as a
relation. But that is a different issue from the
question of whether or not this is FO reasoning.
Every step in this proof is *exactly* FO valid.
> There is no escaping that. Differences in semantics have to be
> there,
True, but they can be kept to a minimum. All we
have to do is to allow a kind of punning between
individuals and relations, by allowing an
individual to have an associated relational
extension which is its meaning *as a relation*,
or if you like the meaning it has when it occurs
in a 'relational role' in the syntax. In
particular, they do not require that the universe
be enlarged, if the text does not itself
explicitly require this (eg by its use of complex
terms in relation position.) The basic point is
that if you have a satisfiable SCL text T and a
subtext T' which is pure GOFOL, and I is a folded
interpretation of T, then there is a
subinterpretation of I which satisfies T' and is
*exactly* a classical FO interpretation of T'.
The folds are only there to keep the various
'alternative' FO structures aligned with each
other: they don't affect any of the truth-values
of any expressions.
>it is completely hopeless to hide the differences by complex
> semantical schemas: this way we simply hide the semantics from
> the eyes of the reader, but we cannot change the basic fact that
> there are some differences.
>
>3) Let us suppose that we want pure, unchanged, traditional FOL
> back into SCL, with exactly the same semantics and everything.
>
> Fortunately, we know that it is already there. The "abstract syntax"
> of ECL, presenting traditional KIF syntax (and (P x) (Q (f x))) as
> Formula_3(and, Atom_2(P,x), Atom_2(Q, Term_2(f,x)))
> is traditional FOL itself.
Well, yes, sure. But its not the *same* FOL as
the original, which is the point.
> SCL really amounts to a terminological suggestion: the suggestion
> to call the first arguments of traditional FOL atoms and terms
> as "predicate symbols" and "function symbols". We have done
> nothing more than introduced slightly nontraditional terminology.
That was the CL idea, indeed. I think we have got
something slightly better than that now. Or
perhaps just a slightly better way to state the
idea, one that roots it in a 'net-centric'
motivation.
>
> What then prohibits us to use the traditional FOL, when the SCL
> abstract syntax already IS traditional FOL? Just the conventions
> of the concrete syntaxes: in abstract syntax I could write
> Formula_3(and, P(x), Atom_2(Q, Term_2(f,x)))
> instead of
> Formula_3(and, Atom_2(P,x), Atom_2(Q, Term_2(f,x)))
> but the KIF concrete syntax does not allow this: it forces me
> to write
> (and (P x) (Q (f x)))
> which is always translated to
> Formula_3(and, Atom_2(P,x), Atom_2(Q, Term_2(f,x))).
But why must it be so always translated? There is
nothing in either the abstract syntax or the
semantics which REQUIRES this translation to be
done. The only reason for requiring a uniform
translation is to provide a uniform way to
process SCL inside FOL, so as to be able to apply
traditional FO engines to (all of) SCL. I do not
mean to say that this is not a good reason, but
it is motivated by operational pragmatics rather
than syntactic or semantic necessity. We can say
this, and endorse it for this (excellent)
pragmatic reason: but we can also point out that
any SCL tool can be used to transmit, parse and
process traditional FOL as a subset of SCL
without doing any translation at all; and that
when so used, the SCL semantics is identical to
the classical semantics.
> It seems that if we want to allow traditional FOL to be used
> in SCL (with exactly traditional semantics), then we ONLY
> need to allow this in concrete syntaxes.
>
> We already can write
> traditional FOL in the abstract syntax (provided we just drop
> the explicit requirement that the only term/atom constructors
> are called "Term_1, Atom_1, Term_2, Atom_2, ..." which
> is very easy to drop (only the equality axiomatisation needs
> a slight modification)). It has traditional FOL semantics,
> with no changes whatsoever.
Right, but now we have to distinguish the
meanings of a name used as a constant and the
same name used as a relation. Now, take this
idea, and just impose an extra condition on the
semantics, that these two meanings of the same
symbol are required to be the same, in the sense
that the relational extension associated with the
thing denoted by the name used as an individual
must be exactly the relation denoted by that name
used as a relation. That's exactly the folded
semantics. The fold maps are just enough to make
sure that you can use a name anywhere and it
always 'means' the same thing: they keep the
entity/relation punning internally coherent, even
in cases such as
(((f a) b ) c)
where there is no other name than the functional term to denote the relation.
> How to allow traditional FOL in concrete syntaxes, then,
> without making the SCL-style function/predicates inconvenient
> to write by forcing abstract syntax Term_N and Atom_N
> to be used?
>
> Clearly, this is a SYNTACTICAL, not semantical issue.
But it has semantic consequences when you take
quantifier rules into account, and when you need
to be able to handle pieces of syntax with
'implicit' existential commitments arising from
assumptions that all functions are total. (All
this would be a lot easier if we had no function
symbols in the language, by the way.)
> We should allow two kinds of terms/atoms: those translated
> into Atom_2(P,x) and those translated into P(x).
Yuck. Two different syntactic forms in order to
specify different translations? That hardly seems
like an adequate reason for introducing a new
syntactic category into the language.
>
> There seem to be several options:
>
> a) Declare that P in the function/predicate position should be
> always translated in the P(x) way, not Atom_2(P,x) way.
> This is possible, but works very badly when SCL text from
> different sources is integrated. Essentially, it would be
> a declaration for the parser, and does not have anything
> to do with semantics.
Right. If we impose a need to declare syntax, we might as well just use GOFOL.
> b) Use two different application syntaxes. We could suggest
> people to use P(x) or (P x), translated to Atom_2(P,x) in
> abstract syntax,
> and to use P[x] or [P x], translated to P(x) in abstract
> syntax.
>
> Only power users would use the P[x] syntax, and they
> would not mind. Most people would never understand
> or use the P[x] construction.
>
> We could even have a special "power user" concrete syntax,
> with the () and [] roles switched, where P(x) or (P x) is
> translated to P(x) in abstract syntax,
> while P[x] or [P x] is translated to Atom_2(P,x).
>
> Regardless of which option we use, questions will be rised
> about relations between P(x) and P[x], translated to
> Atom_2(P,x) and P(x) in abstract syntax, There are several
> options to choose from:
>
> a) Saying that there are no relations whatsoever. P stands for
> completely different things in P(x) and P[x]. I would really
> prefer that option, since anybody sophisticated enough to
> use BOTH P(x) and P[x] would understand the differences
> perfectly and would have a good reason to have two different
> results.
I really don't like this option. Why use the same
name if the two are unrelated? In any case, the
whole point of allowing relations to be objects
is so that one can treat them as objects in the
logic: quantify over them, use equality reasoning
on them, etc.. All that is lost if the relations
and relation individuals are kept dissociated
into separate syntactic categories.
> 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.)
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? 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.
>which simply
>begs to be used and even offers several
>options to choose from.
>
>The only "problem" with this answer is that it is
>embarrassingly trivial and states very clearly that
>SCL is nothing clever and not a single new
>logical idea has been introduced.
>
>I really think that this is what horrified both
>you and Chris. You should not be horrified,
>it is a virtue to avoid new logical ideas in
>SCL, not a sin.
>
>SCL is not a project to invent a new logic
>(join type theorists, linear logicists or even
>DL people for that!), but to use good old
>stuff for new purposes.
>
>Whenever we have a perfect, trivial answer to
>a question, it is a sin to forget it and
>invent your own complex answer instead :)
Well, I tend to agree, but I don't think that
your approach does provide an answer, at least to
my questions.
But you have goaded me into thinking about how to
present these ideas with less fuss and more
simply, and I think I can see how to do it
(without mentioning 'folding maps' as such) . I
will sketch this in a later email soon.
Pat
--
---------------------------------------------------------------------
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
More information about the SCL
mailing list