Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually mcs.anl.gov !OR! owner-qed@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 25 Apr 1995 20:41:34 +0100 Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) id OAA23984 for qed-out; Tue, 25 Apr 1995 14:32:03 -0500 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP id OAA23978 for ; Tue, 25 Apr 1995 14:31:43 -0500 Received: from auk.cl.cam.ac.uk (user jrh (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 25 Apr 1995 20:13:59 +0100 To: qed@mcs.anl.gov Subject: Re: Paper on reflection In-reply-to: Your message of "Tue, 25 Apr 1995 06:26:22 GMT." <3765@campion.demon.co.uk> Date: Tue, 25 Apr 1995 20:13:54 +0100 From: John Harrison Message-ID: <"swan.cl.cam.:139810:950425191403"@cl.cam.ac.uk> Sender: owner-qed@mcs.anl.gov Precedence: bulk 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.) John.