FOM: Strength of NSA (was: Monomathematics and Friedman)
David Ross
ross at math.hawaii.edu
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 tarski.math.hawaii.edu)
More information about the FOM
mailing list