Post #2264411

@johncarlosbaez@mathstodon.xyz @typeswitch@gamedev.lgbt but still, what is wrong with the following reasoning: Since IST is a conservative extension of ZF(C), we have that the reduct of IST models (forgetting the additional structure on these models) gives us ZF(C) models. That means: via IST we get non standard models of ZF(C). In these, we cannot prove via ZF(C) machinery that the nonstandard elements are there, but we know it from our meta view knowing that this is a reduct coming from an IST model.