[SCL] Re: scl:comment [was: Re: SCL spec question]

[Bill Andersen]

> Well,  the commenting syntax is designed recursively to allow 
> 'nesting' of comments. Thus on three successive days the axiom might 
> look successively like:
>
> (forall (?x) (p ?x))
> (scl:comment "bill likes this" (forall (?x) (p ?x)))
> (scl:comment "pat thinks bill is crazy" (scl:comment "bill likes this" 
> (forall (?x) (p ?x))))

Right.  Does this mean that the second comment is about the sentence

	(scl:comment "bill likes this" (forall (?x) (p ?x)))

??

>> Another (I think reasonable) compromise, would be to introduce 
>> non-denoting constants to name axioms.
>
> Well, wait a minute. If they name axioms don't they denote them?
>
>>  I say non-denoting because I'm trying to avoid quantification over 
>> formulas.
>
> Hmm. I see why you want to avoid it, but these 'names' would have to 
> be distinguishable from names that really do denote, right? How?

That was kindof my question.  I figured since we opened the door to 
non-denoting predicates and function symbols, we could make another 
exception.  I was trying to avoid the situation where

	(scl:formulaID a1 (forall (?x) (p ?x))) =_df (= a1 (forall (?x) (p 
?x)))

Secondly, my goal was to provide a mechanism for multiple comments to 
be made on the same axiom -- "same" being the sticky notion that we're 
trying to avoid dealing with.

>> This is, in general, a useful mechanism for commenting on any 
>> constant introduced.  I don't think it's a good idea to embed this in 
>> the term syntax, since there seems to be no principled place to put 
>> the comment.
>
> ? Seems to me that one can put a comment anywhere.

Right.  Probably need both mechanisms.  There will need to be 
documentation for constants introduced in documents as well as 
(perhaps) documentation on the use of those constants in particular 
axioms.  For example:

(scl:comment "basic part relation of mereology" mereo:part)
(scl:comment "basic proper part relation of mereology" mereo:pPart)

(forall (?x ?y ?z)
    (=> (and (locatedIn ?x ?y)
                    ((scl:comment "use pPart because case ?y=?z is 
uninteresting" pPart) ?y ?z))
           (locatedIn ?x ?z)))

Seems like you need both kinds of scope for comments.

>>  What are the ramifications of doing it this way instead:
>>
>> (scl:comment "biological fatherhood relation" bill:fatherOf)
>>
>> One big difference could be that bill:fatherOf denotes, but for 
>> something as mundane and useful as making comments I think there's 
>> good cause to special case the function of scl:comment
>
> Hmm, maybe. I basically wanted to allow comments (annotations more 
> generally) but make them logically transparent/invisible. You are 
> suggesting a convention which treats them in a particular way. Since 
> they don't denote, the role of axiom labels seems to be orthogonal to 
> any logical role they might have. So this is a convention that could 
> be added transparently to SCL without modifying it, I think.
>
> One issue is that if comments are transparent then your example
>
> (scl:comment "biological fatherhood relation" bill:fatherOf)
>
> is logically just a bare constant name, which currently isn't a legal 
> phrase.
>
> Need to think about this some more. Would you say that this example 
> should be treated like an atomic sentence?

I would, except now we're creeping into ontology a bit.  Question is 
are we making comments about the syntactic pieces (terms, formulas, 
sentences) or the referents of those pieces?  The former removes 
worries about what, e.g., scl:formulaID would mean -- it could just 
denote the piece of text for a term or formula, which is fine, but 
might then involve the whole meta-SCL issue.  Of course this would 
provide some machinery to talk about formula identity.  I think the 
issue of whether to treat comments as atomic formulae or not is a wash 
-- if one wants to be a comment-semantics-nazi, one could use some kind 
of meta-SCL and write a theory of comments, introducing a new 
comment-denoting relation to do that work; on the other hand, I think 
there's a pragmatic solution that would do most of the same work 
without invoking all kinds of machinery..

The major problem I see with my first suggestion is that it wants 
special treatment for formula IDs, and as you pointed out, there is the 
issue of whether scl:comment statements are taken as SCL atomic 
formulae or are taken as transparent.