[SCL] Metalinguistic constructs

[Chris Menzel]

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.

-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