| 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.)
John.