From owner-qed Wed Oct 26 10:31:05 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id KAA04357 for qed-out; Wed, 26 Oct 1994 10:27:47 -0500
Received: from life.ai.mit.edu (life.ai.mit.edu [128.52.32.80]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id KAA04345 for <qed@mcs.anl.gov>; Wed, 26 Oct 1994 10:27:18 -0500
Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA04028; Wed, 26 Oct 94 11:27:00 EDT
From: dam@ai.mit.edu (David McAllester)
Received: by spock (4.1/AI-4.10) id AA12659; Wed, 26 Oct 94 11:26:58 EDT
Date: Wed, 26 Oct 94 11:26:58 EDT
Message-Id: <9410261526.AA12659@spock>
To: dahn@mathematik.hu-berlin.de
Cc: qed@mcs.anl.gov
In-Reply-To: Dahn's message of Wed, 26 Oct 94 11:18:25 +0100 <9410261018.AA06492@mathematik.hu-berlin.de>
Subject: Remarks on David's Mail of Oct. 25
Sender: owner-qed@mcs.anl.gov
Precedence: bulk


The fact that your system integrates several formalisms seems
interesting.  Does your system have a web page?  (Ontic does not yet,
one of those things I must do.)

   If you ask a mathematician (not being a logician) which logical system
   dominates his thinking, he will - probably - not even understand the
   question!  ... Whether a system is accepted will be much more dependent on
   it's user interface, especially on it's ability to model the language
   normally used by mathematicians.

   The consequence I see for QED is: A QED-system aiming at
   mathematicians should hide the logic unless the user wants access to
   it.

I agree.  Let me use the phrase "Platonic System" to refer to any
verification system whose manual intentionally avoids any mention of
formal inference rules --- it just specifies the semantics of a
machine readable language.  A proof is a sequence of statements each
of which "follows" (by Platonic introspection) from the previous ones.
I believe that mathematicians will never accept having to think about
rules of inference or any other syntactic inference process.  The main
obstacle in constructing an effective Platonic system is constructing
the machinery needed for "Platonic introspection".  It seems that very
sophisticated automated reasoning techniques are required.

   3) Logical systems are concerned with proofs - not with truth
   ([almost] no automated theorem prover incorporated any idea of
   semantics). Therefore, only the syntactic approach makes sense to me.

All the formal languages that I am familiar with have a natural
semantics.  I am not sure what you mean by "few theorem provers
incorporate semantics".  They are all sound (I hope).  It is possible
(easy) to define the semantics formally and formally prove
relationships between syntactic operations and semantic meaning.

Mathematicians are concerned with truth.  From a marketing perspective
it seems better to speak their language.

	David