On 10/27/21 9:55 PM, Mario Carneiro wrote:
> An example of a ZFC+classes expression containing class variables that
> has no equivalent without class variables is "x e. A". Any expression
> equivalent to this must contain the variable "A".
"A" can be introduced and eliminated by substitution into a theorem scheme.
We assume x e. A is part of some theorem scheme. The (meta)variable A can
be substituted with a class builder of the form { y | ph }, where ph is a
wff (meta)variable.
Going from class variable to wff variable:
x e. A (we assume this is part of a theorem scheme)
x e. { y | ph } substitute "{ y | ph }" for "A" in the scheme
[ x / y ] ph by df-clab
To go back to the original class variable:
[ x / y ] ph (we assume this is part of a theorem scheme)
[ x / y ] y e. A substitute "y e. A" for "ph" in the scheme
x e. A using sbie and eleq1
So the scheme x e. A is equivalent i.e. represents the same set of object
language wffs as the scheme [ x / y ] ph.
ZFC+classes is exactly equivalent to ZFC in terms of the object-language
theorems it can prove. This is very different from NGB as a "conservative
extension of ZFC", which has statements stronger than what ZFC can prove
such as global choice (primarily because the class variables in ZFC+classes
cannot be existentially quantified).
On 10/28/21 10:11 AM, Thierry Arnoux wrote:
> A solution is mentioned in the comment for df-cleq, shall it be
> reconsidered?
>
> / We could avoid this complication by introducing a new symbol,
> say =_2,//
> // in place of ` = ` . This would also have the advantage of making//
> // elimination of the definition straightforward, so that we could//
> // eliminate Extensionality as a hypothesis. We would then also
> have the//
> // advantage of being able to identify in various proofs exactly
> where//
> // Extensionality truly comes into play rather than just being an
> artifact//
> // of a definition. One of our theorems would then be ` x ` =_2//
> // ` y <-> x = y ` by invoking Extensionality.//
...
A discussion about eliminating overloading of = and e. in
df-clab,cleq,clel, and why it isn't that simple, is here (from 2016):
https://groups.google.com/g/metamath/c/IwlpCJVPSLY/m/f8H9lze_BQAJ
I believe Mario correctly concludes (contrary to my initial suggestion)
that overloading of "e." can't be removed with this method. Since the 3
definitions work together, it doesn't make sense to half-fix it with the
clumsiness and longer proofs that will result from =_2 (always having to
convert back and forth to make use of FOL theorems).
I have removed the comment you mention from df-cleq since it is misleading
in this way.
On 10/28/21 12:09 PM, Cris Perdue wrote:
...
> Norm replied -
>
> The standard is that a definition must be conservative and eliminable.
>
> --------------------------------------
>
> It seems to me that Norm is mistaken in this, and that the usual
> terminology is that "definitions" have certain prescribed forms.
>
> The wikipedia article on extension by definitions
> (https://en.wikipedia.org/wiki/Extension_by_definitions
> <https://en.wikipedia.org/wiki/Extension_by_definitions>) refers to
>
> * S.C. Kleene (1952), /Introduction to Metamathematics/, D. Van Nostrand>
* E. Mendelson (1997). /Introduction to Mathematical Logic/ (4th ed.),
> Chapman & Hall.
> * J.R. Shoenfield (1967). /Mathematical Logic/, Addison-Wesley
> Publishing Company (reprinted in 2001 by AK Peters)
>
>
> I have copies of Kleene and Shoenfield, and they describe "definitions"
> as having specific defining forms, which I take to be much like those
> that Metamath can automatically check.>
While I haven't studied them in detail, except for his "explicit
definitions" they seem to involve somewhat complex proofs that mmj2 might
not be able to automatically check.
> In Kleene, section 74 (page 405 to 420) is titled "Eliminability of
> descriptive definitions", and it has subsections on "Eliminability of
> explicit definitions" and "Eliminability of descriptive definitions".
> He also discusses eliminability of some other constructs including "a
> defined sort of variables" (p. 420).
As far as I can tell, he isn't proposing to rename any of these various
forms of definition as "axioms".
>
> In Shoenfield, section 4.6 starting p. 57 is titled "Extensions by
> definitions", covering definitions of new predicate symbols and
> definitions of new function symbols. He states (p. 60) that, "We say
> that T' is an /extension by definitions/ of T if T' is obtained from T
> by a finite number of extensions of the two types which we have
described."
I don't have a copy of Shoenfield, but from what you quote he is still
calling them "definitions" rather than new axioms.
As for Mendelson, he uses NBG which has class variables built in, so it
doesn't really apply to set.mm.
Takeuti/Zaring has the same class theory as we do, and their versions of
df-clab,cleq,clel are all called "definitions".
The only place I could find class theory definitions called "axioms" is in
Levy. But he calls them "extralogical axioms", whatever that means,
compared to what he calls the "logical axioms" of ZFC. Perhaps he doesn't
consider them "real" axioms?
On 10/28/21 12:39 PM, Scott Fenton wrote:
> So, to me, the whole point of doing Metamath is to lay out assumptions
> as explicitly as possible. We work in logic that requires us to state
> every single assumption we make along the way. This is one of the things
> I love about Metamath as compared to other theorem proving systems. We
> seem to be embedding an assumption in making class and set equality the
> same thing. This overloading leads to subtle assumptions that are not
> always obvious. We can see that by the proof of ax-9 from df-cleq. This
> defeats the whole point of Metamath to me. If we no longer overload
> equality, say by making set equality be "==" insead of "=", we can
> eliminate this ambiguity. This brings us back closer to the foundations
> of Metamath, so I propose we do it.
>
I modified the proof of dfcleq to use axext3 instead of ax-ext so that it
now uses ax-9. This will temporarily address the complaint that ax-9
doesn't always show up in the "This theorem was proved from axioms" list on
the set theory web pages, until we make a final decision about how to
handle it.
Personally I think that, while not desirable, it is OK in principle for the
soundness of a definition to depend on axioms that were introduced before
it. Certainly the literature does that all over the place (e.g. in
recursive definitions, which are not called new axioms even though their
rigorous justification is significantly more complex than for class theory).
Of course, metamath.exe cannot identify such dependencies, making the FOL
axiom usage list sometimes incomplete. I have never felt that was more than
a minor cosmetic problem since once we're into set theory, we don't
normally care about which FOL axioms were used; all we care about is which
ZFC axioms were used.
Another alternative is to have metamath.exe suppress the FOL axioms once
ax-ext is introduced, and change the name of the list to "This theorem was
proved from ZFC axioms".
Norm
--
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/3dfffa04-d6cc-49d8-b9bf-4a1b8c5beda3n%40googlegroups.com.
