FOM: Completeness of Intuitionistic Logic

[Harvey Friedman]

I took a closer look at what I claimed in posting 20 Mar 2000 11:03:40 on
Completeness of Intuitionistic Logic, and found that my proof of that
completeness theorem for intuitionistic propositional calculus does not
work for absurdity as I claimed. So at this point I don't have any kind of
BHK interpretation with absurdity treated normally that is complete.

I will restate this completeness theorem carefully using the
"realizability" terminology.

1. ABSURDITY NOT ALLOWED.

HPC is Heyting's propositional calculus based on atoms A_1,A_2,..., and,
or, implies, absurdity.

Let U be a set. We define the type structure over U. We define S(phi,U)
inductively for formulas of HPC without absurdity.

1. S(A,U) = U if A is an atom.
2. S(phi and psi) = S(phi) x S(psi).
3. S(phi or psi) = {0} x S(phi) union {1} x S(psi).
4. S(phi implies psi) = S(psi)^S(phi).

A U-assignment is a function f:{A_1,A_2,...} into P(U). For formulas phi of
HPC without absurdity and U-assignments f, we define

x f-realizes phi under f

as follows.

1. for atoms A, x realizes A under (f,U) if and only if x in f(A).
2. x realizes (phi and psi) under (f,U) if and only if x is of the form
(y,z) where y realizes phi under (f,U) and z realizes psi under (f,U).
3. x realizes (phi or psi) under (f,U) if and only if x is of the form
(i,y) where (i = 0 and y realizes phi under (f,U)) or (i = 1 and y realizes
psi under (f,U)).
4. x realizes (phi implies psi) under (f,U) if and only if x in S((phi
arrows psi),U) and for all y, if y realizes phi under (f,U) then x(y)
realizes psi under (f,U).

We say that x is a uniform realizer of phi under U if and only if for all
U-assignments f, x realizes phi under (f,U).

THEOREM 1. Let U be an infinite set. A formula phi of HPC without absurdity
is provable in HPC if and only if it has a uniform realizer under 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 phi.

2. ABSURDITY ALLOWED.

What does this tell us about formulas with absurdity? We can extend this
semantics in order to incorporate absurdity, but allowing realizers of
absurdity. We then have the same result, and it can be obtained as an easy
Corollary. So there is nothing gained by doing the "exploding" semantics
beyond what we have without absurdity. Here are the details.

Let U be a set. We define the type structure over U. We define S(phi,U)
inductively for all formulas phi of HPC.

1. S(A,U) = U if A is an atom or absurdity.
2. S(phi and psi,U) = S(phi) x S(psi).
3. S(phi or psi,U) = {0} x S(phi) union {1} x S(psi).
4. S(phi implies psi,U) = S(psi)^S(phi).

An exploding U-assignment is a function f:{absurdity,A_1,A_2,...} into P(U)
such that for all n >= 1, f(absurdity) containedin A_n. For formulas phi of
HPC and exploding U-assignments f, we define

x f-realizes phi under f

as follows.

1. if A is an atom or absurdity, then x realizes A under (f,U) if and only
if x in f(A).
2. x realizes (phi and psi) under (f,U) if and only if x is of the form
(y,z) where y realizes phi under (f,U) and z realizes psi under (f,U).
3. x realizes (phi or psi) under (f,U) if and only if x is of the form
(i,y) where (i = 0 and y realizes phi under (f,U)) or (i = 1 and y realizes
psi under (f,U)).
4. x realizes (phi implies psi) under (f,U) if and only if x in S((phi
implies psi),U) and for all y, if y realizes phi under (f,U) then x(y)
realizes psi under (f,U).

We say that x is a uniform realizer of phi under U if and only if for all
U-assignments f, x realizes phi under (f,U). This definition obviously
agrees with the previous definition of uniform realizers for phi that do
not mention absurdity.

THEOREM 2. Let U be an infinite set. A formula phi of HPC is provable in
HPC if and only if it has a uniform realizer under 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 phi.

Here is why Theorem 2 is an easy Corollary of Theorem 1. Let phi be a
fomula of HPC. Treat absurdity as just another atom, B. It then suffices to
show that phi* =

((B implies A_1) and ... and (B implies A_n)) implies phi'

is provable in HPC, and phi' is obtained from phi by replacing absurdity
with B. It can be verified that the uniform realizer of phi in the sense of
the exploding semantics is a uniform realizer x of phi* in the absurdity
free semantics. Hence phi* is provable in HPC.