[..] If I see a constant, how far forward do I need to scan to find out whether this is actually a definition? [..]
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?
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.
[..]
Norm
Concerning the circular definitions: are there any meaningful cases, or even already examples in set.mm?
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)
My first question is, how will it be checked? Can the mmj2 definition check be modified to ensure it?
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.
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.
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.
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.
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 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.
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 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.
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."
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.
> > 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 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..." ?
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.
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 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.
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.
--
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.