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
Replied: Wed, 26 Oct 1994 12:07:30 -0500
Replied: "Piotr Rudnicki <piotr@cs.ualberta.ca> "