FOM: Completeness of Intuitionistic Logic

[Harvey Friedman]

In posting my posting of Fri, 17 Mar 2000 14:33 on Completeness of
Intuitionistic Logic, I discussed Lauchli's paper, which I read with great
interest in the mid 1980's.

To complete the story, I found a new completeness theorem for HPC around
1986 after pondering Lauchli, and lectured on it at Berkeley. It avoids
using the notion of invariant functional - key to Lauchli's approach.
However, I didn't write a manuscript and I just reconstructed the proof and
wrote it down. But I noticed something important that I don't recall
noticing at the time. And that it works just fine interpreting absurdity in
the normal way!

I also found some written claims stating the result for HQC, but I don't
think I ever lectured or wrote about the details of that. I will look into
this shortly. In fact, I expect that this should work also with absurdity
interpreted in the normal way.

As you will see, my approach here definitely depends on the type structure
- i.e., the same S(phi) used by Lauchli. So there is still the question of
finding an appropriate completeness theorem that interprets absurdity
normally and also does not use a type structure.

COMPLETENESS OF HPC - UNIFORM REALIZATIONS

HPC is the Heyting propositional calculus with atoms A1,A2,..., and, or,
implies, absurdity.

We define the following type structure over any set U.

1. If X is an atom or absurdity then S(X) = U.
2. S(B and C) = S(B) x S(C).
3. S(B or C) = {0} x S(B) union {1} x S(C).
4. S(B implies C) = S(C)^S(B).

An assignment (relative to U) is a map whose domain is a set of atoms and
whose values are subsets of U. We then define f* as follows.

1. f*(absurdity) = emptyset.
2. f*(A) = f(A) if A is in the domain of f.
3. f*(B and C) = f*(B) x f*(C).
4. f*(B or C) = {0} x f*(B) union {1} x f*(C).
5. f*(B implies C) = the set of all f in S(B implies C) such that f maps
f*(B) into f*(C).

We can think of f*(B) as the set of realizers of B.

An assignment for B is an assignment whose domain is exactly the set of
atoms in B.

THEOREM. Let U be an infinite set. A formula B of HPC is provable in HPC if
and only if it has a uniform realizer (relative to U). I.e., if and only if
the intersection of f*(B), taken over all assignments f for B, is nonempty
(relative to U). Furthermore, this result holds if U is chosen to be any
sufficiently large finite set. The sufficient size can be taken to be a
reasonable function in the size of the formula B.