FOM: Completeness of Intuitionistic Logic

Harvey Friedman friedman at math.ohio-state.edu
Fri Mar 17 16:40:17 EST 2000

```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.

```