[SCL] Metalinguistic constructs

[Tanel Tammet]

Hi,

Christopher Menzel wrote:
> On Saturday, December 21, 2002, at 04:31 AM, Tanel Tammet wrote:
> 
> Hello Tanel.  Thank you for your interesting and detailed comments.  I 
> think they raise some very important issues.
...
>> However, I have several doubts about this way to express information
>> in SCL. I still think a tagged and unquoted (in some sense, but read
>> on) expression is better. There are two separate reasons:
>>
>> - Trying to use "real" metalogic here may lead us to serious
>>   complexities.
> 
> 
> Depending on the use to which you want to put it -- on which, see below.
> 
>>  IMHO the scl focus is on practical possibilities
>>   to present, extend, modify, annotate and connect formula-representing
>>   data.
>>
>>   I'd prefer viewing SCL as a vehicle where we can convey data in
>>   various logical languages: FOL, intuitionistic logic, TR, default
>>   logic, etc.
> 
> 
> Well, then we might have a disagreement over what SCL is about.  My 
> understanding, in Pat's words, is that its purpose is to be "a good 
> logic standard."  More specifically, he wrote:
> 
>   I propose to form an ad-hoc working group whose aim will be to produce 
> a firm,
>   detailed CL-style standard suitable for immediate application, with 
> similar aims
>   to the declared CL project, ie a general-purpose first-order logic 
> language, with
>   a clear semantic theory and a machine-oriented syntax...
> 
> By contrast, I'm not exactly sure what a vehicle for conveying data data 
> in various logical languages is supposed to be, but it doesn't sound 
> like something that is *itself* a logic.  But if we *are* working on 
> something that is itself a logic, then if we want it *also* to be able 
> to convey data in various other logics (and it isn't obvious to me that 
> that is what we want -- though it isn't obvious to me that it isn't 
> either), then what we need is a logical *theory* of those other 
> frameworks and how data in them is conveyed.  That will, of course, 
> involve the sort of extension indicated above.  Note this is not simply 
> my idea; it has been a part of the KIF/CL group for quite some time -- 
> though not with quite the scope you seem to have in mind.  Now maybe it 
> wasn't good idea for some reason we might convince ourselves of, but I 
> think we should be careful about a sudden change of direction.

I agree that our group should not wander into uncharted territories
we did not plan to visit.

Since my only knowledge of the CL project comes from reading
the drafts, minutes (and the earlier KIF stuff) I may well
have had ignored some agreements of the CL project.

Pointing this out is a right thing to do, thanks!

Despite of this, I still think that it would be very
useful if we could achieve some of the goals I put
into the mini-agenda before. It would very good if
we could stick to the CL goals, yet achieve something
additional on a way.

I really think that SIMPLY agreeing on a common
syntax of FOL does not bring many benefits and is
not necessarily an important goal in itself
We already have a number of FOL syntaxes. If we simply
wanted a nice FOL syntax, then why not take some
classical syntax directly from the classical books :-)

Exchanging pure FOL formulas between the systems without
any agreed-upon possibility to give metainformation
is not of much use. Metainformation, as the examples pointed
out, is really crucial in practice. If we cannot convey
it, then obviously system implementors need to design
their own languages for that. During this, the considerations
stemming from the need to exchange metainformation might
well make them to decide to drop the pure FOL standard
we or CL had created.

Similar considerations apply to conveying information
in other logics. People have a very strong tendency
to use exotic logics here and there. Very often
these logics are extensions or special forms of FOL,
or share large parts with FOL. If we make it possible
for them to use our syntax, they will not have to devise
completely different syntaxes and the common FOL
part in their formulas would be understandable to
"ordinary" systems as well. FOL would be a distinguished
common denominator, so to say, not a "not-invented-here"
system to be avoided.

To summarize what I learned from your message:
it is highly desirable to view the metainformation
constructions as FOL formulas.

Although I think this will not be easy, we may try.

Regards,
        Tanel Tammet