FOM: Completeness of Intuitionistic Logic

[urquhart@urquhart.theory.toronto.edu]

Harvey Friedman's interesting posting on intuitionistic 
logic has close connections with an old paper of Hans
Lauchli, "An abstract notion of realizability for which
intuitionistic predicate calculus is complete."  This
was published in "Intuitionism and Proof Theory", 
the proceedings of the Summer Conference at Buffalo, 1968.

In his paper, Lauchli works within a simple type structure
built up from two countably infinite sets Gamma and Pi, one representing
the individuals and the other representing an abstract set
of primitive proofs.  The interpretation of formulas is essentially
the same as Friedman's, with an exception noted below.
He then proves the following things to be equivalent:

1.  A is provable is Heyting's predicate logic;
2.  F(A) contains a definable functional;
3.  F(A) contains an invariant functional.

Here, "invariant" means "invariant under permutations of
Gamma union Pi."  

The one difference from the interpretation proposed by Harvey Friedman is 
that the False can have a non-empty set of proofs assigned to it,
subject to the constraint that every proof of the False is a proof
of any atomic sentence.  Without this generalization (i.e. if we
insist that the False have no proofs), there are counter-examples to
completeness.  Lauchli gives the counter-example 

	~~Av( R(v) v ~R(v)).

Presumably this generalization is not needed for the propositional case.

I would guess that one could use Fraenkel-Mostowski permutation model ideas
to prove the conjectured Theorem 2, starting from Lauchli's result on
invariant functionals.

Alasdair Urquhart