TL;DR: there are various definitions of the notion ‘countable set of reals’ and only one seems to lead to nice equivalences in Reverse Mathematics. In particular, injections and bijections to the naturals à la Cantor are not very suitable. A slightly more general notion leads to many equivalences involving regulated and bounded variation functions, as…
On representations and their brute-forced connections.
TL;DR: classical Reverse Mathematics makes heavy use of so-called codes or representations. We observe a major problem with this coding practise, namely the connection between open sets and continuous functions, which is ‘brute-forced’ by the coding of these objects. The long version: Reverse Mathematics needs no introduction on this blog and neither does , the…
The Biggest Five of Reverse Mathematics
TL;DR: Dag Normann and I have obtained LOTS of equivalences between the second-order Big Five of Reverse Mathematics and third-order theorems from mainstream analysis about (possibly) discontinuous functions, working in Kohlenbach’s higher-order Reverse Mathematics. We also show that slight generalisations or variations of the aforementioned third-order theorems fall FAR outside of the Big Five. Our…
Notation for focused proof systems
Standardized notation can be helpful, especially after a topic has matured. For example, Gentzen used as an infix symbol to build sequents from lists of formulas. While one also sees used, it seems that in recent years, has become the standard, especially when proof theory is applied to type theory (where is invariably used) and…
