From owner-qed Thu Sep  1 09:37:01 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA28403 for qed-out; Thu, 1 Sep 1994 09:35:22 -0500
Received: from compu735.mathematik.hu-berlin.de (compu735.mathematik.hu-berlin.de [141.20.54.12]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id JAA28396 for <qed@mcs.anl.gov>; Thu, 1 Sep 1994 09:35:08 -0500
Received: from kummmer.mathematik.hu-berlin.de by compu735.mathematik.hu-berlin.de with SMTP
	(1.37.109.8/16.2/4.93/main) id AA10235; Thu, 1 Sep 1994 16:29:10 +0200
Received: from orion.mathematik.hu-berlin.de by mathematik.hu-berlin.de (4.1/SMI-4.1/JG)
	id AA28827; Thu, 1 Sep 94 16:35:07 +0200
Date: Thu, 1 Sep 94 16:35:07 +0200
From: dahn@mathematik.hu-berlin.de (Dahn)
Message-Id: <9409011435.AA28827@mathematik.hu-berlin.de>
To: qed@mcs.anl.gov
Subject: Types and sets
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

N.G. de Bruijn says:

>>  Since the teaching of Bourbaki very many pure mathematicians feel that
>>  they should think that all their objects are untyped sets, but what
>>  does that really mean for them?

BUT: Most mathematicians use types and will reject ill-typed expressions.

Ken Kunen wrote:

>>  Even books (such as mine) on pure set theory often use typing to facilitate
>>  the exposition.  For example, borrowing from Fortran, we say:
>>  "we use Greek letters alpha,beta,gamma ... to vary over ordinals".

Recall Paul Halmos's nightmare of a mathematician from his paper "How to write mathematics": A sequence epsilon_n that tends to infinity if n tends to 0.

The advantage of set theory is, that it enables a typed language with quantifiers "for all X in Y ..." and "for some X in Y ...", but it does not enforce it. Many things in mathematics can be expressed by Delta_0-formulas, i. e. using only these bounded quantifiers, but some - like the existence of a power set - cannot.

A major advantage of types for proving theorems in Mathematics is, that they help chosing the knowledge to use in order to prove a specific theorem. In order to prove a theorem on real numbers, in the first run only knowledge on real numbers will be used. This is a concious strategic decision of the prover - it is not enforced by the logic and it can be wrong. E. g. in order to prove the intermediate value theorem for polynomials - a statement that involves only numbers and arithmetic operations - it is necessary, to consider the reals as a set, either using properties of it's subsets or properties of the real numbers themselves as sets.

In order for a QED project to attract mathematicians it should - like set theory - support the use of types but not enforce it.

Ingo Dahn