Delivery-Date:
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