Question on Theorem pm2.61ne

[bil...@gmail.com]

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.

[Mario Carneiro]

(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.

--
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/4765307e-2a18-40aa-a754-7591522e4305n%40googlegroups.com.

[bil...@gmail.com]

So we can say that metamath is working in "new foundations" rather than "zfc"? In particular, this would explain why "classes" are being used.

[Mario Carneiro]

No, set.mm is working in ZFC, or rather a conservative extension thereof. Classes are ZFC classes, they cannot be quantified but they represent maybe-proper classes in the usual way. They are not "in the universe" in the sense that "A. x ph" ranges over all sets, and proper classes are not considered, but they are expressible in the language, essentially as syntactic sugar for predicates with one designated free variable.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/dcbccba7-8a0d-40ad-86cf-829ce4c7a333n%40googlegroups.com.