3 Nov 2009
Utrecht, The Netherlands
EXTRA SESSION OF THE SEMINAR ON THE PHILOSPHY OF MATHEMATICS
On the ocasion of the visits of two eminent speakers,
Peter Hacker from Oxford and Peter Koepke from Bonn,
we are organising a special session of the seminar.
date: 3 November 2009
place: Belle van Zuylenzaal, Academiegebouw, Domplein, Utrecht
programme:
15.00: Peter Hacker: Wittgenstein on the Nature of Mathematical Proof
16.00: Tea
16.30: Peter Koepke: "Mathematical Proofs as Derivation-Indicators -
Theory and Implementation"
All interested are cordially invited to attend. Summaries of the
lectures can be found below.
Ieke Moerdijk
Herman Philipse
------------------------------------------
>
> abstract Hacker:
>
> The lecture is concerned with clarifying Wittgenstein's remarks on the
> nature of mathematical proof. These remarks are obscure, have been
> variously interpreted or misinterpreted, and are central to his
> philosophy of mathematics. The idea that he was defending an eccentric
> form of mathematical existentialism ('full-blooded conventionalism' as
> Dummett dubbed it) is argued to be misconceived. The key to
> understanding his observations is the principle, which he advances,
> that mathematical propositions are norms of representation. It is by
> following through this insight that one can make sense of his
> controversial remarks that in a mathematical proof one wins through to
> a decision. But the 'decision' is not on the truth of the theorem, but
> rather on the consequent concept-formation -- it is a decision to
> employ the resultant concept in one's reasonings.
>
>
> abstract Koepke:
>
> Jody Azzouni proposes a "derivation-indicator view of mathematical practice",
> whereby the components of an ordinary mathematical proof can be taken as
> indicators for building an equivalent formal derivation (Philosophia
> Mathematica, 2004). We interpret the derivation-indicator view in terms of
> formal and computational linguistics. The Naproche system (Natural language
> proof checking) translates natural language mathematical proofs into
> sequences of first-order formulas and checks them for correctness using
> automated theorem provers. The talk will explain relevant linguistic and
> logical foundations and give Naproche examples which look like natural proofs
> yet are fully formal since they are accepted by the Naproche system.