FOM: Completeness of Intuitionistic Logic

[Harvey Friedman]

In the middle of my continuing frenzied development of Boolean Relation
Theory, I took a break and briefly focused my attention on completeness of
intutionistic propositional calculus (HPC). This was prompted by an
interesting week long visit to OSU by Sergei Artemov who presented, among
other things, his proof polynomial approach to HPC and more generally, S4.
The proof polynomial approach is seemingly unrelated to what we discuss
here.

We go all the way back to the informal BHK (Brouwer, Heyting, Kolmogorov)
interpretation of intuitionistic logic. One version of this informal
interpretation is as follows:

1. The proofs of A &B are the pairs of proofs of A and B.
2. The proofs of A v B are the proofs of A and the proofs of B.
3. The proofs of A implies B are the mappings from the proofs of A to the
proofs of B.
4. There are no proofs of absurdity.

The BHK interpretation is actually more flexible than this. For instance,
we can replace 3 with

3'. The proofs of A implies B are certain functions which send proofs of A
to proofs of B.

It is very important to deal with 3'. This leads to the general concept of
"a BHK interpretation" rather than "the BHK interpretation." But in this
initial posting we restrict to 1-4.

We now take 1-4 literally in set theory. Thus we can define a set theoretic
interpretation of HPC as a map F from all propositional formulas into sets
obeying the following conditions:

1. F(A & B) = F(A) x F(B).
2. F(A or B) = F(A) union F(B).
3. F(A implies B) = the set of functions from F(A) into F(B).
4. F(absurdity) = emptyset.

An obvious variant is:

1. F(A & B) = F(A) x F(B).
2. F(A or B) = F(A) x {0} union F(B) x {1}.
3. F(A implies B) = the set of functions from F(A) into F(B).
4. F(absurdity) = emptyset.

The folllowing theorem is straightforward.

THEOREM 1. Phi is a tautology if and only if F(phi) is nonempty under every
set theoretic interpretation if and only if ZFC proves F(phi) is nonempty
under every set theoretic interpretation.

However, it appears that we have obtained the following result:

THEOREM 2. Phi is provable in HPC if and only if ZF proves F(phi) is
nonempty under every set theoretic interpretation.

I simply don't have the time right now to properly check this proof, and I
am keeping this stuff off of the numbered postings until I get some time
away from Boolean Relation Theory.

But I am throwing this out for comment and discussion on the FOM -
including somebody coming up with a counterexample to this, which would be
very useful to me.

PS: I suspect that things will work out just fine for HQC = Heyting
quantificational calculus. In particular, absurdity can be treated in the
normal way.