FOM: Relative completeness of Heyting logic
William Tait
wwtx at midway.uchicago.edu
Tue Apr 4 14:45:40 EDT 2000
I have recently returned from email-free land and noticed a number of
messages, notably by Harvey Friedman, about the completeness of
Intuitionistic logic. I haven't yet had time to read through them;
but I have a result which bears on the question. I don't know if it
is otherwise known.
I have proved that any first-order formula deducible in the
Curry-Howard theory of types C-H is already deducible in Heyting's
formailzation of first-order intuiitionistic logic, HL. The
difference in these systems is essentially in the rule for
existential quantifier elimination. In the theory of types, it leads
from a deduction p of \exists x:D. F(x) to a term p1 of type D and a
deduction p2 of F(p1). Thus, even when \exists x:D. F(x) is
first-order (with D the domain of individuals, deductions in C-H may
involve formulas, e.g. F(p1), which are not first-order. I have shown
that, nevertheless, any consequence relation Gamma |- A deducible in
C-H, where Gamma and A are first-order, is already deducible in HL.
(I announced some time ago in print recollecting that I had proved
this in the early '70's, but was not able to find a proof in my
notes. As a matter of fact, when I did write up a proof, still some
years ago now, it was defective---as was pointed out to me last
autumn by Frank Pfenning. So my claim to an earlier proof should be
treated with some skepticism---I so treat it.)
Incidently---and not surprisingly, the method of proof extends to
higher order logic as well.
Bill Tait
--
William W. Tait
Professor Emeritus of Philosophy
University of Chicago
wwtx at midway.uchicago.edu
Home:
5522 S. Everett Ave
Chicago, IL 60637
(773) 241-7288
More information about the FOM
mailing list