[FOM] 606: Simple Theory of Types

[Harvey Friedman]

On Sun, Aug 30, 2015 at 5:39 AM, Sam Sanders <sasander at cage.ugent.be> wrote:

> Dear Harvey,
>
> As you have pointed out in the past, a non-trivial aspect of Reverse Math
> is the representation (aka “coding”) of mathematical objects in
> second-order arithmetic.
> In your below posting, you also suggest that low levels of the type
> hierarchy suffice for formalising mathematics.
>
> In general, I agree with that statement, but there are however non-trivial
> exceptions (which seem to tank associated grand claims).
>

​My posting 606 is mainly concerned with the interpretation power of the
simple theory of types, and other type schemes with full comprehension. Not
any issues connected with refined foundations of mathematics such as
Reverse Mathematics and coding issues. The logical strength of 3rd order
arithmetic is ridiculously strong by most standards.

What I have seen about trying to do RM at higher types, including what you
are mentioning, is not nearly refined enough for that purpose, but may
serve some special purposes.

The GOLD STANDARD is SRM = strict reverse mathematics, which allows no
coding whatsoever, so everything is up front. Of course, the biggest issue
for SRM is whether is can be pulled off with some strong form of
ROBUSTNESS. The answer is yes, but not without difficulty, and I owe some
papers on this after the one I published, which only scratches the surface,
and desperately needs to be improved on and further developed.

Harvey Friedman
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20150830/f3dbcf03/attachment.html>