>
> Another more thing: it may be more correct to use the universal closures
>> of the $e hypotheses above (as I did in the current bj-df-clel and
>> bj-df-cleq). This does not change much, since one can go back and forth
>> between them by ax-gen/sp, but sentences (closed formulas) are
On 11/29/21 8:15 PM, Norman Megill wrote:
I'm not saying you are wrong, only that I don't understand the
reasoning or advantage and need to be educated. :) I know that many
books show ZFC axioms and even FOL axiomatizations with universal
closures, and I've never understood why.
I don't
On Monday, November 29, 2021 at 6:11:32 PM UTC-5 Benoit wrote:
> I agree that the FOL= part should remain well-separated from the rest.
> And if one wants to keep proximity with textbooks, then ax-8, ax-9, ax-ext
> should remain untouched as well (actually ax-ext should be the universal
>
I agree that the FOL= part should remain well-separated from the rest. And
if one wants to keep proximity with textbooks, then ax-8, ax-9, ax-ext
should remain untouched as well (actually ax-ext should be the universal
closure of what it currently is). This would give:
ax-mp, ax-gen,
I would be happy to see this idea explored in a mathbox. Even if we don't
import it and change our "official" FOL= axiom system on the MPE home page
(which is the result of a lot of fine tuning over many years and admittedly
somewhat biased by my personal preferences), it can still exist as an
I wonder whether one can derive df-cleq and df-clel from more class
centered axioms in a separate section. In the manner complex numbers are
implemented using dedicated definitions like Kuratowski style pairs. And
then introduce the results as axioms, abstracting from the details of
On Saturday, November 27, 2021 at 11:21:49 AM UTC-5 Benoit wrote:
> Here is a complement to Mario's, Thierry's, and Wolf's proposals, as Wolf
> is beginning to formalize his in his mathbox.
>
> If you do not want to overload the membership predicate, then the most
> sensible thing to do in my
Here is a complement to Mario's, Thierry's, and Wolf's proposals, as Wolf
is beginning to formalize his in his mathbox.
If you do not want to overload the membership predicate, then the most
sensible thing to do in my opinion is to simply remove ax-8 and ax-9. By
bj-ax8 and bj-ax9-2, they are
Thank you very much, Mario and Benoît, I will update the repository.
On 02/11/2021 00:01, Mario Carneiro wrote:
Correction: the first line of the abidc proof should be
||- ( x =s y -> ( y e.c A <-> x e.c A ) )|
with a set equality on the left (since class
equality
Correction: the first line of the abidc proof should be
|- ( x =s y -> ( y e.c A <-> x e.c A ) )
with a set equality on the left (since class equality is not yet introduced
yet). We also want ax-8c to reference only primitive term constructors, so
it should also use =s .
On Mon, Nov 1, 2021 at
Sorry, our emails crossed with Mario, so when I was mentionning the proof
above (and the typo), I meant the previous one!
On Monday, November 1, 2021 at 4:56:11 PM UTC+1 Benoit wrote:
> On Monday, November 1, 2021 at 4:34:10 PM UTC+1 Thierry Arnoux wrote:
>
>> In order to make that work, I had
On Monday, November 1, 2021 at 4:34:10 PM UTC+1 Thierry Arnoux wrote:
> In order to make that work, I had to introduce two new axioms. I wonder
> if anyone can eliminate any of them, or propose a cleverer approach.
Note that your ax-abidc is basically bj-eleq1w or Mario's ax-8c above (he
Regarding the new axioms:
ax-abidc should be derivable from df-cleq (it should not be expressible
prior to this anyway, since A = B as a wff is not introduced until then).
Specifically:
|- ( x = y -> ( y e.c A <-> x e.c A ) )
|- ( y e.c A <-> [ y / x ] x e.c A )
|- ( y e.c A <-> y e.c { x | x
I was curious about the solution where we do not overload equality `=`
and membership `e.`, but instead have different versions of those
predicates for sets.
For those interested, I've published the resulting experiment here:
https://github.com/tirix/set-noov.mm
One can examine the changes done
On Fri, Oct 29, 2021 at 2:30 PM Benoit wrote:
> Mario: why, when you encounter a dummy class variable in the original
> proof, don't you simply use a dummy setvar variable in place of it ?
>
That works too. Any expression that doesn't use class variables will work
there.
--
You received this
Also, I've said this already in other words, but to put it in the context
of the conservativity proof just given: ax-9c is derivable from the set.mm
class axioms as they currently exist (obviously, since it's a special case
of eleq1), but without ax-9c, we can't remove the class axioms one at a
> I've referenced it a few times in this conversation as a hypothetical
> axiom extending ax-9 to classes: x = y -> (x e. A -> y e. A).
>
This looks more like "ax-8c" , aka
http://us.metamath.org/mpeuni/bj-eleq1w.html
Mario: why, when you encounter a dummy class variable in the original
On Fri, Oct 29, 2021 at 2:06 PM Norman Megill wrote:
> What is ax-9c? It isn't an axiom in set.mm.
I've referenced it a few times in this conversation as a hypothetical axiom
extending ax-9 to classes: x = y -> (x e. A -> y e. A).
--
You received this message because you are subscribed to
The recent commits to set.mm resolve the issue starting this thread (or are
at least a major step forward). I would like to thank all participants
here for their input. In the end that helped getting this done.
For the side considerations regarding df-cleq/df-clel: I had not time
enough to
What is ax-9c? It isn't an axiom in set.mm.
Norm
On Friday, October 29, 2021 at 1:46:46 PM UTC-4 di@gmail.com wrote:
> Here's a sketch of the proof of conservativity of the class axioms. We
> remove them one at a time: first removing df-clel, then df-cleq, and
> finally ax-9c, df-clab
Here's a sketch of the proof of conservativity of the class axioms. We
remove them one at a time: first removing df-clel, then df-cleq, and
finally ax-9c, df-clab and class all at once.
Assume that the base theory S has enough to move equivalences through the
logical connectives, and prove alpha
On Friday, October 29, 2021 at 6:05:19 PM UTC+2 Norman Megill wrote:
> Can you remind me what the minimal positive calculus is?
>
What I had in mind was {ax-mp, ax-1, ax-2, impbi, biimp, biimpr, simpl,
simpr, pm3.2}, or really anything that suffices to move the equivalences
through the other
Can you remind me what the minimal positive calculus is?
On Friday, October 29, 2021 at 11:58:02 AM UTC-4 Benoit wrote:
> The hypothesis of bj-df-cleq corresponds to setvar substitutions into A
>> and B. Do we know that other substitutions into A and B can't generate FOL=
>> statements that
>
> The hypothesis of bj-df-cleq corresponds to setvar substitutions into A
> and B. Do we know that other substitutions into A and B can't generate FOL=
> statements that are stronger than the hypothesis? Perhaps we are safe since
> we may need df-cleq itself to eliminate the resulting class
On 10/28/21 2:20 PM, Benoit wrote:
> I think we should keep the "overloading" of equality and membership.
> The assumption is not hidden in set.mm, but explicit: it is ~cv
> (http://us2.metamath.org/mpeuni/cv.html). I still favor the forms
> bj-df-cleq/bj-dfclel, which imply minimal changes
On Thu, Oct 28, 2021 at 7:19 PM Norman Megill wrote:
> 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 true, but a
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
I think we should keep the "overloading" of equality and membership. The
assumption is not hidden in set.mm, but explicit: it is ~cv
(http://us2.metamath.org/mpeuni/cv.html). I still favor the forms
bj-df-cleq/bj-dfclel, which imply minimal changes over the current set.mm,
and which fix the
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
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
I am going to read carefully through all this during weekend, or whenever I
have more time to focus on details particularly about where are the limits
of a proof scheme like Metamath. For now I would like to remind of the
starting point of this thread.
And this is a problem pertaining to the
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
The stance I take in MM0 is that df-cleq is a definition, but it is
defining class equality in terms of set equality. The suspicious thing that
set.mm is doing is asserting that the two are the same by definition,
implicitly by representing x = y as wceq (cv x) (cv y). If you have two
equalities,
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.
If, as you write, ax-9 is not important any
Which comment of Benoît you are referring to?
Anyway, he has brought this up before; see bj-ax9, which derives ax-9 from
df-cleq (with the help of additional axioms ax-1 through ax-7, ax-12, and
ax-ext), and bj-df-cleq, which is proposed as a replacement for df-cleq.
See also my comment at
46 matches
Mail list logo
