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.
[email protected] schrieb am Donnerstag, 2. Mai 2024 um 08:13:47 UTC+2:
> 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...
>
> Mario Carneiro <[email protected]> wrote:
> > 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.
> >
> > On Wed, May 1, 2024 at 5:21 AM 'B. Wilson' via Metamath <
> > [email protected]> wrote:
> >
> > > 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
> > >
> > > --
> > > 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 [email protected].
> > > To view this discussion on the web visit
> > >
> https://groups.google.com/d/msgid/metamath/2F5KIFFJJY2KH.28Z6N87TP90O2%40wilsonb.com
> > > .
> > >
>
>
>
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/dfbb8e29-3f78-4e20-b617-1b6acfe6b399n%40googlegroups.com.
