From lusk Wed May 25 00:11:52 1994
Received: from uqcspe.cs.uq.oz.au (uqcspe.cs.uq.oz.au [130.102.192.8]) by antares10.mcs.anl.gov (8.6.4/8.6.4) with SMTP id AAA05948 for ; Wed, 25 May 1994 00:08:48 -0500
Received: from everest.cs.uq.oz.au by uqcspe.cs.uq.oz.au
id ; Wed, 25 May 94 15:08:05 +1000
Received: by everest (5.0/SMI-SVR4)
id AA01086; Wed, 25 May 1994 15:08:01 --1000
Date: Wed, 25 May 1994 15:08:01 +1000 (EST)
From: John Staples
Subject: spelling out the Manifesto
To: qed@mcs.anl.gov
Cc: staples@cs.uq.oz.au
Message-Id:
Mime-Version: 1.0
Content-Type: TEXT/PLAIN; charset=US-ASCII
Content-Length: 5586
This is a comment on Mike B's `spelling out the Manifesto'.
It is not an author response since I was not one of the
authors.
In particular I want to comment on Mike's notion of
reification, which interprets various logics (or, their
theories) as theories based on classical first order logic.
So far, so good, but note that Mike's introduction of reification
in 2. does not discuss translation of inference rules. Perhaps for this
reason, I was uneasy to read `This can be done for EVERY logic'.
However, provided the other logic has a model theory comprehensible in
classical logic, I don't have a solid objection.
At Mike's point 4 I start to have real concerns.
The claim is that each proof of a result A in a logic L can be converted
into a proof of the reification of A in classical first order logic.
Without knowing how inference is converted, I can't confirm that.
Mike then introduces the name Meta for the (prospective)
QED metatheory, but he does not make explicit the relationship
between Meta and the first order classical theories that are
the targets of reification. I believe that both the logic L and the
classical logic in which it is reified are object languages relative to
the metatheory. The metatheory is for example a language
in which reifications may be described.
But my biggest problem is that I find footnote 9 seriously confusing:
It talks of translating `into Meta' - a translation which hasn't been
discussed previously unless Meta is supposed to be the classical first
order logic which is the target of reification. It also says we don't
need to mention, as part of reification, any axioms (of the theory
L to be reified, I presume) that are in Meta. This appears to mean that
Meta axioms are necessarily true of the reification of L.
That seems to imply a restriction on the generality of reification.
For example, what if some theory of L has an axiom whose reification
contradicts some axiom of Meta?
There are two issues here: what Mike intended (which I hope he'll indicate)
and what I would suggest. I now outline the latter.
1. QED needs a simple, precise, trustworthy, adequately expressive
framework in which eg. languages, logics and translations such as
reification can be discussed. That is the metatheory.
2. Techniques such as reification are relationships between object logics.
3. Being a metatheory is a relationship that one theory has to others.
When that relationship is ignored, a metatheory is an
ordinary theory, and this ordinary theory should be one of the
object theories which is within the scope of the metatheory.
This doesn't mean the metatheory necessarily has a reflection principle.
It does mean that there can be QED support for the metatheory.
4. At the workshop I felt there was some concern that a metatheory
might cause complications. To me, the opposite is true.
A metatheory is the only way I know to think coherently about the
relationships between different formalisms. If we don't have an
explicit metatheory, these relationships will exist only as
implementations of translation algorithms. Then, complications and
incoherence will be a continual threat (read `reality'!).
There'll be no basis for discussion of correctness of such algorithms.
5. Here's an example of just how simple a metatheory can be.
Consider pure Prolog, limited to primitive recursive predicate definitions,
if you will. (No, this is not a plug for Prolog programming!)
Pure Prolog is quantifier-free, first order, unsorted, and lacks negation.
In the usual semantics, each pure Prolog program is a metatheory
of a simple object language, whose terms are usually called
`Herbrand objects'. These objects are sometimes described as
`ground terms of Prolog', and indeed there is an 1-1 correspondence with
Prolog round terms, but there also is a difference:
the object terms are at the object level and Prolog terms are at the
meta level. The meta level is more obviously represented by:
* the relation (or `predicate', `procedure') symbols of Prolog,
which in general are meta-level relation symbols, though some
are employed to describe object-level relations;
* Prolog variables, which are meta-level variables and so allow
schemes of object-level expressions to be described;
* the symbols `:-' and `,' which are respectively
meta-level implication and meta-level conjunction.
Since Herbrand objects can represent arbitrary ordered, labelled trees,
they can be used to represent the syntax of EVERY (sorry Mike) logic
and theory. Well, maybe enough to satisfy QED, anyway.
My point is not to advocate this approach, even though here in Oz
we are getting satisfaction from a development of this basic idea.
Rather I want to emphasise two points, which I think this example
demonstrates:
* there doesn't need to be anything complicated about a metatheory
* there's really no need to worry about conceptual difficulties
being caused by jumping back and forth between objects and meta levels.
There's no jumping. Conceptually, AS IN EVERY FORMAL LOGIC TEXT,
the whole discussion is at the meta level, with metalevel vocabulary
sometimes being used to describe the object level. All the formal
things you know and love doing at the object level are there
(word for word if adequate concrete syntax is available) as part
of the meta-level description of the object level. You've lost nothing
and gained an ability to formally describe eg. axiom schemes,
inference rules, side conditions and relationships between
logics and theories.
John Staples