BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The unreasonable effectiveness of Nonstandard Analysis - Sanders\,
  S (Ludwig-Maximilians-Universitt Mnchen)
DTSTART:20151214T150000Z
DTEND:20151214T153000Z
UID:TALK62893@talks.cam.ac.uk
CONTACT:42080
DESCRIPTION:The aim of my talk is to highlight a hitherto unknown computat
 ional aspect of Nonstandard Analysis. In particular\, we provide an algori
 thm which takes as input the proof of a mathematical theorem from pure Non
 standard Analysis\, i.e. formulated solely with the nonstandard definition
 s (of continuity\, integration\, dif- ferentiability\, convergence\, compa
 ctness\, et cetera)\, and outputs a proof of the as- sociated effective ve
 rsion of the theorem. Intuitively speaking\, the effective version of a ma
 thematical theorem is obtained by replacing all its existential quantifier
 s by functionals computing (in a specific technical sense) the objects cla
 imed to exist. Our algorithm often produces theorems of Bishops Constructi
 ve Analysis ([2]). \n The framework for our algorithm is Nelsons syntactic
  approach to Nonstandard Analysis\, called internal set theory ([4])\, and
  its fragments based on Goedels T as introduced in [1]. Finally\, we estab
 lish that a theorem of Nonstandard Analysis has the same computational con
 tent as its highly constructive Herbrandisation. Thus\, we establish an al
 gorithmic two-way street between so-called hard and soft analysis\, i.e. b
 etween the worlds of numerical and qualitative results.\n \nReferences: \n
  [1] Benno van den Berg\, Eyvind Briseid\, and Pavol Safarik\, A functiona
 l interpretation for non- standard arithmetic\, Ann. Pure Appl. Logic 163 
 (2012)\, no. 12\, 19621994. \n \n[2] Errett Bishop and Douglas S. Bridges\
 , Constructive analysis\, Grundlehren der Mathematis- chen Wissenschaften\
 , vol. 279\, Springer-Verlag\, Berlin\, 1985. \n \n[3] Fernando Ferreira a
 nd Jaime Gaspar\, Nonstandardness and the bounded functional interpre- tat
 ion\, Ann. Pure Appl. Logic 166 (2015)\, no. 6\, 701712. \n \n[4] Edward N
 elson\, Internal set theory: a new approach to nonstandard analysis\, Bull
 . Amer. Math. Soc. 83 (1977)\, no. 6\, 11651198. \n \n[5] Stephen G. Simps
 on\, Subsystems of second order arithmetic\, 2nd ed.\, Perspectives in Log
 ic\, CUP\, 2009. \n
LOCATION:Seminar Room 1\, Newton Institute
END:VEVENT
END:VCALENDAR