[SCL] Syntax epiphany (was: Re: Folding unnecessary [was: Re: Update to SCL-related work])

[Pat Hayes]

>Pat Hayes wrote:
>
>>>3) Keeping the SCL concrete syntaxes simple
>>>     and traditional, with no weird/complex
>>>     constructions.
>>
>>
>>Agreed, but we might have different views on what counts as more 
>>weird and complex. I find lexical conventions awkward and we have 
>>tried to eliminate them as far as possible.
>>
>Right, it makes sense as well.
>
>However, we need some convention to distinguish between two different kinds
>of predicate/function application. The question remaining is which convention
>is nicer. We cannot avoid using some kind of a convention.


OK, how about this? Follow your idea, but rather than make it a 
lexical distinction (which I am averse to for reasons based on Web 
architecture) , use the syntax.  This idea is so simple its almost 
beautiful: combine the P(x) and (P x) conventions. They both mean 
apply P to x, but the first one requires that P is not in the 
universe of discourse, the second requires that it is.  Then SCL 
using the KIF convention is unchanged, and FOL using the prefix 
convention is unchanged: and (P x) in SCL maps *exactly* to Apply-1(P 
x). SCL then really, *really* is FOL with the holds/app convention 
'built in'. You can get SCL from FOL just by using an eraser. In both 
languages, names and terms in 'inner' positions denote things in the 
universe, and names in a prefix position denote things not in the 
universe: but in pure KIF syntax, there aren't any such names.

We can tell people that if they want to maximize interoperability and 
syntactic freedom, use the KIF style. If they want to be all up-tight 
about keeping relations out of their universes, use the FO style 
syntax.  Or mix and match.  The basic meaning is the same.

The syntactic convention in the core syntax will be that a name 
followed by an open parenthesis without an intervening  space always 
indicates a FOL application (function or atom). I'll need to re-write 
the EBNF yet again, but that's life.

This allows two ontologies to use P differently, and we have to 
decide what to do when such texts are combined. IMO they ought to be 
inconsistent, ie their conjunction is a contradiction, since P(a) & 
(P a) requires that P to be both in and not in the universe of 
discourse; but I can't see any simple way to make such a 
contradiction apparent in a proof derivation...ah, wait, yes I do: 
there is an axiom (tautology) scheme:

(forall (x)  (not x(...) ))

which now gets us an explicit contradiction:

(and P(a) (P a))
(exists (x) (and x(a) (x a)))     EGeneralization applied to the name 
P (kosher because P is used as a name in the expression)
(exists (x) x(a) )      &elim applied inside the existential (ahem. 
Please don't look behind the curtain....)
(not (exists (x) x(a) )     transformation of instance of the axiom

So the EG rule is, that one can existentially generalize on any name 
in any argument position (just as in FOL) ; but if that name occurs 
also in a relation position, then it can be 'captured' by the 
generalization. This makes sense, since the name should always have 
the same meaning wherever it occurs. Note that this is NOT a valid 
application of the rule:

P(a)
?? therefore??
(exists (x) x(a) )

since P is not a name in that text: it only produces this aberration 
when applied to 'mixed' text which is already internally 
contradictory.

>
>>>
>>>In any concrete SCL syntax we split the names,
>>>i.e lexical items for constants/predicates/functions
>>>into several sets:
>>>
>>>- ordinary constants (like a, c1, bbx)
>>>- numeric constants (like 0, -2, 10)
>>>- string constants (like "aab", "1")
>>>- possibly date and time constants (like 01.02.2004)
>>>- special function and predicate names: any name
>>>  prefixed by ! is a special name (like !f, !P)
>>
>>
>>But now this requires a global naming convention to be agreed on. I 
>>don't think this is acceptable for a logic to be used on the Web.
>>
>>Tell you what:I'll see how simple I can make the 'headers' idea 
>>come out to be, and then we compare notes. I agree we need to have 
>>some simple straightforward way to determine when to translate (P 
>>x) correctly as holds_2(P x) and when as itself. I think this is 
>>best determined by what is said ABOUT the text rather than in the 
>>text itself, however.
>>
>OK. I'll upgrade the ECL draft later today, following the notes in 
>my last email.
>Will send mail when it is ready.
>
>Perhaps the lexical and header approach can be combined.

Yes. There are other advantages to headers. Using the above scheme, 
the P(...) syntax should be forbidden in a header since header 
sentences are supposed to be interpreted in the 'global universe' 
where everything that can possibly exist, exists. So in the header, 
you can refer to the ontology's universe of discourse explicitly by 
using the ontology name. So the header version of P(a) in an ontology 
named ex:fred would be (and (P a) (not (ex:fred P))), ie P is true of 
a but P is not in the local universe.


MOre later (on datatyping) : I have to run now.

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