Metamath and Reverse math

[Mingli Yuan]

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

[Jim Kingdon]

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.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAGDRuAjhQMVs-iQqOzQ5C4FdAokQRw0kscqq39_oMyMCd1LwAQ%40mail.gmail.com.

[Mingli Yuan]

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 

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/ea5dc249-b8fa-9625-7998-5d839a4e83cf%40panix.com.