Mnemonic of Fr

[B. Wilson]

This has been bugging me midly for a while, but I couldn't figure out what the
Fr symbol in df-fr stood for:

19201 df-fr $a |- ( R Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z R y ) ) $.

I finally bothered to look up the Takeuti and Zaring reference, which also uses
"Fr" and calls R a "foundational relation". It's not super important, but would
it be worth mentioning this in df-fr's comment?

Cheers,
B. Wilson

[Mario Carneiro]

My understanding is that it stands for "founded relation", as in well-founded but without the "well", I think because it doesn't have any other ordering properties like being a partial order attached to it.

--
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/2F5KIFFJJY2KH.28Z6N87TP90O2%40wilsonb.com.

[heiph...@wilsonb.com]

My guess was "(well-)founded relation" as well, but Takeuti and Zaring are
saying "foundational relation" in description of the 6.21 definition for Fr. If
the Fr syntax is riffing off T&K anyway, I think it'd be an epsilon improvement
to mention where the mnemonic comes from in the comment. Something like the
below?

Define the well-founded (a.k.a. foundational) relation predicate...

[Alexander van der Vekens]

Are we talking about the same edition of the book? In my (very old) paper copies, definitions 6.21 and 6.24 are on page 27...

Nevertheless, if the numbering of the definitions is still the same, definition 6.21 defines a "foundational relation" (`R Fr A`) , whereas definition 6.24 1) defines a "well founded relation" (`R Wfr A`). The difference between both is that the second adds an "is a set" property (on each R-initial segment of A): ``R Wfr A <-> ( R Fr A /\ A. x e. A ( A i^i  ( `'R  " { x } ) ) e. _V )`.

In set.mm, ~dffr3 is an alternate definition of ~df-fr which corresponds exactly to definition 6.21 in Takeuti/Zaring (as indicated in the comment).

Furthermore, we have a set-like predicate `R Se A` in set.mm (see ~df-se - there isn't such a predicate in Takeuti/Zaring!?), which exactly represents the  "is a set" property mentioned above.

So if we want to define a well founded relation as in def. 6.24 1) in Takeuti/Zaring, then this would be

 `df-wfr $a |- ( R Wfr A <-> ( R Fr A /\ R Se A ) ) $.`

We use this definition implicitly, for example in ~tz6.26, where the `R Wfwe A` in Takeuti/Zaring is represented by `( R We A /\ R Se A )`.

Under the assumption that the definitions in my copy (maybe "first edition") and the edition used in set.mm ("second edition") are the same, we actually have to replace "well-founded" by "foundational" in many places, at least it should be mentioned in the comment of ~df-fr that there is a deviation in terminology, as proposed by B. Wilson.

It would be great if my observations can be approved by somebody who has access to the edition of Takeuti/Zaring which is referenced in set.mm.

[Alexander van der Vekens]

The definition ~df-fr in set.mm corresponds exactly to the definition in Wikipedia (https://en.wikipedia.org/wiki/Well-founded_relation), and here the terms  well-founded or wellfounded or foundational are used synonymously, with the side note "Some authors include an extra condition that R is set-like, i.e., that the elements less than any given element form a set.".