Erweiterung df-cleq

[ookami]

I think Benoit Jubin is right when stating, that df-cleq need not only ax-ext as its prerequisite, but also ax-9.

This issue recently surfaced when KP noticed in a commit comment, that a dependency on ax-9 was unexpectedly removed from his proof, too.

The reason why ax-ext is referred to in df-cleq is explained in its comment.  The same logic holds also for ax-9.  Consequently, one should adapt the definition df-cleq accordingly.  Apart from dfcleq, no other proof should be affected by this move.

Are there objection to this extension?

Wolf Lammen

[Norman Megill]

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 https://github.com/metamath/set.mm/pull/965#issuecomment-506578377 . Basically, once we are in set theory, we no longer care about the details of the underlying classical FOL with equality.

set.mm already goes much further than almost all textbooks, which state df-cleq without an explicit ax-ext hypothesis like we do (although they may mention it in passing).  I myself have wondered if that was going too far in set.mm.  I don't think I have ever seen in any book a concern about which FOL axioms are needed to justify a set theory definition; indeed, many set theory textbooks don't even show an FOL axiomatization but assume the reader will use their favorite.

It would be fine to add to the df-cleq comment an explanation of these things, with links to bj-ax9 and bj-df-cleq, but I am not in favor of changing the existing df-cleq itself.

Norm

[ookami]

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 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?
   
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.

I am at a loss how text books handle these issues; I never read one on logic.  I am willing to believe that Metamath outperforms a majority of them.  But this should be no reason for missing out an improvement, right?

So far I think there is unusual complexity inherent to df-cleq, and since you cannot avoid people possibly be overwhelmed by it, you can at least syntactically take a clean stance.

Wolf

[Mario Carneiro]

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, then there is nothing odd going on in df-cleq, and you can then prove a theorem that weq x y is equivalent to wceq (cv x) (cv y). This theorem will require ax-ext (and presumably ax-9 as well).

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/34ea47c9-0b57-4b1c-8cc4-6e81617a3fefn%40googlegroups.com.

[ookami]

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 df-clel that ( x e. A -> E. y y e. A ) with y, A distinct holds.  Thus df-clel leaves the semantics of x e. A almost always undecided, the exemption being the empty set.

This is a sensible, but not obvious result of the pair df-cleq and df-clel.

Now lets look at how A. x ph is handled.  At the time of introduction nothing is known about that operation, too.  It could mean "count the x in ph and return true only iff its an even number".  Axioms now narrow the semantics down.  ax-gen is already sufficient to render the suggested meaning invalid.

Note that df-cleq and df-clel do NOT explain x e. A, and hence are not definitions then.  Their role in this particular case is that of an axiom somehow imposing a meaning on a generally undefined expression by specifying the empty set case.

I remember, I had to sort out this kind of ideas a couple of years ago.  In the end I was satisfied, but that was not a "10-minutes walk".

Wolf

[Mario Carneiro]

On Wed, Oct 27, 2021 at 5:26 AM 'ookami' via Metamath <meta...@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 e. A isn't supposed to have any definition, it is axiomatic, and can mean any proposition at all. We get completeness after df-clab. This is, roughly speaking, the "definition of 'class'": a class is a unary predicate on sets, and this is the application operator.

 

It is known to be well-formed (by wcel), though, so our typical logical manipulations apply.  It follows from df-clel that ( x e. A -> E. y y e. A ) with y, A distinct holds.  Thus df-clel leaves the semantics of x e. A almost always undecided, the exemption being the empty set.

df-clel is another instance of notation overloading, defining A e. B in terms of x e. A. There is no primitive constructor for x e. A but let's call it wvel for the purpose of discussion, such that wvel x A = wcel (cv x) A; then df-clel is defining wcel in terms of wvel (which is axiomatic and introduced along with the new sort "class"; in type theory parlance we would say that wvel is the eliminator for "class" and cab is the constructor). The axiom that connects these two axiomatic constructors is df-clab.

In the case of the empty set, the reason x e. (/) is determined is because of the definition of the empty set, not the definition of wvel (which is maximally generic). Since we define (/) using the constructor for "class", i.e. (/) = {x | F.}, we obtain the theorem x e. (/) <-> F. using df-clab.

Now, it is true that df-clel and df-cleq are doing a bit more heavy lifting than just described because of the notation overloading. More specifically, we need a way to prove that x e. A acts like a regular predicate, i.e. satisfies equality on the left and right. On the right, we get this by definition, since this is how wceq is defined (in terms of wvel). On the left this needs to be axiomatized, like a strengthened version of ax-8, but df-clel + notation overloading makes it derivable. Additionally, we need to pin down what cv does; but this is because wvel x (cv y) = wel x y by definition (because of the notation overloading). Without the overloading, this would be considered the definition of cv, i.e. x = { y | y e. x } (to be precise, "cv x = cab x (wel y x)") would be "df-cv".

Mario

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/1e7e79a3-c369-42a7-a2b4-d6c43b923a76n%40googlegroups.com.

[ookami]

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 A):  -. x e. A (what else demands this?).  I don't know whether this is of importance, like to go through this in greater detail, but this has to wait until evening.  Again, it highlights that  you have to be careful.

Wolf

[Mario Carneiro]

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 skimping out on this axiom and using df-cleq to prove it instead, which makes it a load-bearing definition which is not great.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/702d5dd4-910b-4ac0-88d9-f9712491c77en%40googlegroups.com.

[Norman Megill]

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.

 

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

[Mario Carneiro]

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.

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/be783362-425b-4fb3-b07e-e04d87e756a4n%40googlegroups.com.

[Norman Megill]

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.

[ookami]

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 from ax-12, but is provable from ax-13 too.  This simply says, that our axiomatic system is not "orthogonal".  There are overlapping areas where in particular border cases are provable using different axioms.  A simple solution to this ambiguity is to prioritize axioms and prefer those appearing first.

2. Definition vs axiom.  One should still note that df-clel and df-cleq are definitions, too.  As long as you feed in A e. B and A = B, these expressions are explained and reduced to more basic expressions x e. A and x e. B.  Only if you iterate again and apply the definitions to the freshly created terms you run into trouble.  I think a clean approach would follow Mario's idea and state some basic facts about x e. A as axioms.  Along the lines of modifying ax-9 or ax-8, as he suggested.  Not doing so leaves open a gap, where not all results from set theory are rigorously traced back to fundamental ideas.  While one can certainly live with some blurred results, this is a bit against the philosophy of Metamath.  If you ask me.

3. Thanks for your answers and interest in my posting.

Wolf

[Benoit]

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

[Mario Carneiro]

On Wed, Oct 27, 2021 at 11:40 AM Norman Megill <n...@alum.mit.edu> 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 think that this is true. In fact, ZFC + classes is a conservative extension in exactly the same way that NBG is, especially if you pay attention to metalogical completeness. 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. 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.

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 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 *actually* proving new lemmas, it's not merely a theoretical concern. If ax-9c at least existed as an axiom, then we could at least say that the definitions are not load-bearing, they only prove theorems that were already true beforehand, but it's not that way in the current setup. I think this weakens the trust in the overall distinction between definition and axiom, so users can't just ignore the "This theorem depends on definitions" list, which is much larger than the axioms list.

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.

 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 axioms then readers might think that ZFC isn't enough for mathematics (which I actually think is mostly true - the class extension exists in metamath for a very good reason), and if we mark them as definitions then people (like Wolf in this very thread) might get confused about by what standard we judge axioms to be "definitions", which is a question of high importance considering that it forms part of the trusted base of metamath (since verifiers don't check it).

[Norman Megill]

(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 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 think that this is true.

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.

 

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?

 

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.

 

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.

 

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?

 

 

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.

 

*actually* proving new lemmas, it's not merely a theoretical concern. If ax-9c at least existed as an axiom, then we could at least say that the definitions are not load-bearing, they only prove theorems that were already true beforehand, but it's not that way in the current setup. I think this weakens the trust in the overall distinction between definition and axiom, so users can't just ignore the "This theorem depends on definitions" list, which is much larger than the axioms list.

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.

 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?

 

axioms then readers might think that ZFC isn't enough for mathematics (which I actually think is mostly true

Whether or not ZFC is enough for mathematics, class notation does not strengthen it.

- the class extension exists in metamath for a very good reason), and if we mark them as definitions then people (like Wolf in this very thread) might get confused about by what standard we judge axioms to be "definitions", which is a question of high importance considering that it forms part of the trusted base of metamath (since verifiers don't check it).

The standard is that a definition must be conservative and eliminable.

Norm

 

[Mario Carneiro]

On Wed, Oct 27, 2021 at 7:22 PM Norman Megill <n...@alum.mit.edu> 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

[ookami]

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 current version of Metamath.  The thread started from the observed fact, that the axiom list is somewhat flaky, "a good estimate of what should be in it, nothing more".  This is something I am personally less content with.  One reason is that I use this list on regular base to separate the regions of concern of any axiom. It is a source of incentives for proof modification, and I hate the idea, it cannot be used thoughtlessly. Actually the list seem to be very close to perfect, and I cannot see a good reason to leave the final gap open.

The analysis has lead to df-clel and df-cleq as the culprits for the observed shortcoming.  To my understanding they bear unnecessary complexity, and despite their name, they are not laid out according to the rules of pure doctrine, requiring definitions to be conservative (one downside of never having read a text book on logic is that I developed a language on my own, and now have to adapt to common usage).  What I sense in this thread is some reluctance to address this defect, and I still havent't grasped the reason behind it.  Is it habits?  Is it some superficial imitation of concept of other sources?  I don't know. I like to urge getting back on the track of rigor, that convinced me some ten years ago.

I initially asked permission to add ax-9 to the list of covered axioms by df-cleq.  This is likely not the best solution, because it does not address the observed lack of conservaty.  What about the solution of Benoit then?  Or develeping an intermediate stage between set theory and class theory? Or something else experimental.

Is it possible to make some progress in this direction?  Or come up with a (hopefully) convincing reason to stop where we are.

Wolf

[Thierry Arnoux]

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.

       However, to conform to literature usage, we retain this overloaded
       definition.  This also makes some proofs shorter and probably easier to
       read, without the constant switching between two kinds of equality.

As far as I understand Mario has chosen this in MM0.

--

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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/879eb864-f2b1-40a3-9018-c5a698ad5ac8n%40googlegroups.com.

[Scott Fenton]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/28471da3-9ad8-a648-d251-258af55f22e9%40gmx.net.

[Benoit]

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 concrete problem of having later theorems which misleadingly do not indicate ax-8 or ax-9 as a dependency (which is the problem which started this thread).  And Wolf, who started the thread, seems to agree.

Then, we can think about calling them definitions or axioms.  For the moment, I do not have an opinion: what's important is that they are $a-statements, and the distinction axiom/definition, apart from a matter of taste, has implications on other tools (mmj, mm0) which I do not know enough yet.  To put what Mario wrote differently, and a bit roughly: they are more like definitions at the object level (eliminable and conservative), and more like axioms at the meta level (eliminable, see the section beginning with http://us2.metamath.org/mpeuni/eliminable1.html, but not conservative).  This is similar to ax-10, ax-11, ax-13 being redundant at the object level, but not (conjecturally for all, and at least for ax-13) at the meta level.

Finally, there is the possible further step I mentioned at https://github.com/metamath/set.mm/pull/965#issue-461788828 of splitting bj-df-cleq/bj-df-clel in two halves to study more precisely their implications (in which case, they would be axioms, not definitions).

Benoît

[Norman Megill]

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

[Mario Carneiro]

On Thu, Oct 28, 2021 at 7:19 PM Norman Megill <n...@alum.mit.edu> 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 metamath assertion is more than just its image on the object language. If you view a metamath assertion as simply a set of object language theorems then there is no distinction between logical completeness and metalogical completeness.

 

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).

It is possible to state global choice in ZFC+classes, and indeed this has been proposed for set.mm in the past. It is a conservative extension, so when you say it is "stronger" this is only as a theorem of NBG or ZFC+classes in the extended language; the base language is not strengthened by the presence of global choice.

> 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.

I think in this case "extension by definitions" is talking about definitions in the strict sense, i.e. the kind that can be checked by mmj2.

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?

The term "extralogical axioms" is usually applied to anything beyond (predicate) logic, e.g. the axioms of ZFC as distinct from pure FOL.

Just to be clear, I am okay with the current state of affairs, this isn't a hill I am willing to die on. To the extent that we can, we should call these oddities out and clarify them for readers, but tools can work around this ( "$j not-really-a-definition "df-clel";" anyone?), and removing the notation overloading has a high cost for users and the library generally, so the tradeoff may not be worth it.

[Norman Megill]

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 over the current
> set.mm, and which fix the concrete problem of having later theorems
> which misleadingly do not indicate ax-8 or ax-9 as a dependency (which
> is the problem which started this thread).  And Wolf, who started the
> thread, seems to agree.

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 notation, but I haven't thought it through completely to be sure there aren't tricks that can be done with the other two class definitions.  What do you think?

A radical solution that would guarantee complete isolation of df-cleq from FOL= would be to use a conjunction of all FOL= axioms (and ax-ext) as the df-cleq hypothesis.  But that would be ugly, and we might get the opposite complaint that too many FOL= axioms become required to use df-cleq. :)

Norm  

[Benoit]

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 notation, but I haven't thought it through completely to be sure there aren't tricks that can be done with the other two class definitions.  What do you think?

If I understand your question correctly, then the following result might answer your concerns:

Theorem:  Let S be any set of schemes.  Assume that we can prove a scheme Phi which contains no class terms or class variables from S \cup \{df-clab, bj-df-cleq, bj-df-clel\}.  Then, we can prove it from S \cup {minimal positive calculus}.

Proof:  Consider a proof of Phi from S \cup \{df-clab, bj-df-cleq, bj-df-clel\}.  Using \{df-clab, bj-df-cleq, bj-df-clel, minimal positive calculus\}, eliminate class abstractions from the proof.  There may also be dummy class variables; replace them with fresh dummy setvar variables.  Now, the proof contains no class abstraction so does not use df-clab, and for the lines using bj-df-cleq or bj-df-clel, they can be "removed" since the conclusion is an alpha-renaming of the hypthesis (more precisely, you prove their conclusion directly using the corresponding alpha-renaming of the proof of its hypothesis in the original proof). QED

Benoît

[Norman Megill]

Can you remind me what the minimal positive calculus is?

[Benoit]

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 connectives.  I realize one may also need ~alim and ~exim since these quantifiers occur in dfcleq/clel.  But actually, that part of my proof sketch is too sketchy... I should ponder a bit more on this, but it seems that the special form of bj-df-cleq/clel could permit to simplify Levy's proof in the appendix of Basic Set Theory.

Benoît

[Mario Carneiro]

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 renaming of FOL= formulas. Suppose we have a proof of Phi from S \cup \{df-clab, bj-df-cleq\} where Phi does not use any occurrences of A = B except on set variables; we will eliminate bj-df-cleq. If bj-df-cleq is not used in the proof then we are done, otherwise consider the first occurrence of bj-df-cleq in the proof. By minimality, the hypothesis to bj-df-cleq must not be proven using bj-df-cleq, so ax-ext is a theorem of S \cup \{df-clab\}. Now, pick a variable z not appearing in the proof, and replace all occurrences of A = B with A. z (z e. A <-> z e. B). At the leaves, we have transformed instances of axioms like ax-8': (A. z (z e. a <-> z e. b) -> (a e. c -> b e. c)), and we can prove this from ax-8 by replacing A. z (z e. a <-> z e. b) with a = b using ax-ext and equality theorems. Thus Phi' is provable from S \cup \{df-clab\}, and Phi differs from Phi' only in the replacement of some a = b with A. z (z e. a <-> z e. b), so we can use ax-ext and equality theorems to prove Phi as well.

The situation with df-clel is more complicated, and here is a failed proof of a similar reduction to replace A e. B with x e. A. Suppose S \cup \{df-clab, bj-df-cleq, bj-df-clel\} proves Phi, and Phi does not mention A e. B except as x e. A. If bj-df-clel is not used then we are done, else a minimal application of it shows that cleljust is provable from S \cup \{df-clab, bj-df-cleq\}. Now replace all instances of A e. B with E. z (z = A /\ z e. B) where z is a variable not occurring in the proof, and use cleljust (!!!) to replace each transformed E. z (z = x /\ z e. A) in axioms with x e. A, so that the original axiom + equality theorems proves the transformed axiom. Similarly, we prove Phi' <-> Phi and thus Phi is provable from S \cup \{df-clab, bj-df-cleq\}.

This proof fails at the (!!!), because we need to know that x e. A <-> E. z (z = x /\ z e. A), and cleljust is not good enough to cover this situation. We can repair the proof with a variation on bj-df-clel that looks like this:

mc-df-clel.1 $e |- ( u e. B <-> E. v ( v = u /\ v e. B ) )

mc-df-clel $p |- ( A e. B <-> E. x ( x = A /\ x e. B ) )

We have to be more careful about uses of cleljust now because class variables in a hypothesis can't be substituted. Let cleljust[A] refer to the theorem |- ( u e. A <-> E. v ( v = u /\ v e. A ) ) for fixed A. We need to know that this is equivalent to |- ( x e. A <-> E. y ( y = x /\ y e. A ) ) (where u,v,x,y,A are all distinct), and I don't think this comes for free, so let us assume ax-9c is derivable from the base theory S. Now, for each application of mc-df-clel[A, B], there is a minimal one for each fixed B, and hence we get that cleljust[B] is derivable from S. For each such B we replace all occurrences of A e. B (for any A) with E. x ( x = A /\ x e. B ), then back substitute E. v ( v = u /\ v e. B ) to u e. B in transformed axioms and Phi to conclude (using cleljust[B] to validate the substitution).

Now this is interesting, because even if you have ax-9c directly as a premise to mc-df-clel, it's still not good enough to derive variations on ax-9c with different set variables, because you need (different substitution instances of) ax-9c itself to prove the equivalence. So this trick with adding hypotheses to axioms is not sufficient in general, you can't just stick all of FOL as a hypothesis and hope that solves the situation.

Finally, we want to eliminate x e. A, which is the hardest part because it comes together with "class" and { x | ph } as a unit. Suppose Phi derives from S \cup \{df-clab\}, and Phi does not contain any class variables, any use of { x | ph }, any use of A e. B except as x e. y, and any use of A = B except as x = y. By substituting all dummy class variables B in the proof by { x | F. }, we get that Phi is derivable without any class variables in the proof. By the previous two transformations we can ensure that the proof also does not use A = B or A e. B except as x e. A. For the latter part, we need cleljust[B] to be derivable for various B, but because all class variables are eliminated from the proof, we only need cleljust[{x | ph}] for various choices of x,ph and this is derivable using df-clab. Thus we get a simplified proof of Phi from S \cup \{df-clab\} which only uses x e. A and { x | ph }. Now, since there are no class variables, every subformula of the form x e. A must have the form x e. {y | ph}, and so we can replace all instances of x e. {y | ph} with [x / y] ph. The transformed df-clab and ax-9c instances are theorems of S, and none of the other axioms mention cab or wvel. Since Phi is not changed by the transformation, Phi is derivable from S.

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/063cda68-5e30-45a8-8397-b694093b2924n%40googlegroups.com.

[Norman Megill]

What is ax-9c?  It isn't an axiom in set.mm.

Norm

[ookami]

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 think the topic over.  My first impulse after the discussion with Mario was a rigorous bottom-up design starting from x e. A , avoiding df-clab altogether, and axiomatize this term in a way that  df-cleq / df-clel become true definitions.  Later one can introduce df-clab and note that its interpretation of x e. A is a perfect match and hence a valid option (but no requirement!).  I am looking forward to have a look at the other suggestions as well.  Its too early for me to say I made up my mind.

Wolf

[Mario Carneiro]

On Fri, Oct 29, 2021 at 2:06 PM Norman Megill <n...@alum.mit.edu> 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).

[Benoit]

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 proof, don't you simply use a dummy setvar variable in place of it ?  Your proof is more or less what I was trying to write up, but I hadn't seen some of the subtleties... Maybe I'll come back with further questions.

Benoît

[Mario Carneiro]

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 time like I did. We can remove df-cleq, but ax-9c is derivable from FOL + {ax-ext, df-clab, df-clel} but not FOL + {ax-ext, df-clab}, that is, it is a concrete counterexample to conservativity of df-clel, at least if one reads df-clel naively as a definition of A e. B in terms of simpler quantities.

[Mario Carneiro]

On Fri, Oct 29, 2021 at 2:30 PM Benoit <benoit...@gmail.com> 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.

[Thierry Arnoux]

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 set.mm using GitHub's diff tool.
I've also put a description of my changes in the README.

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.

In any case, this approach involves duplicating many of the predicate
calculus theorems, proving them once in their set-only version, and then
again in their class version, so overall this method is not elegant and
I agree it shall not be pursued.

BR,
_
Thierry

On 29/10/2021 07:19, Norman Megill wrote:
> On 10/28/21 10:11 AM, Thierry Arnoux wrote:
>
> > A solution is mentioned in the comment for df-cleq, shall it be
> > reconsidered?

[Mario Carneiro]

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 e.c A } )
|- A. y ( y e.c A <-> y e.c { x | x e.c A } )
|- A = { x | x e.c A }


We need ax-8c as an axiom to prove the first line, but abidc should be derivable.

The second axiom, ( x e.c y <-> x e.s y ), is actually a definition: If we indicate the coercion explicitly as ( x e.c cv y <-> x e.s y ), then it should be clear that we can write it in definition form as

|- cv y = { x | x e.s y }


(which looks a lot like abidc but only because of the suggestive notation).

--
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 metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f387c42a-ac19-3979-851b-d5b6fb8e2638%40gmx.net.

[Benoit]

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 wrote ax-9c instead).  The need to define not two but three predicates for membership reflects the three step process in Levy's proof or Mario's proof above.

 

Benoît

[Benoit]

Sorry, our emails crossed with Mario, so when I was mentionning the proof above (and the typo), I meant the previous one!

[Mario Carneiro]

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 .

[Thierry Arnoux]

Thank you very much, Mario and Benoît, I will update the repository.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/CAFXXJSutSTcXhDB_ucpWitfy3ej7TpMO8MHS%2B-0a7FVzy36TcQ%40mail.gmail.com.

[Benoit]

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 recoverable from FOL= and df-clab, df-cleq, df-clel (stated without hypotheses, so you also remove ax-ext).  This is not very satisfying since df-cleq appears to group two axioms (the two directions).  You could split it into two, to get the system:
  $d x A $.  $d x B $.  [in all these axioms]
  df-clab $a |- ( x e. { y | ph } <-> [ x / y ] ph ) $.
  df-clel $a |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $.
  ax-classext $a |- ( A. x ( x e. A <-> x e. B ) -> A = B ) $. 
  ax-9clbi $a |- ( A = B -> ( x e. A <-> x e. B ) ) $.
It would be better to state ax-9clbi without a biconditional, as
  ax-9cl $a |- ( A = B -> ( x e. A -> x e. B ) ) $.
but then, you cannot prove anymore that = is an equivalence relation among classes.  So you have to strengthen ax-7 to
  ax-7cl $p |- ( A = B -> ( A = C -> B = C ) ) $.
Finally, df-clel also appears to group two axioms, and it appears clearer to split it into:
  ax-8clbi $a |- ( x = A -> ( x e. B <-> A e. B ) ) $.
  ax-elisset $a |- ( A e. B -> E. x x = A ) $.  [this is the current ~bj-elissetv]
Note that ax-8clbi needs a biconditional in its consequent.  You can remove it if you put a class variable in place of x, that is,
  ax-8cl $a |- ( A = B -> ( A e. C -> B e. C ) ) $.

Of course, you always have the syntactic axiom ~cv in all of these systems.  So to sum up, you can use the system
  {ax-mp, ax-gen, ax-1--6, ax-7cl, ax-8cl, ax-9cl, ax-classext, ax-elisset, df-clab}

where ax-8cl is replaceable by ax-8clbi, and ax-9cl could be strengthened by replacing in it x with a class variable, although this is recoverable.  It has the advantage of having simpler axioms, each one stating a single fact instead of grouping several facts.  In particular, it states as an axiom the fundamental bj-elissetv.  It has the disadvantage of not singling out FOL= (since ax-7 was replaced by ax-7cl) nor ax-ext in its textbook form.  They could be restored by adding the corresponding $e hypotheses to these axioms (the $e hypotheses would have exactly the same form as the $a conclusions, with class metavariables replaced by variable metavariables).

Benoît

[Norman Megill]

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 opinion is to simply remove ax-8 and ax-9.  By bj-ax8 and bj-ax9-2, they are recoverable from FOL= and df-clab, df-cleq, df-clel (stated without hypotheses, so you also remove ax-ext).  This is not very satisfying since df-cleq appears to group two axioms (the two directions).  You could split it into two, to get the system:
  $d x A $.  $d x B $.  [in all these axioms]
  df-clab $a |- ( x e. { y | ph } <-> [ x / y ] ph ) $.
  df-clel $a |- ( A e. B <-> E. x ( x = A /\ x e. B ) ) $.
  ax-classext $a |- ( A. x ( x e. A <-> x e. B ) -> A = B ) $. 
  ax-9clbi $a |- ( A = B -> ( x e. A <-> x e. B ) ) $.
It would be better to state ax-9clbi without a biconditional, as
  ax-9cl $a |- ( A = B -> ( x e. A -> x e. B ) ) $.
but then, you cannot prove anymore that = is an equivalence relation among classes.  So you have to strengthen ax-7 to
  ax-7cl $p |- ( A = B -> ( A = C -> B = C ) ) $.
Finally, df-clel also appears to group two axioms, and it appears clearer to split it into:
  ax-8clbi $a |- ( x = A -> ( x e. B <-> A e. B ) ) $.
  ax-elisset $a |- ( A e. B -> E. x x = A ) $.  [this is the current ~bj-elissetv]
Note that ax-8clbi needs a biconditional in its consequent.  You can remove it if you put a class variable in place of x, that is,
  ax-8cl $a |- ( A = B -> ( A e. C -> B e. C ) ) $.

Of course, you always have the syntactic axiom ~cv in all of these systems.  So to sum up, you can use the system
  {ax-mp, ax-gen, ax-1--6, ax-7cl, ax-8cl, ax-9cl, ax-classext, ax-elisset, df-clab}

where ax-8cl is replaceable by ax-8clbi, and ax-9cl could be strengthened by replacing in it x with a class variable, although this is recoverable.  It has the advantage of having simpler axioms, each one stating a single fact instead of grouping several facts.  In particular, it states as an axiom the fundamental bj-elissetv.  It has the disadvantage of not singling out FOL= (since ax-7 was replaced by ax-7cl) nor ax-ext in its textbook form.

I am traveling and haven't had time to study this carefully, but here are some general comments.

I would prefer not to mess with FOL=.  ax-8 and ax-9 are part of Tarski's FOL= system, and removing ax-8 and ax-9 would make it incomplete as a stand-alone system.  Mixing up FOL= and class theory with some new axioms seems inelegant and confusing, probably more so to beginners.

There is nothing mathematically wrong with adding new definitions that depend on previously introduced axioms for their justification; books do this all the time.  We have mostly avoided this in set.mm, with the exceptions df-cleq and df-clel that need to justified "outside" of Metamath and whose justification needs some earlier axioms (ax-ext and some mild FOL=).

Adding new axioms for class theory sends the message that FOL= + ZFC is not sufficient for mathematics, when in fact all uses of df-cleq and df-clel can be eliminated by converting the notation back to the the native ZFC language (or more accurately to our scheme language, since class variables map to wff variables).  It's just not a "direct" substitution of definiens for definiendum like the other definitions in set.mm.  No new mathematics results from df-cleq and df-clel; they just provide a convenient notational device that makes set theory much more practical to work with.

 

  They could be restored by adding the corresponding $e hypotheses to these axioms (the $e hypotheses would have exactly the same form as the $a conclusions, with class metavariables replaced by variable metavariables).

I am more open to this, as long as it will put this to rest once and for all.  Do we know that other substitutions into A and B of df-cleq and df-clel can't generate FOL= statements that are stronger than these hypotheses?

Norm

 

Benoît

On Tuesday, November 2, 2021 at 4:18:35 AM UTC+1 Thierry Arnoux wrote:

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 is not yet introduced yet). We also want ax-8c to reference only primitive term constructors, so it should also use =s .

[ookami]

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 construction.

Wolf

[Norman Megill]

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 important stand-alone study that can be referenced in the main set.mm and the MPE home page. We do keep some permanent important things in mathboxes, such as the old FOL= axiomatization in my mathbox that is referenced in many places.  

[Benoit]

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, ax-1--13, cv, wceq, wcel: unchanged
${
  $d x y z A $.  $d x y z B $.  $d x y z C $.
  ax-7cl.v $e |- ( x = y -> ( x = z -> y = z ) ) $.
  ax-7cl   $a |- ( A = B -> ( A = C -> B = C ) ) $.
$}
${
  $d x y z A $.  $d x y z B $.  $d x y z C $.
  ax-8cl.v $e |- ( x = y -> ( x e. z -> y e. z ) ) $.

  ax-8cl   $a |- ( A = B -> ( A e. C -> B e. C ) ) $.

$}
${
  $d u v w x A $.  $d u v w x B $.
  ax-9cl.v $e |- ( u = v -> ( w e. u -> w e. v ) ) $.

  ax-9cl   $a |- ( A = B -> ( x e. A -> x e. B ) ) $.

$}
${
  $d u v w x A $.  $d u v w x B $.
  ax-classext.v $e |- ( A. u ( u e. v <-> u e. w ) -> v = w ) $.

  ax-classext   $a |- ( A. x ( x e. A <-> x e. B ) -> A = B ) $.

$}
${

  $d x A $.  $d x B $.

  ax-elisset $a |- ( A e. B -> E. x x = A ) $.

$}

df-clab $a |- ( x e. { y | ph } <-> [ x / y ] ph ) $.

ax-ext: unchanged
...
Note the maximal unbundlings.

One more thing: in order to prove that equality of classes is an equivalence relation, one needs Euclideanness (ax-7cl), and one also needs reflexivity, proved for instance using ax-classext (hence ax-ext).  That's not necessarily a problem, but it would be nice to be able to prove that equality of classes is an equivalence relation without these less basic axioms. (Note that in addition to Euclideanness, left-seriality (ax6ev) is enough to prove that the relation is an equivalence relation, so one could be tempted to use ax-elisset, but sethood hypotheses would stay, like ( A e. V -> A = A ) for reflexivity, and similar sethood hypotheses for symmetry and transitivity.)  Therefore, it may be better to replace ax-7cl with a single axiom (single in order to keep independence) asserting directly the wanted result that equality of classes is an equivalence relation.  This could be the less elegant

${
  $d x y z t A $.  $d x y z t B $.  $d x y z t C $.  $d x y z t D $.
  ax-cleq.v $e |- ( ( x = y -> ( x = z -> y = z ) ) /\ t = t ) $.
  ax-cleq $a |- ( ( A = B -> ( A = C -> B = C ) ) /\ D = D ) $.
$}

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 easier to understand than open formulas (and the problem of having specific instances as hypotheses creeps up in the conservativity theorem, it seems).

That is not necessarily a proposal to change the axiomatic, and certainly not in a hurried way.  At least it's here for future reference.  I looked a bit at these questions a few years ago, and even with the current axiomatization, one can remove many usages of ax-ext, df-cleq, df-clel (see the subsection titled "Classes without extensionality" in my mathbox).

Benoît

[Norman Megill]

 Why do you think universal closures are easier to understand? Personally I don't find them easier, if nothing else because the formula is longer and thus takes slightly more effort to parse mentally.

Moreover, instantiating the $e from the $a in your ax-cleq is an immediate and obvious substitution, whereas with universal closure in bj-df-cleq we also need applications of ax-gen.

Also, if we require the universal closures of the hypotheses, for consistency shouldn't we also require the universal closure of the conclusion? That would be awkward: for bj-df-clel we would have to prefix the $p with "A. x1 ... A. xn" along with the side condition "where x1,...,xn are the free variables in A and B", and of course the current set.mm doesn't even have a notation that allows us to express that.

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. Requiring all proof steps to be universally closed (as some FOL axiomatizations do) can make them quite tedious to work with. There are "Quine closures" and "Berry closures", each with a set of rules to add, drop, and reorder the quantifiers in universal closures as we apply ax-mp etc. These seem like a major distraction and complication vs. using simple open formulas, particularly when schemes are involved.

Maybe there are advantages to universal closures (sentences) for some theoretical purposes, but I don't see any advantage for set.mm.

 

(and the problem of having specific instances as hypotheses creeps up in the conservativity theorem, it seems).

 Where do you see this? In any case, can't we just apply ax-gen as needed if open formulas are problematic?  

Norm

[Jim Kingdon]

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 really know whether avoiding the free variables is just convention/tradition or whether it really is easier to learn this way. But it is pretty common in how people teach logic. For example: "a statement is a formula with no free variables (Margaris, p. 21) and "a formal proof is a finite sequence of statements" (p. 13) (these quotes are a bit out of context, in the sense that later chapters of Margaris, which aim to be more rigorous, are stated differently). Certainly when I was learning predicate logic I found ax-gen to be very confusing (perhaps because it really is hard to get your head around the idea that something can have a truth value when it contains free variables, or perhaps because of this educational tradition which will say a formula cannot have a truth value when it contains free variables).

Now, some sources may not be worrying about pedagogy but may be thinking of measuring quantifier alternations or other topics I understand dimly if it all. So there may be reasons for the universal quantifiers in some contexts that I'm not really aware of. But in the context of set.mm/iset.mm (which is where I spend my time these days), I have certainly gotten used to the statement meaning the same thing with or without the quantifier. It looks like in http://us.metamath.org/ileuni/onintexmid.html we picked the style without the quantifier but in others like http://us.metamath.org/ileuni/ordtriexmid.html (admittedly, a restricted quantifier here) or http://us.metamath.org/ileuni/ssfiexmid.html (here an unrestricted quantifier) we picked the style with the quantifier. Would http://us.metamath.org/ileuni/acexmid.html be easier to read if there was an "A. x" at the start, which would prevent the eye from having to hunt for the free variable in a fairly long formula? I sort of gave up on having a strong opinion one way or the other a while ago.

[Benoit]

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 easier to understand than open formulas

 Why do you think universal closures are easier to understand? Personally I don't find them easier, if nothing else because the formula is longer and thus takes slightly more effort to parse mentally.

I think we generally do not see a difference in difficulty because we got so used to the (very standard) convention, "a formula holds exactly when its universal closure holds", so we mentally do the translation, so for us open formulas are as easy as their universal closures.  But you can see from the mere statement of this convention that the objects whose truth we first define unambiguously are sentences, and then we posit the above convention to give a truth value to open formulas as well.  This convention is not always the most convenient (for instance on the empty domain of discourse (see Leblanc, Meyer, Open formulas and the empty domain, Arch. math. Logik 12 (1969), 78--84), or in free logic, that is, with a domain with non-denoting, or non-existent, objects).  Of course, in set.mm there is no difference, and on the proof theoretic side, ax-gen/spi allow us to go back and forth.  In general, ax-gen holds, but spi may not hold, so the universal closure is weaker.  An example of this in set.mm is ax6vsep, which proves ax6v from {propcalc, ax-ext, ax-sep}.  To me, this shows that ax-sep is too strong, and should be replaced by its universal closure (for ax-ext, this is less important, since we then posit class extensionality and there is no quantification over classes).

 

Moreover, instantiating the $e from the $a in your ax-cleq is an immediate and obvious substitution, whereas with universal closure in bj-df-cleq we also need applications of ax-gen.

Indeed.  I was a bit torn to weaken the similarity of the $e and $a statements in e.g. bj-df-cleq.  But I think we should give this up because of the above paragraph.  Additionally, the lesser similarity is due to the fact that we cannot quantify over classes, so this is an occasion to ponder why this is so, especially in the context of free logic (I found the articles of the online Stanford Encyclopedia of Phylosophy very interesting: articles "Free logic" and "Nonexistent objects").

 

Also, if we require the universal closures of the hypotheses, for consistency shouldn't we also require the universal closure of the conclusion? That would be awkward: for bj-df-clel we would have to prefix the $p with "A. x1 ... A. xn" along with the side condition "where x1,...,xn are the free variables in A and B", and of course the current set.mm doesn't even have a notation that allows us to express that.

No, I think bj-df-clel is OK as is.  As I wrote above, classes cannot be quantified over anyway.  I do not aim to have only closed formulas, far from it.  Axioms would preferably be expressed in closed form, but then we can make free use of spi to remove initial quantifiers.  See e.g. ileuni/ax-strcoll immediately followed by ileuni/strcoll2 --- unfortunately, I did two things at once there, but the idea would be to have "ax-ext $a |- A. x A. y ( A. z ( z e. x <-> z e. y ) -> x = y ) $." (with correct dv's), immediately followed by "axext $p |- ( A. z ( z e. x <-> z e. y ) -> x = y ) $= [using spi twice] $.".

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. Requiring all proof steps to be universally closed (as some FOL axiomatizations do) can make them quite tedious to work with. There are "Quine closures" and "Berry closures", each with a set of rules to add, drop, and reorder the quantifiers in universal closures as we apply ax-mp etc. These seem like a major distraction and complication vs. using simple open formulas, particularly when schemes are involved.

Some books want to have only sentences and avoid use of generalization (like in one section of Tarski's article that serves as our foundation).  Again, this is not my aim at all here.  And like you, I'm not sure why they go into so much trouble to do so.  Note that most proofs of Godel's completeness theorem found in textbooks allow only sentences; some (minor) work has to be done to extend it to open formulas as well.  This may be one of the reasons.

 

Maybe there are advantages to universal closures (sentences) for some theoretical purposes, but I don't see any advantage for set.mm.

I mostly agree, which is why I propose to do as I wrote above with ax-ext followed by axext.  The advantage I see is being closer to textbook axioms, and especially not stating stronger axioms (again, ax6vsep is a good example).

 

(and the problem of having specific instances as hypotheses creeps up in the conservativity theorem, it seems).

 Where do you see this? In any case, can't we just apply ax-gen as needed if open formulas are problematic?  

Mario's proof of the conservativity theorem above in this thread (https://groups.google.com/g/metamath/c/xdHB0oW0aZ4/m/8Rfzy_lWAQAJ) is for hypotheses-free theorems.  In the first paragraph, where he concludes "so ax-ext is a theorem of S \cup \{df-clab\}", we need to change it, when there are hypotheses, to "so ax-ext is a theorem of S \cup \{df-clab\} or is a hypothesis of Phi" [actually, we have to be more precise that it is "that" particular instance of ax-ext].  But two sentences later in his proof, one sees that other instances of ax-ext may be needed. Therefore, it is more convenient to have a sentence for ax-ext, since then another instance is simply obtained by alpha renaming.  Maybe one can do without this, but at the price of more complexity, I think.

Benoît