Re: Paper on reflection

Roger Bishop Jones (rbj@campion.demon.co.uk)
Thu, 27 Apr 1995 07:06:16 GMT

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