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 04:55:25 +0100 Received: (from listserv@localhost) by antares.mcs.anl.gov (8.6.10/8.6.10) id WAA22283 for qed-out; Thu, 27 Apr 1995 22:49:12 -0500 Received: from pnl.gov (gate.pnl.gov [130.20.64.36]) by antares.mcs.anl.gov (8.6.10/8.6.10) with ESMTP id WAA22266 for ; Thu, 27 Apr 1995 22:49:02 -0500 Received: from ccmail.pnl.gov by pnl.gov (PMDF V4.3-13 #6012) id <01HPUI7OHMO000004Y@pnl.gov>; Thu, 27 Apr 1995 20:49:33 -0700 (PDT) Date: Thu, 27 Apr 1995 20:49 -0700 (PDT) From: ma_friesel@gate.pnl.gov Subject: Re[2]: Paper on reflection To: qed@mcs.anl.gov, slind@informatik.tu-muenchen.de Message-id: <01HPUI7OKAQA00004Y@pnl.gov> MIME-version: 1.0 Content-transfer-encoding: 7BIT Sender: owner-qed@mcs.anl.gov Precedence: bulk Perhaps the challenge is not to make a computationally >perfect< system, but to make an effective system with enough flexibility to be improved? MAF 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.