[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