IST is more than an algorithm to prove ZFC theorems
Abstract
Description
There is a sentence in the language of IST, Nelson's internal set theory, which is not equivalent in IST to a sentence in the ZFC language. Thus the Reduction algorithm of Nelson, that converts bounded IST formulas with standard parameters to provably (in IST) equivalent formulas in the ZFC language, cannot be extended to all formulas of the IST language. Therefore, certain IST sentences are "meaningless" from the point of view of the standard universe.