Delivery-Date: Thu Feb 26 20:50:06 2009
Envelope-to: wirth@logic.at
Date: Thu, 26 Feb 2009 14:48:10 -0500
Message-Id: <200902261948.n1QJmA7Q016866@arxiv1.library.cornell.edu>
Precedence: bulk
From: no-reply@arXiv.org
To: wirth@logic.at
Subject: 0902.4682 password (SAVE)
Reply-To: cs@arXiv.org

            *** SAVE THIS MESSAGE FOR FUTURE REFERENCE ***
          (and forward to any collaborators for safekeeping)

Your user/password combination for this article is

 User-ID: 0902.4682
 Password: phrwt

You will need this ID/password pair to do any of the following:

  - to check the article before it is announced
  - to cross-list the article 
  - to add publication information
  - to replace the article with a revised version

Keep this password safe -- all future replacements will require it.

If you submit this article to an overlay journal based on arXiv you may
need to supply the following identifier to allow the collaborating
service to track your submission: arXiv:tracking/9e30cb95cc794117

------------------------------------------------------------------------------
\\
arXiv:0902.4682
From: Claus-Peter Wirth <wirth@logic.at>
Date: Thu, 26 Feb 2009 19:48:01 GMT   (1227kb)

Title: Lectures on Jacques Herbrand as a Logician
Authors: Claus-Peter Wirth, Joerg Siekmann, Christoph Benzmueller, Serge
  Autexier
Categories: cs.LO cs.AI
Comments: ii + 70 pages
Report-no: SEKI Report SR-2009-01
Journal-ref: Dov M. Gabbay & John Woods (eds.). 2009. Handbook of the History
  of Logic, Vol 5: Logic from Russell to Godel
License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
\\
  We give some lectures on the work on formal logic of Jacques Herbrand, and
sketch his life and his influence on automated theorem proving. The intended
audience ranges from students interested in logic over historians to logicians.
Besides the well-known correction of Herbrand's False Lemma by Goedel and
Dreben, we also present the hardly known unpublished correction of Heijenoort
and its consequences on Herbrand's Modus Ponens Elimination. Besides Herbrand's
Fundamental Theorem and its relation to the Loewenheim-Skolem-Theorem, we
carefully investigate Herbrand's notion of intuitionism in connection with his
notion of falsehood in an infinite domain. We sketch Herbrand's two proofs of
the consistency of arithmetic and his notion of a recursive function, and last
but not least, present the correct original text of his unification algorithm
with a new translation.
\\