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; Fri, 28 Apr 1995 01:47:19 +0100 Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) id TAA20593 for qed-out; Thu, 27 Apr 1995 19:34:49 -0500 Received: from tuminfo2.informatik.tu-muenchen.de (root@tuminfo2.informatik.tu-muenchen.de [131.159.0.81]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP id TAA20588 for ; Thu, 27 Apr 1995 19:34:43 -0500 Received: from sunbroy14.informatik.tu-muenchen.de ([131.159.0.114]) by tuminfo2.informatik.tu-muenchen.de with SMTP id <26619-3>; Thu, 27 Apr 1995 21:54:52 +0200 Received: by sunbroy14.informatik.tu-muenchen.de id <8067>; Thu, 27 Apr 1995 21:54:43 +0200 From: Konrad Slind To: qed@mcs.anl.gov In-reply-to: <199504271822.UAA01520@muppet53.cs.chalmers.se> (message from Randy Pollack on Thu, 27 Apr 1995 20:22:37 +0200) Subject: Re: Paper on reflection Message-Id: <95Apr27.215443met_dst.8067@sunbroy14.informatik.tu-muenchen.de> Date: Thu, 27 Apr 1995 21:54:41 +0200 Sender: owner-qed@mcs.anl.gov Precedence: bulk Isn't computational reflection problematic for QED? There seems enough difficulty agreeing on a root logic (terms, formulae, theorems, and proofs) without dealing with a formal notion of computation, which as far as I can tell, is necessary for computational reflection, or even Randy Pollack's proposal. Would we have to agree, not only on a root logic, but a root computation system, into which we could translate all our reflected decision procedures? Wouldn't the notionally simple root logic then have to become rather more complex, in order to adequately relate computation and proof? A strong point of the QED proposal was that it forced no choices about the underlying implementation system; however, consideration of computational reflection seems to drag that back in. Konrad.