On Wed, Oct 27, 2021 at 7:22 PM Norman Megill <[email protected]> wrote:
> In fact, ZFC + classes is a conservative extension in exactly the same way
>> that NBG is,
>>
>
> There is a fundamental difference.
>
> NBG has global choice, which has no ZFC equivalent. From the wikip page
> on NBG, "the axiom of global choice ... is stronger than ZFC's axiom of
> choice".
>
> On the other hand, any ZFC+classes expression containing class variables
> can be converted to an equivalent expression with wff variables, and
> vice-versa. They are just two different notations for the same thing. See
> Takeuti/Zaring Ch. 4 or Levy Appendix X or Quine pp. 15-21. Class
> variables can be considered wff (meta)variables in disguise. See also the
> comments in ~abeq2.
>
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". (More on this below.)
A more substantive observation about ZFC+classes is that it provides a
proof speedup, just like ACA_0 over PA (ACA_0 is a conservative extension
of PA that adds second order variables). Or at least it would, in a
traditional axiomatization; in metamath the advantage is largely nullified
because you can prove schemes over wff variables, which normal ZFC can't
do. I suspect there is still some speedup in the metamath setting because
being able to hide the bound variables involved in a class abstraction
means you don't have to substitute and alpha-rename them in deeply nested
situations.
especially if you pay attention to metalogical completeness.
>>
>
> What does this have to do with our metalogical (scheme) completeness - or
> do you mean something else?
>
I am talking about scheme completeness. This is very important to
understand because it is the crux of the argument that the textbook proofs
fall short of a true proof of conservativity in the metamath setting.
As far as I can tell, the standard argument that classes are a definitional
>> extension only applies if we think that the only inhabitants of "class" are
>> class abstractions, but in metamath there are always variables living in
>> every sort, and you can't prove properties about generic variables even if
>> the property holds for all class abstractions.
>>
>
> Sorry, I don't understand what this sentence means. :) What is an
> inhabitant, "living in every sort", generic variable, property? There are
> no "generic" variables (as I understand that word) in set.mm; there are
> only wff, setvar, and class variables.
>
An inhabitant just means an object of that type. Here I am referring to the
terms that can be considered as valid things of type "class": in the
traditional setting, every class is either a class abstraction, i.e.
literally {x | ph} for some ph, or is defined to be something that
ultimately boils down to a class abstraction (and when traditional logics
talk about definition they usually mean an abbreviation at the meta-level,
so it is still syntactically a class abstraction). In metamath there are
other things of type "class", that I am calling "generic variables", by
which I mean "A", "B" and so on. These are not class abstractions, they are
variables; if you ask what syntax makes them up "cab" is nowhere to be
found.
> A simple example of this is axiom ax-9c, which is true for class
> abstractions
>
>> because of df-clab (i.e. x = y -> (x e. { z | ph } -> y e. { z | ph }) is
>> true by properties of substitution) but cannot be proven for arbitrary
>> classes.
>>
>
> This is an instance of eleq1+biimpd, which holds for arbitrary classes.
>
eleq1 is a consequence of df-cleq though, which as we have already
established makes ax-9c derivable. If you drop df-cleq and df-clel, keeping
only df-clab, the mentioned theorem is true for class abstractions but not
for arbitrary classes (even though x = y -> (x e. A -> y e. A) involves
neither wceq or wcel, at least if we ignore the notation overloading and
read it as "weq x y -> (wvel x A -> wvel y A)").
> Traditional textbooks don't cover this, because of course metalogical
>> completeness isn't a thing. But I think it is impossible for metamath to
>>
> introduce a new sort without letting these extra variable terms sneak in,
>> so metalogical completeness is always relevant to us. I believe that
>> conservativity in the traditional sense still applies to the set.mm
>> formulation of "class" over the set-only part of , but nothing stronger
>> than that.
>>
>
> I don't understand what you mean. What is an example of extra variable
> terms that sneak in?
>
Perhaps this is not the most intuitive picture for you, but the way I
internalize metalogical completeness as a concept is that in the model of
metamath every sort contains additional things beyond the regular things.
The space "wff" contains more than just object level formulas, it also
contains "variables" which are uninterpreted / generic predicates. It is a
consequence of this that just because a fact is true (say by induction on
formulas) for every object level formula, it may not be true at these
"generic points" (points because we are thinking of "wff" as a space of
things, with the points being formulas of the object language but also
these uninterpreted variable things), which is another way of saying that a
logically complete schema may not be metalogically complete.
Applied to the sort "class", we get that the regular points of the space
are the class abstractions (those are the things we put there
deliberately), and the generic points are the variables "A", "B" (those
come along for the ride because of how metamath works). And now to the
point: the theorem in the textbooks that reduces every theorem in the
object language using classes to an equivalent theorem without classes is
performed by induction on formulas and terms, and so it does not apply to
the generic points. For any metamath theorem about classes, you can always
make a special case of the theorem by substituting class abstractions for
everything and then run the elimination proof, but a plain variable "A" is
not eliminable: you can replace it with { x | x e. A } but you are no
closer to eliminating A by doing so.
> I don't see the fact that our definitional check algorithm can't check
>>> them as sufficient justification in itself to call them axioms. If we had
>>> adopted the usual textbook convention of using multipart recursive
>>> definitions for df-oadd etc. instead of our direct definitions with `rec`,
>>> would you want to call those axioms?
>>>
>>
>> What it amounts to is that all our tools are saying it's not a
>> definition, and the only reason it is considered a definition is because we
>> are explicitly overriding the tool and declaring them definitions by fiat.
>> Furthermore, because of the notational overloading situation, these
>> definitions are
>>
>
> There is no new mathematics that results from the class theory
> definitions, and as a practical matter I have chosen to trust the multiple
> proofs of conservation and eliminability in the literature. In principle
> they could be proved formally. Class theory is simply a different notation
> for the same thing that is often more practical to work with. Since no new
> mathematics results from the class theory definitions, it's hard for me to
> justify calling them axioms.
>
> I understand that these literature proofs may not qualify as a "trusted
> base" from your point of view since they haven't been verified formally.
> In which case it would make sense for you to rename/treat them as ax-* in
> your copy of set.mm.
>
The new mathematics is kind of fringe stuff, so I can understand why you
might think this, but I think this conversation started exactly because
Wolf has been exploring the mathematics of subsystems of set.mm's axiom
system where you can't take equivalence to the textbooks for granted, and
it is in this light that the conservativity proof starts to break down.
Regarding my position on axioms, the issue is not that they haven't been
verified formally. I think I am probably more willing to accept new axioms
than you because I see theorems vs axioms as the difference between
"correct by internal reasoning" and "correct by external reasoning". In MM0
of course I am planning to verify the metalogic in addition to proving
theorems in the logic, so making a theorem into an axiom is not cheating,
it is merely moving the work from one part to another. Some things are best
verified internally, these are the theorems; and some things are easier to
verify by a metatheoretic proof, and these are the axioms. From such a
description it should be clear why I consider df-cleq et al. axioms, and it
has nothing to do with believing the conservativity result to be false or
unverified.
> For a careful reader, it is not clear to me what the relative
>> probabilities of the "type I and type II errors" here are. As you say, if
>> we mark them as
>>
>
> What are type i and type II errors?
>
Not a perfect match for the situation, but see
https://en.wikipedia.org/wiki/Type_I_and_type_II_errors . I mean that we
have roughly two choices, and both choices have some probability of leading
readers astray, in different directions.
Mario
--
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/CAFXXJSvy5OSCsHdRpnHA2eKYS34XnBFVZ2%2BCfyv%3DAOnjuUFZ7Q%40mail.gmail.com.
