[X-logic-strategy] XML foundation vocabularies (was strategy update note)

[Roger B. J. <rb...@rb...>]

Neil observed (inter alia):

> The idea that meaning of an expression could be defined as
> the expression consequences of the initial expression is an
> idea by one of the philosophers of language (whom, I do not
> remember).

What will do for a philosopher of language may fall short
of an adequate position for a software engineer!

> The idea is simply that we may ask someone what
> they mean by an expression and their expression response
> would be the meaning of the initial expression.

(which is a bit stronger than talking about consequences)
To give an expression when defining or explaining the meaning of
some other expression does not mean that the meaning
_is_ an expression.
It usually means that the meaning of the defined expression is
the same as that of the defined or explained expression.
...
> We might think of this as _formalist_
> meaning. Meaning as the relations strings (expressions) have
> in a particular generating/computable sequence.

> Logic for, say, _formalist_ meaning would be similar to the
> Intuitionist's logic for Constructive mathematics.  An implication
> is a construction/computation and arguments of implication
> states or arguments of the computable function.  There is a
> sense in which the Intuitionist's formalism is an abstraction of
> arbitrary computation.

I associate a formalist conception of meaning with a context
in which the logic is established first and plays a role in axiomatic
definition of the meaning of concepts.

i.e. I associate it with Hilbert's idea that mathematical concepts
should be defined by axiomatisation, which these days one thinks
of usually in the context of first order logic (in which case, however
we know that the meaning of many concepts cannot be completely
caputured by recursive axiom systems).

In my conception of semantics in X-Logic, the semantics of some
XML vocabulary is defined using some other XML vocabulary.
Ultimately this must come to an end!
Let us call an XML vocabulary which is suitable for defining the
semantics of other XML vocabularies but is not itself so defined
(except maybe in terms of itself) a XML foundation vocabulary.

I advocate that an XML foundation vocabulary be defined in
several ways.
(1) in terms of itself
(2) formally (but incompletely)
(3) informally (perhaps by describing how
the formal account is incomplete)

As far as (3) goes this comes down to something quite simple.
e.g. referring to "standard models" of HOL.
(some people will never understand this... you have to accept that
I think)

More specifically I advocate (and may eventually get round to)
obtaining an XML foundation vocabulary by the following means:
(1) define (as above) a simple vocabulary corresponding to HOL
      (polymorphic version of Church's STT)
(2) implement a feature in a HOL proof tool which will export
     theories as definitions of XML vocabularies in terms of the
     vocabulary in context.
(3) apply this to the Galactic Set Theory developed on the X-Logic
     site to export an XML vocabulary for a rich polymorphic higher
     order set theory.

Does any of that make any sense?

Roger
RB...@RB...