FOM: Friedman and Mayberry: beyond sterility

[Colin McLarty]

Harvey Friedman <friedman at math.ohio-state.edu> wrote:

on expressibility in first and second order logic:

>The appropriate way to look at this is as follows. There is the
>first order language of set theory. It is then trivial to express such
>concepts as "inductive number system" in this first order language of set
>theory. Since there are no axioms and rules of inference involved here,
>there is no issue as to "nonstandard models" and the like. And this is the
>normal concept of "express" that mathematicians use.

        This seems to me quite correct. As Harvey says, this language has
"no axioms and no rules of inference" and so there is "no issue as to
standard models" and it is the way mathematicians normally express
themselves. I believe this language is just what John Mayberry means by "set
theory". 

        This language is not itself a formal theory though it can be quite
directly formalized in first order terms. The formalized version does have
axioms and the usual first order rules of inference, and mathematicians
rarely bother with it. 

        Mayberry has stressed all along the value of such formalization--the
only way to tell what does NOT follow from our set theory is to see what is
NOT deducible in the formalized version. (E.g. AC is not deducible from ZF.)
But the formalization remains a way of elucidating the actual set theory. 

        The formalization, which has axioms and rules and issues about
models, and is not normally used by mathematicians, is a tool for
mathematical knowledge but not the basis of it.