FOM: Completeness of Intuitionistic Logic

[Harvey Friedman]

Todd Wilson and Arnon Avron pointed out to me that ZF obviously proves
F(A v notA) is nonempty under every set theoretic interpretation, and 
so my "almost theorem" is false as stated.

I forgot to put in the uniformity needed, and restate this below.

The earlier posting with this error is

Completeness of Intuitionistic Logic, Thu, 16 Mar 2000 09:43.

MORALE: Be slow to trust anybody who claims something substantial while
he/she is working feverishly on something else.

So here is a self contained restatement of the situation which is also more
informative than the 9:43AM 3/16/00 posting. Note that we have changed the
notation somewhat to make it easier to state the result (and further
results that we anticipate).

WARNING: I am still working feverishly on something else - Boolean relation
theory.

1. LAUCHLI PAPER.

Lauchli published a very interesting paper in

H. Lauchli, An abstract notion of realizability for which intuitionistic
predicate caluclus is complete, p. 227-234,  ed. Kino, Myhill, Vesley,
Proceedings of the 1968 Summer Conference at Buffalo, North-Holland, 1970.

I studied this paper in the mid 1980's.

Here he gives a completeness theorem for predicate calculus - extending an
earlier completeness theorem for propositional calculus that he claims in

H. Lauchli, Intuitionistic propositional calculus and definably non-empty
terms (abstract), JSL 30, no. 2 (1965).

In this posting, we discuss only the propositional calculus HPC, postponing
discussion of the predicate calculus HQC to when I have more time to 
go into this in serious detail. It is
assumed that the atoms of HPC are the letters A_1,A_2,... .

Lauchli first fixes an infinite set U. (He actually requires that U be
countable, but that is irrelevant for our puposes). He starts by
associating a type to every formula of HPC (relative to U) as follows:

1. S(A_n) = U, n >= 1.
2. S(absurdity) = V.
3. S(B & C) = S(B) x S(C).
4. S(B or C) = ({0} x S(B)) union ({1} x S(C)).
5. S(B arrows C) = S(C)^S(B).

He defines a proof assignment (relative to U) as any function f which
assigns to every formula B in a set f(B) as follows:

1. f(A_n) containedin U, n >= 1.
2. f(absurdity) containedin U.
3. f(B & C) = f(B) x f(C).
4. f(B or C) = {0} x f(B) union {1} x f(C).
5. f(B arrows C) = the set of all functions g in S(B arrows C) such that g
maps f(B) into f(C).
6. f(absurdity) containedin f(A_n), n >= 1.

THEOREM 1.1. (Lauchli). Let phi be a formula of HPC. The following are
equivalent relative to any fixed countably infinite set U.
a) phi is provable in HPC.
b) there is a simple theta such that for all proof assignments f, theta
lies in f(A).
c) there is an invariant theta such that for all proof assignments f, theta
lies in f(A).
d) for all proof assignments f there is a simple theta such that theta lies
in f(A).
e) for all proof assignments f there is an invariant theta such that theta
lies in f(A).

Here simple means given by a closed term in the typed lambda calculus (set
up for the type structure S). Here invariant means invariant under all
permutations of V.

Lauchli mentions in a previous abstract of his to which he refers, 
that if we require f(absurdity) = emptyset, either d) or e) imply a). 
He takes phi = notphi or notnotphi.

In his paper, Lacuchli also shows that in the case of HQC, that 
f(absurdity) = emptyset, then then neither b) nor c) nor d) nor e) 
imply a) for HQC. He gives the example

notnotB = notnot forallx(R(x) or notR(x)).

Here under any proof assignment f, f(S(notnotB)) in his setup for HQC 
is all of S(notnotB).

2. Striving for perfection.

I got interested in trying to reflect more literally the BHK (Brouwer,
Heyting, Kolmogorov) writings about the informal interpretation of HPC and
HQC. It seems that it makes sense to strive for perfection.

Obviously the notion of simple and invariant in Lauchli need to be removed
if we are moving towards perfection.

For perfection, we also need to have f(absurdity) = emptyset. Also, 
in my opinion, we need to remove the type structure S(B) above.

In order to avoid confusion, we will change terminology. We are now in the
context where there are no S's.

Let phi be a formula of HPC. A phi assignment is a function f from the
atoms of phi into sets,

We then extend f to a function f* from the set of formulas of HPC whose
atoms are included in the domain of f, into sets, as follows:

1. f*(x) = f(x), provided x is in the domain of f.
2. f(B & C) = f(B) x f(C).
3. f(B or C) = {0} x f(B) union {1} x f(C).
4. f(B arrows C) = f(C)^f(B).
5. f(absurdity) = emptyset.

We believe that this should work, and will write the details as soon 
as we get a break from Boolean relation theory. Counterexamples are 
most welcome. Thanks to those who provided them for the earlier 
version.

(almost) THEOREM 2.1. Let phi be a formula of HPC. The following are 
equivalent.
a) phi is provable in HPC.
b) it is provable in NBG that there is a class function H
which maps every phi assignment f to an element of f*(phi).
c) it is provable in MK that there is a class function H which maps 
every phi assignment f to an element of f*(phi).

The version for ZF is not quite as elegant.

(almost) THEOREM 2.2. Let phi be a formula of HPC. The following are 
equivalent.
a) phi is provable in HPC.
b) it is provable in ZF that for every set U there is a function H which
maps every phi assignment f whose values are subsets of U to an element
of f*(phi).

This is to be proved using forcing combined with the permutation group approach
in Lauchli. However, the relevant kind of invariance needed for this
forcing argument is weaker than the notion of invariance in Lauchli's work,
and so one has to modify the arguments from scratch.

More later - when I get a break.