Thanks Wolf for starting this thead, and thanks Norm and Mario for the
interesting comments.
As for replacing df-cleq by bj-df-cleq (resp. df-clel by bj-df-clel), I am
still in favor of it. Not only does it remove the problem of redundancy of
ax-9 (resp. ax-8), which has concrete implications like the one witnessed
in the recent PR mentioned by Wolf, or because it would impede some
minimizations (since some minimizations currently appear to add dependency
on ax-9 for theorems already using df-cleq, hence are not performed), but
also, and maybe more importantly, the definitions bj-df-cleq and bj-df-clel
are easier to understand, and they make it easier to convince oneself that
they are conservative since the hypothesis and conclusion have identical
forms, and they are totally unbundled. Both definitions simply assert:
"provided this statement is true for individual variables, then it is also
true for class variables", for two specific statements (namely: set
extensionality / class extensionality and set membership / class
membership). I copied both definitions below for convenience of the reader
and for inspection. With these modifications, I'm fine with keeping the
name "definition" and not "axiom", because of the eliminability and
conservativity theorems mentioned in mmset.html#class and proved in Levy's
Basic Set Theory (see also the section starting with ~eliminable1 and its
comments). I also like Wolf's remark: it's not because set.mm already
outperforms textbooks that we should not make additional improvements.
As for the other examples of pseudo-redundancy that Norm describes as
loopholes, I do not agree that they are real loopholes since you only prove
specific instances of the statement, not the statement itself. In
particular, the concrete implications mentioned in the previous paragraph
do not occur.
Side note: the strengthening ( x = y -> ( x e. A -> y e. A ) ) mentioned by
Mario and Wolf is indeed proved as bj-eleq1w from FOL+df-cleq (for
bj-eleq2w, you also need ax-9).
${
$d u v w x A $. $d u v w x B $.
bj-df-cleq.1 $e |- ( u = v <-> A. w ( w e. u <-> w e. v ) ) $.
bj-df-cleq $p |- ( A = B <-> A. x ( x e. A <-> x e. B ) ) $=
( dfcleq ) AEFH $.
$}
${
$d u v w x A $. $d u v w x B $.
bj-df-clel.1 $e |- ( u e. v <-> E. w ( w = u /\ w e. v ) ) $.
bj-df-clel $p |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $=
( df-clel ) AEFH $.
$}
Benoît
On Wednesday, October 27, 2021 at 5:40:04 PM UTC+2 Norman Megill wrote:
> I discuss the issue of whether to call df-clab,cleq,clel axioms at the end
> of the http://us.metamath.org/mpeuni/mmset.html#class section. Most
> authors call them definitions, and my feeling is that calling them axioms
> would be somewhat misleading since they can (in the presence of ax-ext)
> always be eliminated back to equivalent statements in the primitive
> language.
>
> While I'm not sure what the correct terminology is, class notation as a
> "conservative extension" is not the same notion as calling NBG a
> "conservative extension" of ZFC: in the former case, any class expression
> can be converted back and forth to an equivalent expression in the native
> language, whereas in the latter case, there are statements such as global
> choice that cannot be expressed in the ZFC language and have no equivalent
> in ZFC.
>
> 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?
>
> Most importantly, though, I don't want to give the reader (who typically
> is not a set theorist or even a mathematician) the impression that the
> axioms of set theory aren't sufficient in principle for essentially all of
> math. I think that calling df-cleq an "axiom" simply due to limitations of
> Metamath is not necessarily helpful to the average person just wanting an
> overall understanding of the foundations of math.
>
> You have a somewhat different goal wrt formal verification, and for your
> purposes calling them ax-clab,cleq,clel (with a simple global label
> replacement in set.mm) may very well be preferred. Part of my goal has
> been to break down mathematics into the smallest possible steps that an
> average person can in principle verify for themselves (whether or not they
> are able to grasp the big picture), while also trying to communicate in
> more general terms the foundations of set theory and thus mathematics in
> mmset.html, in a way that doesn't confuse people with "if ZFC is
> sufficient, why do we need axioms beyond ZFC?" I think our goals have
> worked together synergistically.
>
> Aside from ax-9, some issues with definitions are not unique to df-cleq.
>
> 1. Let us temporarily add to our propositional calculus system the
> (redundant) axioms bitri and bicomi. From those two axioms, we cannot
> prove biid. Yet from those two axioms plus df-or, we can prove an instance
> of biid. So df-or implies something stronger than those two axioms. Since
> in our system we use ax-1,2,3 to prove biid, does this mean we should
> include ax-1,2,3 as additional hypotheses for df-or?
>
> 2. The cbvalv-type loophole applies to any definition with dummy
> variables, not just df-cleq. Fortunately the only two definitions with
> dummy variables before set theory are df-tru and df-eu. And fortunately
> df-eu comes after cbvalv, so this loophole doesn't add strength to the
> language in that case (although in theory it could disturb the "This
> theorem was proved from axioms" list). As for df-tru, well, it's had a
> long history of being problematic, and a purist might want to move it below
> cbvalv, but that would be ugly.
>
> Norm
>
> On Wednesday, October 27, 2021 at 8:33:17 AM UTC-4 di.... wrote:
>
>> Personally, I think the easiest way to address the issues is to make
>> df-cleq, df-clab, df-clel axioms instead of "definitions". They are not
>> definitions according to the definition checker algorithm, they are not
>> conservative as observed in this thread, and they significantly complicate
>> the metatheoretic analysis of the axiom system. Even if we want to think
>> that "class" is a conservative extension of ZFC, that is only when you
>> introduce the whole set of axioms at once, and even then we must assume the
>> full set of FOL axioms (like ax-9) to start with. Metamath does not have an
>> adequate mechanism for introducing new conservative sorts, and I think we
>> should just own up to this and admit these as axioms.
>>
>> On Wed, Oct 27, 2021 at 8:04 AM Norman Megill wrote:
>>
>>> On Tuesday, October 26, 2021 at 6:07:19 PM UTC-4 ookami wrote:
>>>
>>>> Norman Megill wrote Tuesday, 26. Oktober 2021 at 21:46:35 UTC+2:
>>>>
>>>>> Which comment of Benoît you are referring to?
>>>>>
>>>>> In PR #2267 he described the phenomenon of the vanishing ax-9 as an
>>>> artifact of df-cleq and further hinted to his bj-ax9 theorem.
>>>>
>>>
>>> ax-9 is not the only problem. Note that with bitri+bicomi+df-cleq we
>>> can prove an instance of cbvalv, which requires ax-4-7,10-13 for its
>>> proof. If a future set theory proof needed that exact instance of cbvalv,
>>> we could "cheat" and use df-cleq instead to bypass all those axioms.
>>>
>>> I think Benoit's result that df-cleq implies ax-9 is nice and should be
>>> documented in the comment for df-cleq, but I think it would be weird and
>>> confusing to add ax-9 as a hypothesis. And if we do that, we should also
>>> add ax-4-7,10-13 to be consistent.
>>>
>>> We have ax-ext as a hypothesis of df-cleq because which ZFC axioms are
>>> needed for a result is considered important in the development of set
>>> theory. But we ordinarily don't care about which FOL= (FOL+equality)
>>> axioms are used after we get into set theory.
>>>
>>> In the development of FOL= itself, it is useful to derive results using
>>> the fewest axioms possible. It can help towards proving independence of
>>> the axioms and possibly finding weaker or alternate versions of axioms in
>>> the future. I appreciate the work you have done towards that.
>>>
>>> Once we get to interesting results in set theory, all of the FOL= axioms
>>> will pretty much be used anyway. Effort spent to eliminate the use of this
>>> or that FOL= axiom in the set theory development doesn't seem productive to
>>> me, and it may even be confusing to the reader to see longer proofs that
>>> may result just to avoid using a certain FOL= axiom in a set theory theorem.
>>>
>>>
>>>>
>>>> If, as you write, ax-9 is not important any more once you arrive at
>>>> df-cleq, you may as well include it to the axiom list unconditionally.
>>>>
>>>> From my point of view the following aspects were important to trigger
>>>> my initial post:
>>>>
>>>> 1. Does the axiom list appear to be trustworthy? And does it
>>>> follow a consistent pattern?
>>>>
>>>> The "This theorem was proved from axioms" axiom list on the web pages
>>> is generated as a convenience for the reader. As noted, df-cleq can
>>> distort this, so in principle the "This theorem depends on definitions"
>>> list must also be considered. I suppose that once into set theory, I could
>>> replace the FOL= axiom list with just a fixed phrase meaning "you might as
>>> well assume that all FOL= axioms are used", but that would require messy
>>> metamath.exe code customized to set.mm to detect the set theory
>>> section, and I really don't want to do that.
>>>
>>> A partial fix (without changing df-cleq itself) is to insert an
>>> artificial application of ax-9 in the proof of dfcleq (in a way that
>>> doesn't 'minimize' out, or make its proof modification discouraged) for the
>>> cosmetic reason of making the axiom list include ax-9 when dfcleq is used,
>>> since ax-9 seems to be the main concern here. Could you do that? That
>>> should address most cases that we see in practice.
>>>
>>>
>>>>
>>>> 1.
>>>> 2. While adding complexity to df-cleq may puzzle readers, vanishing
>>>> axioms after a proof change is not better. And we have a concrete
>>>> incident
>>>> here.
>>>> 3. df-cleq, and even more so df-clel, seem to be no ordinary
>>>> definition anyway, as the right hand side does not always explain the
>>>> definiendum in simpler terms, for example in case set variables are
>>>> involved. It once took me quite some time to get over their recursive
>>>> nature, and their implicit consequences. One is that you can restate 2
>>>> axioms directly, but only one is taken care of.
>>>>
>>>> Yes, these are not ordinary definitions. They are discussed in some
>>> detail at http://us.metamath.org/mpeuni/mmset.html#class.
>>>
>>> I am at a loss how text books handle these issues; I never read one on
>>>> logic.
>>>>
>>>
>>> Textbooks don't handle these issues. Which axioms of FOL= are needed
>>> for a set theory proof aren't considered important or even discussed.
>>>
>>> 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/234db141-41e9-4ec7-8a81-55cfebf7b354n%40googlegroups.com.
