Re: [Metamath] Question abouot indistopon

[Mario Carneiro]

It's not my invention, although I'm not sure it's been used in this exact
situation before. Negative and positive position is a notion in proof
theory relating to whether a certain construct is covariant or
contravariant with respect to increasing in the ordering of propositions
(i.e. "more true"). So for example in the expression "P -> Q", P is in
negative position and Q is in positive position, because implication is
covariant on the right, i.e. if Q -> Q' then (P -> Q) -> (P -> Q'), but
contravariant on the left, because if P -> P' then (P' -> Q) -> (P -> Q).
In general the polarity flips every time you nest in another "negative
position", so in (P -> Q) -> R, P and R are in positive position and Q is
in negative position.

On Thu, May 2, 2024 at 2:04 AM 'B. Wilson' via Metamath <
metamath@googlegroups.com> wrote:

> Thank you for the pointer, Mario. Is this negative vs. positive position
> terminology something you neologized on the fly? Or does it have
> precedent? If
> I'm grokking you correctly, the positive positions plug into the negative
> positions, which jibes with your explanation and the Is-a-set convention
> you
> reference.
>
> Thanks for the clarity.
>
>
> Mario Carneiro  wrote:
> > There is a convention, which is to use "( A e. V -> ..." in antecedents
> to
> > theorems and deduction-form statements and |- A e. _V in inference-form
> > theorems. In "positive position", you often need to use A e. _V, i.e. in
> > fvex there is no other reasonable option for what set to say that
> function
> > value is a member of without any assumptions. In "negative position",
> it's
> > a question of whether to spend one extra elex step in some cases (e.g. 2
> e.
> > RR therefore 2 e. _V therefore I can apply this lemma about sets to 2),
> or
> > one extra syntax step to instantiate the V argument (which also takes
> some
> > space in proofs). I believe the above convention is derived from some
> > analysis along these lines, but it's also somewhat historical (it's more
> > important to have a consistent convention). See the "Is-a-set." section
> of
> > https://us.metamath.org/mpeuni/conventions.html for more information.
> >
> > On Wed, Apr 24, 2024 at 3:52 AM heiphohmia via Metamath <
> > metamath@googlegroups.com> wrote:
> >
> > > > It functions much like A e. _V would. A proof using this theorem can
> > > always
> > > > plug in _V for V but it also could plug in On, RR, or whatever is
> > > convenient.
> > > > Perhaps looking at  makes
> it
> > > clear.
> > >
> > > Okay, elements of ZF classes are always sets, so A e. V restricts A
> from
> > > being
> > > proper classes. That begs the question why one would ever use A e. _V
> > > though.
> > > Is this just a case where there's no particular convention?
> > >
> > > --
> > > 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+unsubscr...@googlegroups.com.
> > > To view this discussion on the web visit
> > >
> https://groups.google.com/d/msgid/metamath/272R9VKF3UZLE.34NMDVUCB3A1P%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 metamath+unsubscr...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/2VC9HKX4Q39T0.1ZIJO4RNZ5BIT%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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/CAFXXJStzbKu4QCWU984ynXRBOQdNVRmRCQd7Udp6CM3cZAJ02g%40mail.gmail.com.

Re: [Metamath] Mnemonic of Fr

[heiphohmia via Metamath]

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 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  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 <
> metamath@googlegroups.com> 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 metamath+unsubscr...@googlegroups.com.
> > 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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/3DPYLIRK0IUR9.2R4PQFMFJN5VC%40wilsonb.com.

Re: [Metamath] Question abouot indistopon

['B. Wilson' via Metamath]

Thank you for the pointer, Mario. Is this negative vs. positive position
terminology something you neologized on the fly? Or does it have precedent? If
I'm grokking you correctly, the positive positions plug into the negative
positions, which jibes with your explanation and the Is-a-set convention you
reference.

Thanks for the clarity.


Mario Carneiro  wrote:
> There is a convention, which is to use "( A e. V -> ..." in antecedents to
> theorems and deduction-form statements and |- A e. _V in inference-form
> theorems. In "positive position", you often need to use A e. _V, i.e. in
> fvex there is no other reasonable option for what set to say that function
> value is a member of without any assumptions. In "negative position", it's
> a question of whether to spend one extra elex step in some cases (e.g. 2 e.
> RR therefore 2 e. _V therefore I can apply this lemma about sets to 2), or
> one extra syntax step to instantiate the V argument (which also takes some
> space in proofs). I believe the above convention is derived from some
> analysis along these lines, but it's also somewhat historical (it's more
> important to have a consistent convention). See the "Is-a-set." section of
> https://us.metamath.org/mpeuni/conventions.html for more information.
> 
> On Wed, Apr 24, 2024 at 3:52 AM heiphohmia via Metamath <
> metamath@googlegroups.com> wrote:
> 
> > > It functions much like A e. _V would. A proof using this theorem can
> > always
> > > plug in _V for V but it also could plug in On, RR, or whatever is
> > convenient.
> > > Perhaps looking at  makes it
> > clear.
> >
> > Okay, elements of ZF classes are always sets, so A e. V restricts A from
> > being
> > proper classes. That begs the question why one would ever use A e. _V
> > though.
> > Is this just a case where there's no particular convention?
> >
> > --
> > 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+unsubscr...@googlegroups.com.
> > To view this discussion on the web visit
> > https://groups.google.com/d/msgid/metamath/272R9VKF3UZLE.34NMDVUCB3A1P%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 metamath+unsubscr...@googlegroups.com.
To view this discussion on the web visit 
https://groups.google.com/d/msgid/metamath/2VC9HKX4Q39T0.1ZIJO4RNZ5BIT%40wilsonb.com.