On Wed, Oct 27, 2021 at 7:22 PM Norman Megill 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
(The us2 server was down most of the afternoon due to a power failure
caused by a storm. It should be back up now.)
On Wednesday, October 27, 2021 at 1:18:17 PM UTC-4 di wrote:
> On Wed, Oct 27, 2021 at 11:40 AM Norman Megill wrote:
>
>> I discuss the issue of whether to call
On Wed, Oct 27, 2021 at 11:40 AM 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
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
Now that my daily work is (almost) finished, I have time again to address
this thread. A few remarks off the cuff:
1. Some facts are provable from different sets of axioms. I know this and
have one example (wl-spae) developed myself. This theorem is an instance
of sp, thus a consequence
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)
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
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
Well, like I said we first need to know that x e. A acts like a regular
predicate, which in particular implies your theorem about the equivalence
of the distinct and bundled cases. I believe that the strengthened ax-9 I
mentioned (i.e. x = y -> (x e. A -> y e. A)) also implies this fact. set.mm
is
Extremely quick answer, because I am busy at work, and have no time to
think anything over: df-cleq DOES say something about x e. A although it is
assumed to be primitive: If you cannot find an y with y e. A, y and A
distinct, you cannot find an x in the bundled case either (x being free in
On Wed, Oct 27, 2021 at 5:26 AM 'ookami' via Metamath <
metamath@googlegroups.com> wrote:
> I am not sure whether the complexity is a problem of operator overloading
> only. Let me explain why:
>
> At the moment of df-cleq the term x e. A is still undefined, and can mean
> anything.
The term x
I am not sure whether the complexity is a problem of operator overloading
only. Let me explain why:
At the moment of df-cleq the term x e. A is still undefined, and can mean
anything. It is known to be well-formed (by wcel), though, so our typical
logical manipulations apply. It follows from
12 matches
Mail list logo
