Hi, Jim, thanks for your explanation. I will play with these different systems to have a try, I believe this will help me to understand and learn both metamath and reverse math.
Mingli On Mon, Sep 13, 2021 at 9:30 AM Jim Kingdon <[email protected]> wrote: > Most of what I know about reverse mathematics is what I see in a quick > look at the wikipedia article, so I'm not sure the following covers it > especially well, but I'll try: > > 1. You are correct that "This theorem was proved from axioms" can be used > to keep track of which axioms were used in a proof. In the Metamath Proof > Explorer this is most developed for the axiom of choice, the axiom of > regularity, and perhaps a few of the predicate logic axioms. However what > we have done so far is mostly about omitting axioms from ZFC more so than > adding axioms to something like RCA0. > > 2. Although there is a bit of a start at doing things with type theory at > http://us.metamath.org/holuni/mmhol.html it hasn't gotten as much > attention as ZF or IZF. I don't know how fully developed it is, how the > type theory there compares with what reverse mathematics generally uses > (which I gather is usually based on second order arithmetic?), etc. > > 3. There is a decent amount of development of IZF at > http://us.metamath.org/ileuni/mmil.html (up to the construction of the > real numbers and existence of square roots, basically). However, I gather > IZF is pretty strong by the standards of these things. There's a little CZF > there as well but I'm not sure that it weak enough to serve as a base > theory. > Hope this gives you at least some basis for comparing what you are seeing > in Stillwell versus what currently exists in metamath. Of course the > metamath tools could be fed a different set of axioms (as we have done with > the IZF iset.mm as opposed to the ZFC set.mm which has been around > longer), so there is a lot which could be done but which in some cases > hasn't been yet. > > On 9/12/21 11:07 AM, Mingli Yuan wrote: > > 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 > <https://groups.google.com/d/msgid/metamath/CAGDRuAjhQMVs-iQqOzQ5C4FdAokQRw0kscqq39_oMyMCd1LwAQ%40mail.gmail.com?utm_medium=email&utm_source=footer> > . > > -- > 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/ea5dc249-b8fa-9625-7998-5d839a4e83cf%40panix.com > <https://groups.google.com/d/msgid/metamath/ea5dc249-b8fa-9625-7998-5d839a4e83cf%40panix.com?utm_medium=email&utm_source=footer> > . > -- 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/CAGDRuAjf5cua1GycScFi7wJpqR-ioEJXsOpPduqyrtfgtwN-Lw%40mail.gmail.com.
