[Prev][Next][Index][Thread]

LaTeX version of article



Date:     Thu, 15 Nov 90 12:14:24 EST

EXCLUDED MIDDLE WITHOUT DEFINITE DESCRIPTIONS IN THE THEORY OF
CONSTRUCTIONS


A LaTeX version of this article, which I circulated on TYPES two
months ago, in now available by anonymous ftp from
clyde.concordia.ca (132.205.1.1); the file is /pub/seldin.dvi.
For those who do not have access to anonymous ftp, I am prepared
to send a uuencoded (or, if you prefer, by tarmail) version of
the file in response to requests by e-mail.

The paper is a response to a posting by Garrel Pottinger a year
ago which shows that excluded middle together with definite
descriptions in the calculus of constructions implies proof
degeneracy:  that any two terms in a small type (a type in Prop)
are equal in the sense of Leibniz equality.  In this paper it is
shown proof-theoretically that excluded middle alone does not
imply proof degeneracy.  This is done by proving consistent a set
of assumptions sufficient for classical arithmetic; since one of
the Peano axioms asserts that zero is not a successor, and since
the numerals involved are all in a small type, this consistency
is incompatible with proof degeneracy.

Jonathan P. Seldin
Internet:				seldin@antares.concordia.ca
Bitnet:						       seldin@conu1