Delivery-Date: 
Date: Thu, 27 Apr 1995 07:06:16 GMT
From: Roger Bishop Jones <rbj@campion.demon.co.uk>
Message-Id: <3802@campion.demon.co.uk>
To: John.Harrison@cl.cam.ac.uk
Cc: qed@mcs.anl.gov
Subject: Re: Paper on reflection
Lines: 36
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

In message <"swan.cl.cam.:139810:950425191403"@cl.cam.ac.uk> John Harrison writes:
> 
> Roger Jones writes:
> 
> | I don't see why a reflection principle should be regarded as "in opposition"
> | to the LCF paradigm.  The LCF paradigm can be applied to any logic however
> | complex its rules.  A reflection principle can be put into a logic and
> | implemented as a rule, using the LCF paradigm, in complete consistency with
> | anything that I would regard as essential to that paradigm.
> 
> Yes, it would have been more precise to say that the following *ideas* are
> naturally placed in opposition: "pure LCF is good enough" and "reflection
> principles are a practical necessity".
> 
> But, if one regards as part of the LCF paradigm a secure metalanguage encoding
> theorems as an abstract type, the addition of a reflection principle *may*
> present a few tricky technical problems. Konrad Slind has thought about the
> practicalities of this more than I have, though my paper contains a few offhand
> remarks. (End of section 6.)

HOL is sufficient to act as its own metalanguage for this kind of purpose,
so I would say that the amount of adaptation to the LCF paradigm strictly
necessary to install a reflection principle is less than you seem to be
suggesting.  (in fact, I would say no changes to the paradigm are necessary,
a reflection principle is no less "pure" than the derived rules which use
mk_thm, but that depends on what mean by "pure LCF" and ditto for "reflection")

If I won the national lottery, my next proof tool would have a reflection
principle, but if it had to be implemented out of revenue from ProofPower
it would take a very long time to come to the top of the priority list!
(actually, I wrote a paper in 1986 advocating a logic with a reflection
principle for use in program verification, but when it came to doing ProofPower
in 1990 we were much more conservative)
 
Roger Jones    http://www.to.icl.fi/ICLE/rbjpub/rbj.htm
at home        rbj@campion.demon.co.uk