From owner-qed Tue Oct 25 07:59:00 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id HAA15969 for qed-out; Tue, 25 Oct 1994 07:54:50 -0500
Received: from compu735.mathematik.hu-berlin.de (compu735.mathematik.hu-berlin.de [141.20.54.12]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id HAA15955 for <qed@mcs.anl.gov>; Tue, 25 Oct 1994 07:54:17 -0500
Received: from kummer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
	(1.37.109.8/16.2/4.93/main) id AA09107; Tue, 25 Oct 1994 13:53:44 +0100
Received: from wega.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
	id AA03500; Tue, 25 Oct 94 13:53:51 +0100
Date: Tue, 25 Oct 94 13:53:51 +0100
From: dahn@mathematik.hu-berlin.de (Dahn)
Message-Id: <9410251253.AA03500@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: PRA as a foundation
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

Before the beginning of modern logic, Leibniz demanded a calculus such that any kind of dispute could be decided by "calculating". The problem with constructivism is, of course,that people don't agree which calculi are reliable. 

Nevertheless, PRA or something alike is accepted by many people to be able to express correctly the basic properties of finite objects like formulas or proofs. Therefore it can serve as a tool to express things like "P is a proof of sentence A from theory T in logic L" (NOT: "A is a logical consequence of T").

I doubt, whether such a translation to PRA is necessary for the acceptance of QED. One might be able to encode proofs from other systems in PRA in linear time and the authors of the proofs may feel better if the encoding went through without errors. But who would by the product - i.e. the encoded proof? (Contrary to David I believe that a translation back from PRA into other calculi will take at least exponential time [I know that this happens even for translations between fairly similar calculi like Modified Problem Reduction, Simplified Problem Reduction and Model Elimination]. The reason is that the structure of a proof contains implicitely information that has been useful in the specific calculus to build that proof. This information is lacking in a proof produced with another calculus).

HOWEVER I have no doubt, that the development of a central bookkeeping system is very useful for the development of QED because it encourages cooperation and exchange.

Ingo Dahn