So we can say that metamath is working in "new foundations" rather than "zfc"? In particular, this would explain why "classes" are being used.
On Friday, September 29, 2023 at 10:51:44 PM UTC-5 [email protected] wrote: > (copying my answer, something odd seems to have happened to the first post) > > The first assumption ( A = B -> ( ps <-> ch ) ) is the idiomatic way to > say that ch is the result of substituting A for B in ps, and there are many > theorems that produce results of this form. The theorem is still true when > you only have a one-directional implication (in fact the first step of the > proof is to weaken it to one), but users of the theorem will normally have > the biconditional on hand so it is more convenient to write it that way to > make the theorems more interoperable. > > This theorem is true in any classical logic, so it holds in both NF and > ZFC. (It does not hold in iset.mm, which uses intuitionistic logic, > because there is a case distinction on A = B in this theorem.) New > Foundations is an axiomatic system with a lot in common with ZFC, and basic > theorems like this will be true in both. > > On Fri, Sep 29, 2023 at 11:46 PM [email protected] <[email protected]> > wrote: > >> Theorem pm2.61ne is the following: >> >> Hypotheses: >> pm2.61ne.1 |- ( A = B -> ( ps <-> ch ) ) >> pm2.61ne.2 |- ( ( ph and A =/= B ) -> ps ) >> pm2.61ne/3 |- ( ph -> ch ) >> >> Assertion: >> pm2.61ne |- ( ph -> ps ) >> >> Question 1. Why isn't the first hypothesis given in the weaker condition: >> >> pm2.61ne.1weaker |- ( A = B -> ( ch -> ps ) ) >> >> Question 2. How does this "new foundations" fit in with metamath? It >> seems like "new foundations" is being mixed together with "zfc foundation". >> For example, Theorem msqge0 that asserts A in R -> 0 <= A * A uses pm2.61ne >> in its proof. >> >> -- >> 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/4765307e-2a18-40aa-a754-7591522e4305n%40googlegroups.com >> >> <https://groups.google.com/d/msgid/metamath/4765307e-2a18-40aa-a754-7591522e4305n%40googlegroups.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/dcbccba7-8a0d-40ad-86cf-829ce4c7a333n%40googlegroups.com.
