RFC: Mandatory definitions after constants

[Mario Carneiro]

Hi All,

This is a fairly irrelevant looking change, but it does affect most of the library as well as the mathboxes, so I would like to RFC it for a bit. In an attempt to make definitions clearer and avoid ordering ambiguities, I would like to institute a convention that each definition comes directly after the constant it introduces. So we have

$( Text text. $)

cfoo $a class foo $.

$( Text text. $)

df-foo $a |- foo = ( x e. bar |-> x ) $.

but the following would not be allowed:

$( Text text. $)

cfoo $a class foo $.

$( Text text. $)

cbar $a class bar $.

$( Text text. $)

df-bar $a |- bar = ( x e. foo |-> x ) $.

$( Text text. $)

df-foo $a |- foo = ( x e. bar |-> x ) $.

I used circular definitions here to make the problem obvious, but the basic issue is the ambiguity of definition ordering when metamath has no innate notion of "a definition" as a unified whole. Spreading the definition across many statements makes the problem even worse. If I see a constant, how far forward do I need to scan to find out whether this is actually a definition? The mmj2 definition checker uses the location of the term constructor to determine the valid dependencies in the definitions, but it has to scan forward arbitrarily to find the definitions.

The solution proposed here is light-weight: just put the df-foo immediately after foo with no intervening statements. Any syntax axiom not followed by a definition axiom is considered to be a primitive term constructor.

Currently, we use a combination of term/def pairs like this, and term/term/term/def/def/def style in larger sections. I haven't looked in detail at the mathboxes, but I believe the story is similar. I don't think term and def are separated by more than a section anywhere in set.mm, and it is rare for theorems to appear in the section header area, so I expect there will be no effect on proofs.

Mario

[ookami]

Am Freitag, 14. Juni 2019 14:55:10 UTC+2 schrieb Mario Carneiro:

[..] If I see a constant, how far forward do I need to scan to find out whether this is actually a definition? [..]

My mathbox will not be affected by your proposed change.  I am unable to judge whether this change has unwanted side effects in the future, preventing something like your depicted circular references. However, if you aim at coupling the constant definition and its usage in a definition more tightly, why not make this explicit by extending the syntax of a constant definition like this:

$( Text text. (Referenced in definition df-foo.)  $)

cfoo $a class foo $.

This will not break current parsers, or editors sensitive to Metamath grammar. The style is already used with New usage.. and Proof modification.. tags, so it does not introduce anything new to Metamath.

What about implicit definitions like df-bi, but involving two constants in two defining expressions? Do you really want to rule out this?

Wolf

 

[Alexander van der Vekens]

I think it is a good idea to couple the definition with the corresponding  constant declaration. Since it is not allowed to have several definitions for the same constant (I made this experience some hous ago ;-)), I see no problems with it. But why not be more strict and combine the text areas (as far as I can remember they are mostly redundant), e.g.:

$( Text text. $)

cfoo $a class foo $.

df-foo $a |- foo = ( x e. bar |-> x ) $.

Concerning the circular definitions: are there any meaningful cases, or even already examples in set.mm?

Alexander

[Benoit]

I would welcome such a convention.  Some syntax statements are not associated with definitions (e.g. wi, wn, cv, wal) and I see that you took this into account in your proposal.  What would the precise convention be? Is it:

  Every statement with label df-xxx is an $a-statement with typecode |- and is immediately preceded by an $a-statement with typecode wff and label wxxx or with typecode class and label cxxx.

Some label changes I see (skimming through mmdefinitions.html) are:
  wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though df-bi is a special case
  df-v --> df-vv (to match cvv and avoid collision with cv)

Handling of df-clab, df-clel, df-cleq ? These are special cases, df-clel and df-cleq for the necessary early position of the associated syntax statements (for "overloading" purpose), and df-clab for the special form of the definition.  In any case, I would still like the labelling consistency, e.g.
  wceq --> wcleq
  wcel --> wclel

Benoit

[Norman Megill]

I can go along with this.

My first question is, how will it be checked?  Can the mmj2 definition check be modified to ensure it?

Norm

[Norman Megill]

On Friday, June 14, 2019 at 9:56:57 AM UTC-4, ookami wrote:

Am Freitag, 14. Juni 2019 14:55:10 UTC+2 schrieb Mario Carneiro:

[..] If I see a constant, how far forward do I need to scan to find out whether this is actually a definition? [..]

My mathbox will not be affected by your proposed change.  I am unable to judge whether this change has unwanted side effects in the future, preventing something like your depicted circular references. However, if you aim at coupling the constant definition and its usage in a definition more tightly, why not make this explicit by extending the syntax of a constant definition like this:

$( Text text. (Referenced in definition df-foo.)  $)

cfoo $a class foo $.

If the syntax axiom is placed immediately before the definition, which I think is what Mario proposed, this tag seems a little bit redundant since it is easy to check either by a human or a program.

This will not break current parsers, or editors sensitive to Metamath grammar. The style is already used with New usage.. and Proof modification.. tags, so it does not introduce anything new to Metamath.

What about implicit definitions like df-bi, but involving two constants in two defining expressions? Do you really want to rule out this?

The four definitions df-bi, df-clab, df-cleq, and df-clel are excluded from the current definition check.  Any new software will have to treat these 4 as special cases, for example by treating them as additional axioms.  Hopefully these 4 are the only ones that will ever need special treatment.

Norm

[ookami]

Am Freitag, 14. Juni 2019 19:30:43 UTC+2 schrieb Norman Megill:

On Friday, June 14, 2019 at 9:56:57 AM UTC-4, ookami wrote:

Am Freitag, 14. Juni 2019 14:55:10 UTC+2 schrieb Mario Carneiro:

[..] If I see a constant, how far forward do I need to scan to find out whether this is actually a definition? [..]

[..] However, if you aim at coupling the constant definition and its usage in a definition more tightly, why not make this explicit by extending the syntax of a constant definition like this:

$( Text text. (Referenced in definition df-foo.)  $)

cfoo $a class foo $.

If the syntax axiom is placed immediately before the definition, which I think is what Mario proposed, this tag seems a little bit redundant since it is easy to check either by a human or a program.

Apparently I was not clear enough. By using a tag (or other kind of reference) the positioning of entries remains unrestricted, open for any future development. I interpreted Mario's foo/bar example in a way that he himself was in doubt whether forcing constant and definition into consecutive entries might cause harm in the future.

Wolf

[..]
Norm

[Mario Carneiro]

On Fri, Jun 14, 2019 at 10:15 AM 'Alexander van der Vekens' via Metamath <meta...@googlegroups.com> wrote:

Concerning the circular definitions: are there any meaningful cases, or even already examples in set.mm?

There are no circular definitions in set.mm. I was not clear, but the mmj2 definition checker uses the order of constants (not the definition) to determine which definitions are allowed to reference which others. So in the circular reference example, bar would be allowed to refer to foo but foo would be rejected as a forward reference (even though the constant bar is declared before the definition foo, the constant foo is declared before constant bar).

On Fri, Jun 14, 2019 at 10:16 AM Benoit <benoit...@gmail.com> wrote:

I would welcome such a convention.  Some syntax statements are not associated with definitions (e.g. wi, wn, cv, wal) and I see that you took this into account in your proposal.  What would the precise convention be? Is it:

  Every statement with label df-xxx is an $a-statement with typecode |- and is immediately preceded by an $a-statement with typecode wff and label wxxx or with typecode class and label cxxx.

I would like to get away from label conventions in favor of something machine readable and not hardcoded. The mechanism I propose is:

  If an $a statement is given for a syntax typecode (i.e. not |-), then it is a definition iff the immediately following statement is a definitional axiom $a |- foo = ... which satisfies the usual rules. Otherwise, it is treated as an axiom, and a warning is issued if the label convention implies that the axiom would like to be treated as a definition and there is no warning-suppressing pragma attached to the axiom.

We can add $j commands to define the df-* convention for issuing warnings, and suppressing warnings on the definitions that aren't actually definitions but are called df-* anyway.

Some label changes I see (skimming through mmdefinitions.html) are:
  wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though df-bi is a special case
  df-v --> df-vv (to match cvv and avoid collision with cv)

The general rule has been to make constant names as short as possible while still disambiguated, because they are not visible to the user. (I'm starting to regret this choice in the recently completed lean translation because these names are literally all that I see.) In particular, making wceq and wcel longer will have a significant effect on total size of set.mm because they are by far the most common theorems applied. (Maybe we should use a Huffman encoding to choose label lengths?)

On Fri, Jun 14, 2019 at 1:22 PM Norman Megill <n...@alum.mit.edu> wrote:

My first question is, how will it be checked?  Can the mmj2 definition check be modified to ensure it?

The definition checker is actually overdue for a rewrite. I've added a lot of $j's recently, and they should all be validated. I actually put a syntax error in a $j in one of my commits and it didn't get caught, which is bad. We need a complete reference of $j statements, which can update along with set.mm itself as new statements are created. Also the existing definition checker has hardcoded names all over the place, which has already caused problems on one occasion; adding a $j parser would fix this issue.

For now, let's just say it's unchecked but I will put this on my todo list.

On Fri, Jun 14, 2019 at 1:30 PM Norman Megill <n...@alum.mit.edu> wrote:

The four definitions df-bi, df-clab, df-cleq, and df-clel are excluded from the current definition check.  Any new software will have to treat these 4 as special cases, for example by treating them as additional axioms.  Hopefully these 4 are the only ones that will ever need special treatment.

I would like to renew my suggestion that we change these to ax-bi, ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an inconsistent naming convention, since we are signaling that these are definitions when they don't meet the criteria, and it's also a lie to the reader because these look like definitions and claim to be definitions and the user may even know that we check definitions for soundness, yet these definitions each have extremely subtle problems that make them invalid as definitions. If the goal is to be open and straightforward, I think it is a more honest approach to call them axioms and explain in detail why they are conservative. (In fact, df-cleq is not even conservative!)

On Fri, Jun 14, 2019 at 5:45 PM 'ookami' via Metamath <meta...@googlegroups.com> wrote:

By using a tag (or other kind of reference) the positioning of entries remains unrestricted, open for any future development. I interpreted Mario's foo/bar example in a way that he himself was in doubt whether forcing constant and definition into consequtive entries might cause harm in the future.

set.mm has never allowed for circular or mutual recursive definitions. Even if some specialized development required them, they would certainly be introduced as axioms, so there would be no pairing and it would be irrelevant. Ideally, a definition wouldn't be two statements at all, and deriving important semantic data based on positional information is messy, but metamath is what it is and I want a way to minimize data loss when interpreting the database without breaking backward compatibility or adding too much boilerplate.

Mario

[David A. Wheeler]

On Sat, 15 Jun 2019 07:05:43 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I would like to get away from label conventions in favor of something
> machine readable and not hardcoded.

I'm fine with adding additional mechanisms.
However, I'd like to keep using & enforcing the label conventions.
I find they're very helpful for the humans who are trying to read this stuff :-).
And once the humans start depending on the conventions, it's wise
to enforce the conventions so the fragile humans aren't misled.

Label conventions are also "machine readable". You can make them
not hardcoded by adding a mechanism to declare the label convention.

> The mechanism I propose is:
>
> If an $a statement is given for a syntax typecode (i.e. not |-), then it
> is a definition iff the immediately following statement is a definitional
> axiom $a |- foo = ... which satisfies the usual rules. Otherwise, it is
> treated as an axiom, and a warning is issued if the label convention
> implies that the axiom would like to be treated as a definition and there
> is no warning-suppressing pragma attached to the axiom.

That's extremely strict. Even though we don't use it in set.mm today,
I worry about being unable to escape it later.
I'd prefer that to be the *normal* case, but with a special statement
(say a $j) that means "it's a definition even though it's down here" statement.

> We can add $j commands to define the df-* convention for issuing warnings,
> and suppressing warnings on the definitions that aren't actually
> definitions but are called df-* anyway.

I would call the df-* definitions definitions, but otherwise sounds good.

> Some label changes I see (skimming through mmdefinitions.html) are:
> > wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though df-bi
> > is a special case
> > df-v --> df-vv (to match cvv and avoid collision with cv)
> >
>
> The general rule has been to make constant names as short as possible while
> still disambiguated, because they are not visible to the user. (I'm
> starting to regret this choice in the recently completed lean translation
> because these names are literally all that I see.) In particular, making
> wceq and wcel longer will have a significant effect on total size of set.mm
> because they are by far the most common theorems applied. (Maybe we should
> use a Huffman encoding to choose label lengths?)

I think conventions are good, even if it would increase the size of set.mm.

So I would support switching to "wDFNAME" everywhere. We've already been
moving to increasingly keep our label names consistent with the "df-NAME"
definitions. And while the constant names aren't usually
visible to the user, in your lean translation they *ARE* directly visible,
and they're also visible in the HTML showing definitions.

Also - the larger size only applies to the *expanded* size. When stored/transmitted
using git or .tar.gz or .zip, I believe these will be trivially compressed to essentially
the same size. This kind of sequence repetition is exactly what
compression algorithms are good at handling.

--- David A. Wheeler

[Norman Megill]

On Saturday, June 15, 2019 at 7:05:57 AM UTC-4, Mario Carneiro wrote:

Also the existing definition checker has hardcoded names all over the place, which has already caused problems on one occasion; adding a $j parser would fix this issue.

BTW if the checker is going to be rewritten, is this a good time to change the definition of T. to be A. x x = x <-> A. x x = x?  You mentioned that there is a special section for df-tru, and it could be eliminated if we make this change.

On Fri, Jun 14, 2019 at 1:30 PM Norman Megill wrote:

The four definitions df-bi, df-clab, df-cleq, and df-clel are excluded from the current definition check.  Any new software will have to treat these 4 as special cases, for example by treating them as additional axioms.  Hopefully these 4 are the only ones that will ever need special treatment.

I would like to renew my suggestion that we change these to ax-bi, ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an inconsistent naming convention, since we are signaling that these are definitions when they don't meet the criteria, and it's also a lie to the reader because these look like definitions and claim to be definitions and the user may even know that we check definitions for soundness, yet these definitions each have extremely subtle problems that make them invalid as definitions.

I'm pretty sure these meet the literature criteria of being valid definitions.  They are eliminable and don't add any new theorems when eliminated down to the primitive language.  The class definitions have detailed soundness proofs in the literature.  In what sense do you see them as invalid?

The problem with calling them axioms is primarily psychological, implying that the real axioms aren't sufficient to express ZFC. It sends the wrong message. Also, they will show up in the "This theorem was proved from axioms" list unless I hard-code them into metamath.exe to exclude them from that list.
 
The issue is that the tools to check them aren't sufficiently sophisticated (and probably will never be) to check that they are valid definitions, so we make them exceptions for the purpose of those tools.  (I think an early version of Ghilbert checked the soundness of df-bi using its justification theorem, but I don't recall the details.  @raph may wish to comment if he is listening.)  As far as I can tell, there will only be these 4 exceptions and no others in the future.  Tools could recognize an exceptions list like the mmj2 definition check does now.  Or perhaps add a special $j statement?  I think you already mentioned that checking tools shouldn't depend on labeling conventions.

If the goal is to be open and straightforward, I think it is a more honest approach to call them axioms and explain in detail why they are conservative.

But if they are conservative, then they aren't really new axioms.  We have very detailed explanations of df-clab, df-cleq, and df-clel on the MPE home page in the Theory of Classes section, and df-bi has a long explanation in its comment.  We could enhance the explanations if that would help.
 

(In fact, df-cleq is not even conservative!)

In the context of ZFC it is, if what you mean is that it depends on ax-ext.  That is also explained in the Theory of Classes.  And the definition has ax-ext as a hypothesis, so it doesn't actually depend on ax-ext until we eliminate that hypothesis.

Norm

[Mario Carneiro]

On Sat, Jun 15, 2019 at 12:11 PM Norman Megill <n...@alum.mit.edu> wrote:

On Saturday, June 15, 2019 at 7:05:57 AM UTC-4, Mario Carneiro wrote:

Also the existing definition checker has hardcoded names all over the place, which has already caused problems on one occasion; adding a $j parser would fix this issue.

BTW if the checker is going to be rewritten, is this a good time to change the definition of T. to be A. x x = x <-> A. x x = x?  You mentioned that there is a special section for df-tru, and it could be eliminated if we make this change.

Yes, that would work.

On Fri, Jun 14, 2019 at 1:30 PM Norman Megill wrote:

The four definitions df-bi, df-clab, df-cleq, and df-clel are excluded from the current definition check.  Any new software will have to treat these 4 as special cases, for example by treating them as additional axioms.  Hopefully these 4 are the only ones that will ever need special treatment.

I would like to renew my suggestion that we change these to ax-bi, ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an inconsistent naming convention, since we are signaling that these are definitions when they don't meet the criteria, and it's also a lie to the reader because these look like definitions and claim to be definitions and the user may even know that we check definitions for soundness, yet these definitions each have extremely subtle problems that make them invalid as definitions.

I'm pretty sure these meet the literature criteria of being valid definitions.  They are eliminable and don't add any new theorems when eliminated down to the primitive language.  The class definitions have detailed soundness proofs in the literature.  In what sense do you see them as invalid?

The problem with calling them axioms is primarily psychological, implying that the real axioms aren't sufficient to express ZFC. It sends the wrong message. Also, they will show up in the "This theorem was proved from axioms" list unless I hard-code them into metamath.exe to exclude them from that list.

The issue is that the tools to check them aren't sufficiently sophisticated (and probably will never be) to check that they are valid definitions, so we make them exceptions for the purpose of those tools.  (I think an early version of Ghilbert checked the soundness of df-bi using its justification theorem, but I don't recall the details.  @raph may wish to comment if he is listening.)  As far as I can tell, there will only be these 4 exceptions and no others in the future.  Tools could recognize an exceptions list like the mmj2 definition check does now.  Or perhaps add a special $j statement?  I think you already mentioned that checking tools shouldn't depend on labeling conventions.

Metamath is a formal verifier. When it says that something is true, we believe it because it's checking everything down to the axioms. If we take that spirit to definitions, it means that when we claim something is conservative, that should mean that we've checked that it is conservative, again down to axioms, down to some system that we can check generally for soundness. So that means that when faced with an unusual definition, we are faced with a choice: Either we formalize a generic checking process that can verify the definitional scheme in use, or we assert it as a fact and leave verification to the meta level, i.e. call it an axiom.

It's not sufficient that the definition be true or conservative; we have good reasons to believe that the real numbers are constructible in ZFC but we do the construction anyway, because we want to demonstrate it such that the computer can check it. I've gone to some trouble to come up with a valid definition schema, both in the mmj2 definition checker and again in MM0, and I think Raph also has a definition schema in Ghilbert. If we apply such a schema to metamath, we can justify most of the current definitions, but it's not exactly a check for conservativity so much as a syntactic check that implies conservativity as a metatheorem.

The definitions that fail the MM0 definition schema are df-tru, df-bi, df-clab, df-cleq, df-clel. For each of these, we have some reason to think that the definitions are conservative but something about the definition makes the standard analysis fail. So we need to either make the schema more complicated to accomodate them, or call them axioms (which is not a cop-out - it's communicating that the tool is not capable of validating the axiom, but we have reasons to believe it anyway and punt on verification to the meta level). Note that in the MM -> MM0 -> Lean translation, all axioms become proof obligations, so it's actually important that things are marked as axiom when we expect a meta level proof.

* df-tru is problematic for reasons I've discussed in another thread (the lack of existential quantification over wffs). But a resolution is proposed so I will skip this.

* df-bi is not written as an iff. It has a definition but df-bi itself doesn't make it obvious what that definition is. The theorem is more like a consequence of the definition than the definition itself. This can be addressed by a $j that points to dfbi1 to indicate the definition of wb, and to bijust to indicate how to prove the unfolded statement. So I think this is addressable.

* df-clab is definitely not an axiom. It is a way to relate two primitive constructors. Metamath, and MM0, have no way to introduce new sorts by other than axiomatic means. HOL has function types and subset types, but these are in general not conservative extensions. We could have a definition schema that creates new sorts; in general, the admissible sorts would be a subclass of the collection of n-ary predicates on V. This is doable, but would be a pretty significant addition to the metatheory.

* df-clel and df-cleq are tricky because of the overloaded notation. At the very least there is a claim that weq x y <-> wceq (cv x) (cv y) that has been smuggled in without proof. Set theory is not required to justify the class sort, so perhaps it could be moved up and wceq and weq could be untangled. This would also avoid the need to have df-cleq depend on ax-ext.

 

If the goal is to be open and straightforward, I think it is a more honest approach to call them axioms and explain in detail why they are conservative.

But if they are conservative, then they aren't really new axioms.  We have very detailed explanations of df-clab, df-cleq, and df-clel on the MPE home page in the Theory of Classes section, and df-bi has a long explanation in its comment.  We could enhance the explanations if that would help.

Things which we think are correct but for which we have an informal justification rather than a formal proof are exactly what axioms are for. Obviously we prefer formal proofs over axioms when possible, but for the most part with definitions it's pretty obvious that we can't just remove the axiom or prove it from what precedes it.

(In fact, df-cleq is not even conservative!)

In the context of ZFC it is, if what you mean is that it depends on ax-ext.  That is also explained in the Theory of Classes.  And the definition has ax-ext as a hypothesis, so it doesn't actually depend on ax-ext until we eliminate that hypothesis.

It is conservative in the same sense that ax-17 is redundant. The classical theory doesn't have metavariables, so there are certain statements that metamath can express that aren't in the traditional accounting, and this slightly changes the meaning of "conservative" because the language is larger. To be more precise, the theorem |- ( A = B -> ( x e. A -> x e. B ) ) is expressible but not provable until df-cleq is introduced. As mentioned above, the introduction order of = and e. on classes is muddled up with the version for sets, and so as things stand today I can't call df-cleq and df-clel anything but axioms. If there were a few more variations on = and e. in the prelude, eliminated straight away similar to <RR, we could have these be plain definitions.

Mario

[Benoit]

On Sunday, June 16, 2019 at 7:35:04 AM UTC+2, Mario Carneiro wrote:

BTW if the checker is going to be rewritten, is this a good time to change the definition of T. to be A. x x = x <-> A. x x = x?  You mentioned that there is a special section for df-tru, and it could be eliminated if we make this change.

Yes, that would work.

I understand the advantages of this definition (I used this trick in ~bj-denotes) but I'm not sure this makes for the drawback of introducing syntax belonging to FOL= into propositional calculus (my candidate was ax-tru $a |- T. $.).  If you think it's ok, then so be it.  But maybe use implication instead of biconditional? i.e. ( A. x x = x -> A. x x = x ).

Benoit

[Mario Carneiro]

I'm also okay with making it an axiom - as I've said, I think axioms have their place and minimizing axioms isn't necessarily the best idea anyway. My impression has been that people prefer straightforward interpretations over fewer axioms. Things like ax-meredith are an interesting observation but no one actually builds logical systems on them, and the laws of boolean algebra are another example - everyone knows the list of axioms is redundant in a few places but it's easier to explain if we don't try to minimize things and break symmetry. I believe Norm's argument is that this suggests that ax-1,2,3,mp are not complete for propositional logic, but I think that's actually true if you use the metamath interpretation of "complete" as metalogically complete, because you can't get propositional constants without it. Anyway this is rehashing arguments in another thread so I'll leave it here.

As for replacing <-> with ->, I agree. Implication is a primitive constructor, and id is proven before biid, so this makes the definition simpler in both the definition itself and the proof of tru. There are shorter proofs than id, but none proves a shorter statement. (In fact, id is the shortest tautology in prop calc using only primitive constructors.)

Mario

[fl]

I don't want to interfere but you make me think of Orwell's Animal farm: 

All axioms are equal, but some axioms are more equal than others

:)

-- 

FL

[Norman Megill]

On Sunday, June 16, 2019 at 1:35:04 AM UTC-4, Mario Carneiro wrote:

I would like to renew my suggestion that we change these to ax-bi, ax-clab, ax-cleq, ax-clel. It adds complexity to the tooling to have an inconsistent naming convention, since we are signaling that these are definitions when they don't meet the criteria, and it's also a lie to the reader because these look like definitions and claim to be definitions and the user may even know that we check definitions for soundness, yet these definitions each have extremely subtle problems that make them invalid as definitions.

I'm pretty sure these meet the literature criteria of being valid definitions.  They are eliminable and don't add any new theorems when eliminated down to the primitive language.  The class definitions have detailed soundness proofs in the literature.  In what sense do you see them as invalid?

The problem with calling them axioms is primarily psychological, implying that the real axioms aren't sufficient to express ZFC. It sends the wrong message. Also, they will show up in the "This theorem was proved from axioms" list unless I hard-code them into metamath.exe to exclude them from that list.

The issue is that the tools to check them aren't sufficiently sophisticated (and probably will never be) to check that they are valid definitions, so we make them exceptions for the purpose of those tools.  (I think an early version of Ghilbert checked the soundness of df-bi using its justification theorem, but I don't recall the details.  @raph may wish to comment if he is listening.)  As far as I can tell, there will only be these 4 exceptions and no others in the future.  Tools could recognize an exceptions list like the mmj2 definition check does now.  Or perhaps add a special $j statement?  I think you already mentioned that checking tools shouldn't depend on labeling conventions.

Metamath is a formal verifier. When it says that something is true, we believe it because it's checking everything down to the axioms. If we take that spirit to definitions, it means that when we claim something is conservative, that should mean that we've checked that it is conservative, again down to axioms, down to some system that we can check generally for soundness. So that means that when faced with an unusual definition, we are faced with a choice: Either we formalize a generic checking process that can verify the definitional scheme in use, or we assert it as a fact and leave verification to the meta level, i.e. call it an axiom.

As presented to the public, Metamath is more than just a formal verifier.  It is also an educational tool that presents the ZFC axioms and derives things from them.  I think this is an important purpose.  For certain technically-minded people who aren't necessarily mathematicians, Metamath has opened up mathematics to them by showing precisely, step by step with very simple rules, how the symbols are manipulated to arrive at results, in a way that they did not fully grasp before.  AFAIK there is nothing else that comes even close to doing that.  Part of its educational goal is to explain the foundations of mathematics i.e. ZFC set theory to these people.  Calling df-clab,cleq,clel "axioms" sends the wrong message, that there's some extra murky stuff that we're not being open about in the beginning and that ZFC isn't sufficient for most of mathematics after all.

I think most people who are capable of understanding Metamath proofs can understand how to unwind a class expression by hand and even write a program to do it if they know some computer programming.  And I think they can grasp intuitively why class notation is a conservative definitional extension of ZFC and does not really add new axioms.

Since you plan to add $j tags to identify the nature of $a statements, can't they be used to indicate that df-cleq, etc. are axioms for your verifier's technical purposes, rather than depend on the hard-coded informal prefixes "ax-" and "df-"?  Let the $js indicate what are to be considered axioms by machines and demanding logicians, and let the prefixes indicate how they should be interpreted informally by most people.

Another thing that seems wrong is that we would be at the mercy of the sophistication of the definition checking tools, with things possibly changing from ax- to df- over time depending on how the tools evolve.  This may send a message that the foundations are unstable and poorly defined.  Again, wouldn't $j tags be a more appropriate place for that?

We are talking about only 3 or 4 definitions that will never change and never be added to, that are almost universally agreed upon to be valid definitions, that have been justified extensively in the literature.  There is zero doubt among mathematicians that they are conservative and eliminable. I don't think it is hard for most technically-minded humans to see that intuitively.  In the end, when you get down to the reliability of the transistors in the machine that runs the definition checks, there is no such thing as absolute certainly.  At some point common sense is needed to delineate what is acceptable, and to me, the "df-" prefix on these 3 or 4 definitions is an acceptable risk.
 
Norm

[Mario Carneiro]

On Tue, Jun 18, 2019 at 10:19 PM Norman Megill <n...@alum.mit.edu> wrote:

As presented to the public, Metamath is more than just a formal verifier.  It is also an educational tool that presents the ZFC axioms and derives things from them.  I think this is an important purpose.  For certain technically-minded people who aren't necessarily mathematicians, Metamath has opened up mathematics to them by showing precisely, step by step with very simple rules, how the symbols are manipulated to arrive at results, in a way that they did not fully grasp before.  AFAIK there is nothing else that comes even close to doing that.  Part of its educational goal is to explain the foundations of mathematics i.e. ZFC set theory to these people.  Calling df-clab,cleq,clel "axioms" sends the wrong message, that there's some extra murky stuff that we're not being open about in the beginning and that ZFC isn't sufficient for most of mathematics after all.

I totally agree on the usefulness of Metamath as an educational tool. But I also want to be sure that our actions match our words to the degree possible. I think that students who are interested in Metamath have already had enough of "white lies" about foundations, and are trying to dig to the heart of it. If ZFC is supposed to be enough, then let's build exclusively on ZFC. If there are pragmatic problems with that, then explain those problems as you add an axiom to that effect.

 

I think most people who are capable of understanding Metamath proofs can understand how to unwind a class expression by hand and even write a program to do it if they know some computer programming.  And I think they can grasp intuitively why class notation is a conservative definitional extension of ZFC and does not really add new axioms.

Since you plan to add $j tags to identify the nature of $a statements, can't they be used to indicate that df-cleq, etc. are axioms for your verifier's technical purposes, rather than depend on the hard-coded informal prefixes "ax-" and "df-"?  Let the $js indicate what are to be considered axioms by machines and demanding logicians, and let the prefixes indicate how they should be interpreted informally by most people.

I think that's not a bad idea. You are right that if we have an alternate means of signaling to the computer, then we can let the name be what it's supposed to be - a mnemonic that assists in understanding the shape and role of the statement in context.

 

Another thing that seems wrong is that we would be at the mercy of the sophistication of the definition checking tools, with things possibly changing from ax- to df- over time depending on how the tools evolve.  This may send a message that the foundations are unstable and poorly defined.  Again, wouldn't $j tags be a more appropriate place for that?

One thing I should probably have said more explicitly is that a definitional schema is nothing more or less than an axiom schema (of a variety more complicated than the things metamath usually calls schema). Replacing a single axiom with an extension to the definition checker is basically trading one axiom for a whole bunch of axioms, and usually the latter will be much more complicated to verify. So for one-off "definition-like" axioms, it's probably not worth building a complicated axiom schema. Just like with theorems in set.mm, we want to know that a theorem "pays for itself" in terms of use. Most of the definitional schema implemented in mmj2 pays for itself, because it supports a large variety of definitions that stress most of the features. The justification theorem extension does not pay for itself, because it is only being used for df-tru (and I am also calling the extension itself into question). And all of the definitional extensions I proposed in the previous email would not currently pay for themselves, because there is only one or two uses of each of them. It's possible that in the future they will get more use, but I think the better practice is to build the unifying framework only after several examples already exist.

So while I think it is possible to extend more things into the definitional schema, it's much more light-weight to just have a few axioms instead, and judge them on a case by case basis.

And what of "conservativity"? My focus here has been on axioms that are "correct", i.e. true in any model of ZFC for an appropriate interpretation of all the "defined" symbols. This is actually sufficient to ensure conservativity over ZFC, since any axiom that is true in every model of ZFC is provable in ZFC and hence is conservative over it. So I am absolutely okay with $a |- T. because it's trivial to verify in a model of ZFC and it's also intuitively correct. There is no need for this to be an eliminable symbol or anything like that, although it's nice when we can obtain that.

 

We are talking about only 3 or 4 definitions that will never change and never be added to, that are almost universally agreed upon to be valid definitions, that have been justified extensively in the literature.  There is zero doubt among mathematicians that they are conservative and eliminable. I don't think it is hard for most technically-minded humans to see that intuitively.  In the end, when you get down to the reliability of the transistors in the machine that runs the definition checks, there is no such thing as absolute certainly.  At some point common sense is needed to delineate what is acceptable, and to me, the "df-" prefix on these 3 or 4 definitions is an acceptable risk.

How about adding some weasel words to the affected definitions? Such as: "This definition is technically an axiom, in that it does not satisfy the requirements for the definition checker. The proof of conservativity requires external justification that is beyond the scope of the set.mm axiomatization."

[fl]

How about adding some weasel words to the affected definitions? Such as: "This definition is technically an axiom, in that it does not satisfy the requirements for the definition checker. The proof of conservativity requires external justification that is beyond the scope of the set.mm axiomatization."

I propose to put expressly and extensively all the checks made by mmj2 in a page on the site. I believe (?) that there is no such thing. And to add details on why these checks do not affect the power of metamath (as for the prohibition of functions that call themselves.) 

[fl]

I also propose to put extensive textual description in commentaries to help the

non-mathematically-oriented minds (in this respect df-prds should be improved

for instance).

And also to add a link to a book that describes the concept. (The description in

the book and the formal definition must be rather straightforward. It's to help students,

not to confuse them. If you give them a link to a description with rather no link

to the formalization it is of no use.)

--

FL

[fl]

And also to vbe able to open définitions in mmj2.

The beautiful layout of the formulas designed by O'Cat complemented by the
colorization of variables realized by Mario Carneiro helps to read these

slightly esoteric formulas.

--

FL

[David A. Wheeler]

> Calling df-clab,cleq,clel "axioms" sends the wrong message...

Is there a way to prove that these are conservative definitions from within metamath? Possibly with an extension to metamath?

--- David A.Wheeler

[Benoit]

On Saturday, June 15, 2019 at 4:42:22 PM UTC+2, David A. Wheeler wrote:

On Sat, 15 Jun 2019 07:05:43 -0400, Mario Carneiro <di....@gmail.com> wrote:
> I would like to get away from label conventions in favor of something
> machine readable and not hardcoded.

I'm fine with adding additional mechanisms.
However, I'd like to keep using & enforcing the label conventions.
I find they're very helpful for the humans who are trying to read this stuff :-).
And once the humans start depending on the conventions, it's wise
to enforce the conventions so the fragile humans aren't misled.

Label conventions are also "machine readable". You can make them
not hardcoded by adding a mechanism to declare the label convention.

I also think that sticking as close as reasonably possible to label conventions makes it easier to humans (and this contributes to making metamath more attractive).

> The mechanism I propose is:
>
>   If an $a statement is given for a syntax typecode (i.e. not |-), then it
> is a definition iff the immediately following statement is a definitional
> axiom $a |- foo = ... which satisfies the usual rules. Otherwise, it is
> treated as an axiom, and a warning is issued if the label convention
> implies that the axiom would like to be treated as a definition and there
> is no warning-suppressing pragma attached to the axiom.

That's extremely strict.  Even though we don't use it in set.mm today,
I worry about being unable to escape it later.
I'd prefer that to be the *normal* case, but with a special statement
(say a $j) that means "it's a definition even though it's down here" statement.

Indeed, I think that one should allow exceptions documented with a $j statement.  I ran into a concrete example recently: I want to eventually define multiplication of extended complex numbers (~df-bj-mulc) from the beginning, but in the infinite case, it requires ~clog (through complex argument), which has to be defined much later.  But this does not prevent one to use multiplication in the finite case meanwhile.  Therefore, the whole thing would look like:
  clog $a class
  cmulc $a class
  df-mulc $a |-
  [many theorems]
  df-log $a |-
There are probably several cases already in set.mm (although they should be kept exceptional).

> > Some label changes I see (skimming through mmdefinitions.html) are:
> >   wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though df-bi
> > is a special case
> >   df-v --> df-vv (to match cvv and avoid collision with cv)
>

> The general rule has been to make constant names as short as possible [...]

I think conventions are good, even if it would increase the size of set.mm.

So I would support switching to "wDFNAME" everywhere.  We've already been
moving to increasingly keep our label names consistent with the "df-NAME"
definitions.  And while the constant names aren't usually
visible to the user, in your lean translation they *ARE* directly visible,
and they're also visible in the HTML showing definitions.

I also think that having the label df-xxx correspond to wxxx or cxxx is a good convention to stick to.  As David says, the compressed size of set.mm would not increase.

Side question: would you extend this rule to the $c-statements? i.e. have blocks
  $c smurf $.
  csmurf $a class smurf $.
  df-smurf $a smurf = ... $.
This would look more systematic.  As suggested above, maybe one could also standardize the comments, for example "Extend class notation to smurf / Syntax for smurf / Define smurf, the function that..." ?

Benoit

[Mario Carneiro]

To be more specific, by "warning-suppressing pragma" I mean a $j statement. Suppressing the "axiom treated as definition" warning on a particular definition has exactly the desired effect, of allowing definitions to "count" as definitions even if they don't meet any reasonable criterion for being one.

 

I ran into a concrete example recently: I want to eventually define multiplication of extended complex numbers (~df-bj-mulc) from the beginning, but in the infinite case, it requires ~clog (through complex argument), which has to be defined much later.  But this does not prevent one to use multiplication in the finite case meanwhile.  Therefore, the whole thing would look like:
  clog $a class
  cmulc $a class
  df-mulc $a |-
  [many theorems]
  df-log $a |-
There are probably several cases already in set.mm (although they should be kept exceptional).

This is not a legal definition, this is mutual recursion which is not allowed. If you tried this in set.mm today you would get an error because mmj2 would not allow df-log to reference mulc. You would be forced to have an intermediate definition for the finite multiplication operation, even if you never use it / immediately eliminate it after the trio of definitions.

Another example of this sort of thing is df-prds, which is a giant structure builder containing a number of slots that pertain to entire areas that haven't been introduced yet. We resolve this by actually moving the relevant definitions up, which is why df-topgen comes long before the first theorem that expands it, tgval.

If it passes mmj2 definition checker today, then it is possible to move the df-* to immediately after the constant declaration, without breaking anything, so I know in advance that my proposal will work - we've been checking for it all along.

 

> > Some label changes I see (skimming through mmdefinitions.html) are:
> >   wb --> wbi (and similarly for wo wa, w3o, w3a, wxo), even though df-bi
> > is a special case
> >   df-v --> df-vv (to match cvv and avoid collision with cv)
>
> The general rule has been to make constant names as short as possible [...]

I think conventions are good, even if it would increase the size of set.mm.

So I would support switching to "wDFNAME" everywhere.  We've already been
moving to increasingly keep our label names consistent with the "df-NAME"
definitions.  And while the constant names aren't usually
visible to the user, in your lean translation they *ARE* directly visible,
and they're also visible in the HTML showing definitions.

I also think that having the label df-xxx correspond to wxxx or cxxx is a good convention to stick to.  As David says, the compressed size of set.mm would not increase.

The size of set.mm would increase, because constant names appear in proof label lists. The compressed size (say with gzip) would probably only increase by a few bytes, but that's not the usual measure. I'm not going to commit to a position here, but that's at least been the historical justification for keeping the names minimal.

 

Side question: would you extend this rule to the $c-statements? i.e. have blocks
  $c smurf $.
  csmurf $a class smurf $.
  df-smurf $a smurf = ... $.
This would look more systematic.  As suggested above, maybe one could also standardize the comments, for example "Extend class notation to smurf / Syntax for smurf / Define smurf, the function that..." ?

While I am not proposing this as part of a rigorously checked rule, I'm fine if we do this. But unlike term/definition pairs, which have to come in pairs (because any new constant requires a definition), there is no one to one relationship between $c constants and new syntax axioms. $c declarations are more about presentation, the token alphabet from which the CFG is defined. A new term can reuse old constants, or introduce new ones, so there might be no new $c's with a term (for example df-mpt2), or there might be more than one (for example df-itg). Additionally, metamath allows $c declarations to be bundled into one declaration, which makes it more convenient to declare them all in a single block.

[Benoit]

This is not a legal definition, this is mutual recursion which is not allowed. If you tried this in set.mm today you would get an error because mmj2 would not allow df-log to reference mulc. You would be forced to have an intermediate definition for the finite multiplication operation, even if you never use it / immediately eliminate it after the trio of definitions.

Of course!  I had overlooked that.  I'll be using only the clause of the "if" that does not involve the future definition, but that's in the object language, and metamath can't know that.  So I'll need temporary definitions, like what is currently done in the construction of the number systems.  The question is then to which extent this is acceptable...  I'll come back when I have something more concrete to propose.

 

While I am not proposing this as part of a rigorously checked rule, I'm fine if we do this. But unlike term/definition pairs, which have to come in pairs (because any new constant requires a definition), there is no one to one relationship between $c constants and new syntax axioms. $c declarations are more about presentation, the token alphabet from which the CFG is defined. A new term can reuse old constants, or introduce new ones, so there might be no new $c's with a term (for example df-mpt2), or there might be more than one (for example df-itg). Additionally, metamath allows $c declarations to be bundled into one declaration, which makes it more convenient to declare them all in a single block.

You're right, there is no bijection, so the rule could be:

  $c the new symbols used in csmurf $.   (here, $c smurf }} $. )

  csmurf $a class smurf [ A }} $.

  df-smurf $a |- smurf [ A }} = ... $.

As for the reuse of symbols, like in df-mpt2, would it be good practice to require at least one symbol unique to each definition?  It could be useful for searching.  E.g. how do you single out occurrences of functions of two variables with the "MM> SEARCH" command (or even searching with ctrl+F in a text editor)?  I guess this is doable in mmj2 with regular expressions?  I've been a bit extreme in not overloading symbols, and defined couples of classes as (| A ,, B |) (see bj-c2uple), although the unicode symbol for ",," is "," so that the couple looks more normal on the webpage.

Benoit

[Alexander van der Vekens]

While working on Github issue #1457, I encountered a situation in set.mm which illustrates this topic. It is the definition of `gsum` (~df-gsum), which must be placed far before the related theorems because the symbol `gsum` is used in definition ~df-prds already.

And it is not sufficient to have the constant definitions "$c gsum $." and "cgsu $a class gsum $." earlier (for metamath.exe it is, for mmj2 it isn't: mmj2 would throw an error message like "Axiom df-gsum has failed the definitional soundness check. The previous axiom df-prds uses the symbol being defined in this axiom.").

And since ~df-gsum uses `0g`, its definitions (including ~df-0g) must occur even before ~df-gsum!

I think this is really awkward. There are two possible solutions:

• to allow a definition (~df-...) to be placed after the usage of the corresponding symbol (and before it is really used, of course). But I think this is exactly the opposite to what Mario proposes.
• to revise the definitions of ~df-prds, ~df-imas, etc. (but I do not know if this would be possible at all...)

Alexander

[Mario Carneiro]

I realize that it seems especially inconvenient that moving df-gsum back requires moving df-0g back too. But this better reflects the reality, because df-gsum not allowed to refer to constants defined after cgsum anyway (to prevent cycles), and placing df-gsum much further along just makes this policy more unintuitive (because normally we can refer to anything before the current line).

That said, I think it would still be better to move all definitions needed for df-prds before it. This is a downside of the "everything structure" approach, but it does not displace too many definitions. We can keep the real theorems about them (including the definitional theorem) in their proper place.

Mario

--
You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/533047c1-210c-4a5f-aad2-cfb291f2a58a%40googlegroups.com.

[Benoit]

On Thursday, February 13, 2020 at 5:46:36 PM UTC+1, Mario Carneiro wrote: 

That said, I think it would still be better to move all definitions needed for df-prds before it. This is a downside of the "everything structure" approach, but it does not displace too many definitions. We can keep the real theorems about them (including the definitional theorem) in their proper place.

So it looks like my reply there (https://github.com/metamath/set.mm/issues/1457#issuecomment-585716367) was unfortunately correct ?  What happens to df-prds (and also image structure, structure restriction, etc.) when we define new slots, for a sigma-algebra, a measure, a smooth atlas, a structure sheaf, etc. ?

Benoît

[Mario Carneiro]

Most of the definitions don't need to be moved up, only the "structural" ones that are required for actually defining the content of the new slot. df-gsum is unfortunate because it is a relatively complex definition that is also a dependency for the slot, but if you can write the slot without any auxiliaries then nothing has to move. (Another option is to unfold the definition in the content of df-prds, and then refold the definition when proving the slot theorem. But this would make df-prds even larger than it already is.)

Mario

--

You received this message because you are subscribed to the Google Groups "Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email to metamath+u...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3dd47cc0-64c1-4ec8-aeb2-31fbd99482fc%40googlegroups.com.