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

David Ross ross at
Mon Nov 17 10:37:43 EST 1997

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

More information about the FOM mailing list