Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (actually antares9.mcs.anl.gov !OR! owner-qed@mcs.anl.gov) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Fri, 12 Aug 1994 00:53:03 +0100 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id SAA22491 for qed-out; Thu, 11 Aug 1994 18:47:27 -0500 Received: from SAIL.Stanford.EDU (SAIL.Stanford.EDU [36.28.0.130]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id SAA22486 for ; Thu, 11 Aug 1994 18:47:21 -0500 Received: by SAIL.Stanford.EDU (5.57/25-eef) id AA26452; Thu, 11 Aug 94 16:47:19 -0700 Date: Thu, 11 Aug 94 16:47:19 -0700 From: John McCarthy Message-Id: <9408112347.AA26452@SAIL.Stanford.EDU> To: qed@mcs.anl.gov Subject: translation into a standard language Reply-To: jmc@cs.stanford.edu Sender: owner-qed@mcs.anl.gov Precedence: bulk This is inspired by Peter Andrews's message. He discusses translating theorems and proofs from one system to another. I think that translating theorems is needed and translating proofs, which is much harder, can be dispensed with. I suspect that set theory can serve as a universal language. Every system can have a translator into set theory for its theorems. However, most likely only a subset of set theory will be translatable into systems like Boyer-Moore in any automatic way. The translator for Boyer-Moore should recognize what it can translate. The set theory itself used as a universal language need not have a prover of its own and quite likely will not be the same as the language of someone's set theory based prover.