Hi, folks, I am a newbie of metamath, and recently I am reading John Stillwell's book - Reverse Mathematics, the book uses a very elegant style to introduce the topic via a minimal way.
I noticed the theorem explorer has a section "This theorem was proved from axioms", so I am wondering whether it is possible to explore the theorems in the book via metamath, and also can get the clear hierarchy of RCA0, WKL0, ACA0, etc. In my understanding, if we have the dependent chain and the net of theorems, it is natural to study the structure of them. While I searched all the emails of this group since 2016, and found nothing. Why? Mingli -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAjhQMVs-iQqOzQ5C4FdAokQRw0kscqq39_oMyMCd1LwAQ%40mail.gmail.com.
