□ 『Reverse Mathematics: Proofs from the Inside Out by John Stillwell』(逆数学：定理から公理を「証明」する)
>> https://press.princeton.edu/titles/11143.html
Hardcover 2018 24.95 20.00 ISBN9780691177175 200 pp. 6 x 9 1/4 5 halftones. 30 line illus.
E-book ISBN9781400889037
読了。
やや解析学よりの視点から、再帰理論、或は計算可能性理論といった
形式的概念、およびメタ数学概念の概観と課題を提示。
定理の"深さ (Depth)"に根源的な意味を問う。
The main purpose is to introduce the base system RCA0 which stands for Recursive Comprehesion Axiom system, and which is still missing the concept of general computable sets to actually prove theorems like for example the Heine-Borel theorem in the stronger ACA0 system.
if a finitely branching tree has infinitely many vertices, then it has an infinite path. Its proof resembles the proof of the Bolzano-Weierstrass or the Heine-Borel theorem that rely on the construction of an infinite sequence of nested intervals.
All these proofs incorporate an enumerable concept that should result in the definition of limit.