FOM: Completeness of Intuitionistic Logic

[Harvey Friedman]

I have to again back off of the formulation of 2.1 and 2.2 in 2:22PM 
3/17/00. Let me try again.

notA or notnotA, the same formula that Lacuchli cited in his 
abstract, is also a problem here.

I will now stop calling these statements almost Theorems - even 
though they get weaker, and more likely to be OK. I've got to get 
back to Boolean relation theory.

CONJECTURE 2.1. Let phi be a formula of HPC without negation. 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.

CONJECTURE 2.2. Let phi be a formula of HPC without negation. 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.

There remains the question of just how we want to handle sentences 
with negation. But back to Boolean relation theory.