[SCL] Metalinguistic constructs

[Christopher Menzel]

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.

> Chris Menzel wrote:
>> On Fri, Dec 20, 2002 at 08:29:08PM +0200, Tanel Tammet wrote:
>>> Here is a toy example:
>>>
>>> (formula (name pluscomm)
>>>         (comment "commutativity of plus")
>>>         (content
>>>            (forall (?x ?y)
>>>                (equal (plus ?x ?y) (plus (?y ?x)) )))
>>
>> The form here is really a metalinguistic template for introducing 
>> terms
>> and their axiomatizations into a theory.  It's good to have examples
>> that illustrate the need for a metatheory extension to SCL to motivate
>> its design and definition.
>> It seems to me there are a couple of use/mention issues here as it
>> stands.  If, as it appears, 'formula' is a predicate true of formulas
>> and auxiliary info (maybe 'term' or 'termdef' would be better, if the
>> idea is to have a mechanism for introducing new terms and 
>> corresponding
>> axioms for them), then we need some sort of quotation device that 
>> forms
>> names for formulas out of formulas, or else the result is not
>> well-formed; or at any rate, it won't mean what it is supposed to 
>> mean.
>> Using a single quote as the quoting mechanism then, it seems to me 
>> that
>> the proper would be something like this:
>> (formula '(name 'pluscomm)
>>           (comment "commutativity of plus")
>>           (content
>>             '(forall (?x ?y)
>>                  (equal (plus ?x ?y) (plus (?y ?x)) ))))
>> Thus, "formula", "name", and "comment" all take names of syntactic
>> thingies in the language as their values.
>
> You are of course right in that IF we treat "formula" as a predicate
> in a meta-language, then the content formula could be considered to be 
> in a simpler language, quoted.

That wasn't quite my point.  I was actually talking about an object 
language extension of basic SCL that includes quotation operators that 
forms names for its own sentences, not simply a metalanguage for a 
simpler language.  But, yes, I was talking about treating formula as a 
predicate in such an extension.

> Then you would not need the tags "name", "comment" and "formula" in
> the example above.

That depends on whether or not the predicates "name" etc were useful to 
you.  If you were working in an extension of the sort just noted, it 
could very useful to have them around -- in which case they would be 
functioning as more than mere tags.

> You could write:
>
> (formula pluscomm
>          "commutativity of plus"
>          '(forall (?x ?y)
>               (equal (plus ?x ?y) (plus ?y ?x)) )

Sure thing -- though you'd still need to quote "pluscomm".

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

> Of course we cannot, in practice, give connectives with
>   predefined meanings for all these logics (and more) in SCL standard.

That really depends on how much metalinguistic apparatus we bring into 
play.

>   Hence we should perhaps:
>   - make it possible to use SCL base language for various logics
>   - give at least one standard set of connectives with an exact
>     semantics (ie implement one particular logic, and leave other
>     logics to others). This one preferred logic should probably be
>     FOL, of course.

I don't understand how these two ideas are consistent, unless by a base 
language you mean something very weak, like minimal logic.  Though even 
that wouldn't work as a base for, e.g., default logic.

>   In case we try to treat "formula" as being a predicate in logic,
>   then the TOP LEVEL, the base language of SCL suddenly becomes
>   logic. What logic should that be?

FOL.

> How do we define exact semantics?

As is already given in the CL document, modified long the lines Pat has 
already suggested.

>   These questions are of course extremely hard and we will drown
>   if we try to attack them...
>
>   To summarize, it would be easier to:
>    - not treat SCL base language ("formula", "declaration", "include"
>      kinds of tags) as logic.
>    - give slots in the base language where the logic goes (in the
>      example I had a (formula (content ..)) slot).
>    - give one standard logic (FOL) as one possible filler of the slot,
>      concretely defining SCL representation of FOL.
>    - make it possible for people to use their own exotic
>      logics in the slot as well.

I  think you are envisioning a project rather different than the one 
that gave rise to Common Logic (CL).  CL was intended to be a 
generalization of the version of KIF that was headed for ANSI 
standardization -- a convenient, ASCII- (better, unicode-) based 
language for doing first-order logic (or, with sequence variables, 
something rather stronger), and in particular for writing ontologies.  
CL was borne from the obvious realization that a standard for something 
as ubiquitous as FOL shouldn't force a particular syntax on its users.  
Thus, the syntax of KIF was generalized in CL and expressed in a purely 
abstract, structural fashion, putting no constraints on how that 
syntactic structure should be manifested (though for practical 
purposes, of course, a given syntax must be machine-readable).  That's 
what CL is.  SCL extends it (or its purely first-order component) with 
a theory of lists.  If you want something else, then we should be clear 
about that right up front and just define a brand new project, because 
your aims are not, as far as I can see, the aims of the CL group as 
expressed in the quote from Pat above.  Mind you, I don't mean to be 
passing judgment on the merits of your aims vs CL/SCL.  We just need to 
be clear about what the project is, and should be, about.

Regards,

-chris

-- 

  /\ ASCII ribbon | Chris Menzel -- http://philebus.tamu.edu/~cmenzel
  \/   campaign   | Philosophy Dept, Texas A&M University
  /\   against    | College Station, TX 77843-4237
/  \ HTML email  | voice: 979.845-5660  fax: 979.845.0458