From qed-owner Mon Aug  9 09:46:53 1993
Received: by antares.mcs.anl.gov id AA27389
  (5.65c/IDA-1.4.4 for qed-outgoing); Mon, 9 Aug 1993 09:34:14 -0500
Received: from mail.Germany.EU.net by antares.mcs.anl.gov with SMTP id AA27382
  (5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>); Mon, 9 Aug 1993 09:34:07 -0500
Received: by mail.Germany.EU.net(EUnetD-2.3.0.g) via EUnet
	id GM06812; Mon, 9 Aug 1993 16:31:50 +0200
Received: from hubinf.informatik.hu-berlin.de by hp832.informatik.hu-berlin.de with SMTP
	(15.11/15.6) id AA17629; Mon, 9 Aug 93 13:48:22 mes
Received: from noether.hu-berlin.de by hubinf (4.1/SMI-4.1)
	id AA19189; Mon, 9 Aug 93 13:51:49 +0200
Date: Mon, 9 Aug 93 13:51:49 +0200
From: dahn@hubinf.informatik.hu-berlin.de (Dahn)
Message-Id: <9308091151.AA19189@hubinf>
To: qed@mcs.anl.gov
Subject: Re:  QED-like Efforts
Sender: qed-owner

Certainly there will be numeruous proof systems, calculi, philosophies etc. and people like to stay with the things they know and they can efficiently work with.
So, why not - in a first phase - encourage people to verify in their own system the stuff (set theory, universal algebra, syntactic properties) necessary to verify the completeness of other systems?
Then a verification in any of the verified systems would be as good as a verification in the original system.

Bernd, Ingo Dahn