The effective content of Reverse Nonstandard Mathematics and the nonstandard content of effective Reverse Mathematics

• Published in 2015
• Added on 2015-11-19

The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis pertaining to Reverse Mathematics (RM). In particular, we shall establish RM-equivalences between theorems from Nonstandard Analysis in a fragment of Nelson's internal set theory. We then extract primitive recursive terms from Goedel's system T (not involving Nonstandard Analysis) from the proofs of the aforementioned nonstandard equivalences. The resulting terms turn out to be witnesses for effective1 equivalences in Kohlenbach's higher-order RM. In other words, from an RM-equivalence in Nonstandard Analysis, we can extract the associated effective higher-order RM-equivalence which does not involve Nonstandard Analysis anymore. Finally, we show that certain effective equivalences in turn give rise to the original nonstandard theorems from which they were derived.

Links

• http://arxiv.org/abs/1511.04679
• http://arxiv.org/pdf/1511.04679v1

Other information

BibTeX entry

@article{Sanders2015,
	key = {Sanders2015},
	type = {article},
	title = {The effective content of Reverse Nonstandard Mathematics and the nonstandard content of effective Reverse Mathematics},
	author = {Sanders, Sam},
	abstract = {The aim of this paper is to highlight a hitherto unknown computational aspect of Nonstandard Analysis pertaining to Reverse Mathematics (RM). In particular, we shall establish RM-equivalences between theorems from Nonstandard Analysis in a fragment of Nelson's internal set theory. We then extract primitive recursive terms from Goedel's system T (not involving Nonstandard Analysis) from the proofs of the aforementioned nonstandard equivalences. The resulting terms turn out to be witnesses for effective1 equivalences in Kohlenbach's higher-order RM. In other words, from an RM-equivalence in Nonstandard Analysis, we can extract the associated effective higher-order RM-equivalence which does not involve Nonstandard Analysis anymore. Finally, we show that certain effective equivalences in turn give rise to the original nonstandard theorems from which they were derived.},
	comment = {},
	date_added = {2015-11-19},
	date_published = {2015-11-01},
	urls = {http://arxiv.org/abs/1511.04679,http://arxiv.org/pdf/1511.04679v1},
	collections = {Attention-grabbing titles,About proof},
	month = {nov},
	url = {http://arxiv.org/abs/1511.04679 http://arxiv.org/pdf/1511.04679v1},
	year = 2015,
	archivePrefix = {arXiv},
	eprint = {1511.04679},
	primaryClass = {math.LO},
	urldate = {2015-11-19}
}