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]
<mailto:[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.
