FOM: Relative completeness of Heyting logic

William Tait wwtx at
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
5522 S. Everett Ave
Chicago, IL 60637
(773) 241-7288

More information about the FOM mailing list