Replied: Wed, 26 Oct 1994 12:07:30 -0500 Replied: "Piotr Rudnicki " From owner-qed Wed Oct 26 11:47:24 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id LAA06116 for qed-out; Wed, 26 Oct 1994 11:46:36 -0500 Received: from scapa.cs.ualberta.ca (root@scapa.cs.ualberta.ca [129.128.4.44]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id LAA06108 for ; Wed, 26 Oct 1994 11:46:29 -0500 Received: from sedalia.cs.ualberta.ca by scapa.cs.ualberta.ca id <18549-5>; Wed, 26 Oct 1994 10:46:17 -0600 Subject: Re: PRA as a foundation From: Piotr Rudnicki To: dam@ai.mit.edu (David McAllester) Date: Wed, 26 Oct 1994 10:45:39 -0600 (MDT) Cc: qed@mcs.anl.gov In-Reply-To: <9410251556.AA12499@spock> from "David McAllester" at Oct 25, 94 11:56:28 am X-Mailer: ELM [version 2.4 PL23] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Content-Length: 1160 Message-Id: <94Oct26.104617-0600_(mdt).18549-5@scapa.cs.ualberta.ca> Sender: owner-qed@mcs.anl.gov Precedence: bulk > Objective 4. The logic in which translations are verified should be as > primitive as possible so as to be acceptable to the widest possible variety > of logicians. David's comments the above objective: > Objective 4 seems to dictate a syntactic approach to verifying > translators. If f is a translator from system S1 to system S2 the > correctness theorem states that if S1 |- Phi then S2 |- f(Phi). I was > confused about the role of PRA here and assumed that a central use of > PRA would force the translation f(Phi) to be a "meta" formula rather > than a "Platonic" formula (one that talks directly about arbitrary > sets). But nothing here is preventing f(Phi) from being a direct > (Platonic) set-theoretic formula. PRA seems adequate once we are > committed to a syntactic approach to verifying translators. > If we have n systems, then we need n*(n-1) translators. Sounds like a bit of work unless n = 1. Another approach is to have one, very strong system, into which anything can be translated, and from which we can translate, but not everything, into weaker systems. This needs only 2(n-1) translators. -- Piotr (Peter) Rudnicki