FOM: Relative completeness of Heyting logic

[William Tait]

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