BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Sam Sanders (RUB Bochum)
DTSTART:20241017T180000Z
DTEND:20241017T190000Z
DTSTAMP:20260423T035931Z
UID:OLS/164
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/OLS/164/">So
 me results in reverse mathematics inspired by proof mining</a>\nby Sam San
 ders (RUB Bochum) as part of Online logic seminar\n\n\nAbstract\nThe study
  of (compact) metric spaces in second-order Reverse Mathematics (RM hereaf
 ter) is fundamentally based on separability conditions\, while the latter 
 are generally avoided in proof mining to enable the extraction of good com
 putational data. Inspired by this observation\, we study basic properties 
 of ‘unrepresented’ compact metric spaces in Kohlenbach’s higher-orde
 r RM\, i.e. we do not assume separability conditions. Our results are four
 -fold as follows\, each building on the next.\n\nMost definitions of compa
 ctness yield third-order theorems not provable from second-order comprehen
 sion axioms. Only one very specific choice of compactness definitions yiel
 ds equivalences involving the so-called Big Five of second-order RM.\n\nMa
 ny basic properties of compact metric spaces inhabit the range of hyperari
 thmetical analysis. Until recently\, few natural examples of the latter we
 re known.\n\nSome basic properties of compact metric spaces\, like the int
 ermediate value theorem\, are equivalent to countable choice as studied in
  higher-order RM\, namely QF-AC0\,1.\n\nSome basic properties of compact m
 etric spaces\, like a continuous function has a supremum and a countable s
 et has measure zero\, imply strong axioms including Feferman’s projectio
 n principle\, full second-order arithmetic\, and Kleene’s quantifier (
 ∃3).\n\nIn conclusion\, the removal of separability conditions from comp
 act metric spaces results in rather interesting phenomena.\n
LOCATION:https://researchseminars.org/talk/OLS/164/
END:VEVENT
END:VCALENDAR
