Misleading definitions

[Benoit]

In the previous thread "other definitions of well-foundedness" (which was "hijacked" to a totally different topic), I made the remark:

> the current df-fr does not define well-founded relations, but well-founded "things"; one should add the condition R \subseteq A \times A.  

to which Mario replied:

> the fact that df-fr only discusses well-founded "things" is deliberate; frinxp expresses exactly how it restricts to relations on the proper base set.

The problem is that the description at http://us2.metamath.org/mpeuni/df-fr.html says "Define the well-founded relation predicate".  This is not a faithful description.  It should say something like "Define the well-founded thing predicate", or more precisely, "Define the well-founded thing predicate, a notion specific to metamath and not encountered anywhere else in the mathematics literature". ;-)

More seriously, you say this is deliberate, so it might have some advantages?  The idea is that anything outside of A \times A is irrelevant, so it could be anything and there is one less hypothesis to check in later proofs, is it correct?  Are these advantages really worth deviating that much from the usual mathematical practice and meaning?  In several of his surveys of proof formalization, Freek Wiedijk writes that one of the reasons proof assistants/verifiers are not widely adopted is because they are too far from mathematical practice, and therefore, one of the goals they should have is getting closer to mathematical practice.

I briefly looked at mmdefinitions.html, and some other examples of misleading definitions are: df-po, df-so, df-se, df-we.

Benoît

[Norman Megill]

On Monday, October 22, 2018 at 7:05:42 AM UTC-4, Benoit wrote:

In the previous thread "other definitions of well-foundedness" (which was "hijacked" to a totally different topic), I made the remark:

> the current df-fr does not define well-founded relations, but well-founded "things"; one should add the condition R \subseteq A \times A.  

to which Mario replied:

> the fact that df-fr only discusses well-founded "things" is deliberate; frinxp expresses exactly how it restricts to relations on the proper base set.

The problem is that the description at http://us2.metamath.org/mpeuni/df-fr.html says "Define the well-founded relation predicate".  This is not a faithful description.  It should say something like "Define the well-founded thing predicate", or more precisely, "Define the well-founded thing predicate, a notion specific to metamath and not encountered anywhere else in the mathematics literature". ;-)

The definition is exactly, symbol for symbol, the one on Takeuti and Zaring p. 30 (2nd edition).  Their English description reads, "We read F Fr A as "F is a founded relation on A.""  Their development is much more formal than most, so I doubt they are assuming an implicit conjoined "Rel F", and their later proofs (most of them reproduced in set.mm) don't require this.  I figured it was just an informal manner of speaking, like we say "(F ` A)" is "function value", even though neither F nor A have any restrictions (including in T&Z's version).  It would certainly be inconvenient and make many proofs much longer if we had to prove that F is a function and A is in its domain before we are allowed to write down "(F ` A)".

As for whether there are uses for F Fr A when F is not a relation, I don't know.

Similarly for the other ones you mention.

Norm

[Benoit]

The definition is exactly, symbol for symbol, the one on Takeuti and Zaring p. 30 (2nd edition).  Their English description reads, "We read F Fr A as "F is a founded relation on A.""  Their development is much more formal than most, so I doubt they are assuming an implicit conjoined "Rel F", and their later proofs (most of them reproduced in set.mm) don't require this.  I figured it was just an informal manner of speaking, like we say "(F ` A)" is "function value", even though neither F nor A have any restrictions (including in T&Z's version).  It would certainly be inconvenient and make many proofs much longer if we had to prove that F is a function and A is in its domain before we are allowed to write down "(F ` A)".

So in TZ's conventions, a well-founded relation need not be a relation?  This is not impossible, by the "red herring principle", and this is not very important, since with any well-founded thing R on A one can naturally associate the well-founded relation R \cap (A \times A) on A, and this construction preserves and reflects well-foundedness, by ~frinxp, as Mario pointed out.  This is only a small deviation from the usual meaning, but I'm simply afraid that the accumulation of many of these small deviations could make it hard to translate back and forth between a formal statement and its informal translation, in the long run.

So I withdraw my "not encountered anywhere else in the mathematics literature", but the other remarks/questions remain.  Namely, is the simplification offered by this definition worth the deviation from the usual meaning (especially in regard to Wiedijk's opinion that proof assistants/checkers should aim to be closer to mathematical practice)?  And more generally, where to put the cursor between ease of formalizing and proximity to human mathematics? Note, by the way, that adding to ~df-fr the condition R \subseteq A \times A would allow, for instance, to remove the antecedent from ~frsn (I happened to see this because it was three theorems below ~frinxp, but there may be many other cases of simplification or complexification, and I don't know which would take over).

As for "( F ` A )", it will not be a surprise to you that I had indeed thought of adding these $e-hypotheses to df-fv !

Benoît

[Scott Fenton]

It's also worth noting that "standard mathematical practice" would easily say that less than is a founded relationship on the naturals, but we don't have "< C_ ( NN X. NN )". I'd argue that allowing arbitrary "out of bounds" behavior makes sense in the context of matching to informal practice.

-Scott

--
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 post to this group, send email to meta...@googlegroups.com.
Visit this group at https://groups.google.com/group/metamath.
For more options, visit https://groups.google.com/d/optout.

[Norman Megill]

It probably isn't worthwhile to change the definition (by conjoining Rel F) since it affects many proofs, but I would have no objection to changing the comment wording to something like "well-founded class" with a remark that F is normally a relation.
 

As for "( F ` A )", it will not be a surprise to you that I had indeed thought of adding these $e-hypotheses to df-fv !

Of course.  You would also probably be interested in  Alexander's df-afv, which returns (F ` A)= _V (i.e. not a set) for undefined values.  While there is a certain elegance to this, it would mean that ~ opex would no longer hold, and in its place we would have to prove that F is a function and A is in its domain for almost 2000 theorems that use opex to simplify things (sometimes quite significantly), so many proofs would be much longer.

We make certain compromises to make life easier for us, especially in earlier set theory. There is nothing mathematically wrong with df-fv as long as we stick to that definition throughout (as Metamath forces you to).  We also use things like "(0o i^i 1o) = 0o" when convenient for finite ordinals, even though as "numbers" that would be nonsense.

The link Mario gave about ZFC and math, https://mathoverflow.net/a/90945/34444, is actually called "Set theories without “junk” theorems?" and discusses this very issue.

If you want a kind of purity that doesn't permit such "junk theorems", I think our extensible structure builders come close by letting you define a class of objects with exactly and only the properties you want.  For example, a specific group may have many "junk theorems" due to accidental properties its members may have, but you can't prove anything about an arbitrary member of Grp that doesn't hold for all other members.

Norm

[Benoit]

I propose adding, as a second paragraph to the comment of df-fr, the following:

Note that this definition does not require that R be a binary relation on A (that is, be included in A x. A).  This is inessential since out-of-domain behavior is irrelevant regarding well-foundedness (see ~frinxp).

And similarly with df-po and df-se (linking to poinxp and seinxp), but I plan to leave unchanged df-so and df-we (since they mention the former).  I'll do a pull request soon, unless your prefer another solution/wording.

The link Mario gave about ZFC and math, https://mathoverflow.net/a/90945/34444, is actually called "Set theories without “junk” theorems?" and discusses this very issue.

Yes, I remember we had a similar discussion in https://groups.google.com/d/msg/metamath/GQmelsKtaWQ/a4sq4PfXFQAJ where I linked to that mathoverflow discussion.  There is clearly a question about balancing ease of the formalization versus proximity with usual mathematical practice, and there is not a single answer, but different answers in each different case.  As I wrote above, some (like Wiedijk) view the lack of proximity with mathematical practice as a hurdle to a wider adoption by mathematicians of formal tools.  (This does not mean I advocate any changes: I don't have enough experience with formalization to ponder the pros and cons.)

Benoît

[Mario Carneiro]

I think that statement makes it sound like out of domain behavior doesn't matter, like we could swap out the definition for one that has different behavior out of domain without breaking any theorems. This is false; frinxp says *exactly* how the predicate behaves out of domain. I should have mentioned this earlier, but one place where it is used essentially is in statements like E. Fr A - we want this to mean that the epsilon relation *restricted to A* is well founded on A. If Fr required that its left argument be a relation with domain the right argument, then we would not need the right argument at all, since it's derivable from the relation itself (well, except in some edge cases), but we also would have to write (E. i^i (A X. A)) Fr A instead.

--

[Mario Carneiro]

One analogy is to the restricted existential (or universal) quantifier E. x e. A ph. If we view ph(x) as a predicate on the universe, then it only "matters" what it says about elements of A; but that doesn't mean that the definition of the restricted quantifier could do something else out of this domain - it is *required* to ignore anything outside A. This allows for theorems like A. x e. A ( ph <-> ps ) -> ( E. x e. A ph <-> E. x e. A ps ). The order predicates are all restricted quantifications in this sense.

[Benoit]

So what do you propose ? Is the following ok ?

Note that this definition does not require that R be a binary relation on A (that is, be included in A x. A).  It only requires that the restriction of R to A x. A be a well-founded relation (see ~frinxp).