FOM: 3 forms over HA/effective topos

[Harvey Friedman]

Franzen appropriately mentions that

>   forall x exists y P(x,y)
>
>   not not forall x exists y P(x,y)
>
>   forall x not not exists y P(x,y)
>
>where P(x,y) is primitive recursive, are intuitionistically distinct, at
>least in terms of provable equivalence in HA.

In fact, for primitive recursive P, HA proves 1 implies 2 implies 3. But
there exists primitive recursive P (with only x,y free) such that these are
strict implications.

Mossakowski 12:30PM 2/13/98 writes:

>Zermelo-Fraenkel set theory is one answer to Russell's paradox: it
>carefully limits comprehension, while keeping classical logic.
>But there also is another answer: keep unlimited comprehension, but not
>classical logic.

But unlimited comprehension with the barest of logic is equally
inconsistent. Later he indicates that he is talking about using lambda
calculi for f.o.m. But the usual ones do not support standard extensional
equality with definition by cases, as well as other things needed for
normal f.o.m. It's too logic free.

I am under the impression that the effective topos is also a direct
translation of recursive realizability notions for intuitionistic set
theory, which I developed in the 60's, following earlier work of Kleene, and
Kreisel for second order arithmetic.