FOM: History of IZF and IHOL

[Colin McLarty]

Steve Simpson wrote: 

>Harvey pointed out to me that the logical aspects of the PER model are
>closely related to realizability as developed a long time ago in
>papers by Kleene, Kreisel, and Harvey himself.  I don't think this
>work was influenced by topos theory in any way.

        This is an interesting question to me. Prior to the Lawvere-Tiernay
axioms for topos theory, "higher order intuitionistic logic" included
substantial restrictions on comprehension. Troelstra gives 52 named axiom
systems in his book "Metamathematical investigation of intuitionistic
arithmetic and analysis" (Springer, 1973), and many more un-named variants,
none of which count every well-formed instance of separation as an axiom.
Some require the defining property to be decidable, others primitive
recursive, and so on. Dana Scott is even careful *not* to assume his
intuitionistic predicates are extensional in his article "Extending the
topological interpretation to intuitionistic analysis I" (Compositio
Mathematica vol.20, 1968, pp.194-210).  

        I suppose the reason is this: Studies of intuitionistic logic aimed
largely at spelling out Brouwer's ideas, and Brouwer had wanted sharply
limited means of set formation and identification. But I would like to hear
from people who were there.

        So far as I have found, Lawvere "Adjointness in foundations" (Dialectica
vol.23, 1969, pp.281-296) is the first work to suggest intuitionistic higher
order logic with separation using all formulas: For every formula Phi(x)
with x a variable over a set X there is a term 
{x in X| Phi(x)} and the axiom:

                y in {x in X| Phi(x)}  IFF  Phi(y)

Here { and } are curly brackets, in case they print as something else on
your e-mail editor.

        Lawvere uses intuitionistic logic and this naive separation axiom
because they are satisfied in the mathematical examples, and he was not
interested in Brouwer's ideas. For the same reason he uses extensionality
for all subsets of a given set.

        By 1971 Dana Scott and John Myhill were familiar with Lawvere's
ideas. Both had papers at the January 1971 conference in Dalhousie reported
in the book "Toposes, algebraic geometry and logic" (Springer-Verlag, 1972).

        Through the 1970s it became normal to study intuitionistic set
theory or higher order logic with the full separation axiom and
extensionality. Myhill was working on this in 1971 along with Harvey
Friedman. So far as I know Friedman's first publication on it was "Some
applications of Kleene's methods for intuitionistic systems" in the book
"Cambridge Summer School in Mathematical Logic" Edited by Mathias and Rogers
(Springer-Verlag, 1973) all presented in summer 1971.

        Myhill was always happy to talk about his interest in topos theory.
So I would be surprized if Friedman did not hear of it from him. Of course,
"hearing of" need not imply much influence. And Friedman's main tool was
realizability, which topos theorists did not work with at that time.   
 
        I would like to hear more about this from Friedman, Scott, and
others who were there. From your viewpoint, how and why did "intuitionistic"
set theory and higher order logic stop putting decidability or effectiveness
restrictions on separation/replacement and equality? Did topos theory have
an influence? 

Colin