FOM: Strength of NSA (was: Monomathematics and Friedman)

[David Ross]

Neil Tennant raises the following question about formal nonstandard analysis:
> 
> 3. There is no blow-up in length of proof of S-free theorems as one
> passes from nsT to T.

This is unlikely; a couple of papers from the mid-1980s by Henson, Kaufmann,
and Keisler show that NSA has a higher formal proof strenth than standard
analysis. I don't remember the details too well, but one of the results said
something like adding Beth_n^+-saturation to PA makes it possible to prove
results with n fewer quantifier alternations.  (Hopefully somebody on this
list has a fresher memory of these results than I do!)

- David (ross at tarski.math.hawaii.edu)