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] 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.

Re: [Metamath] Question abouot indistopon

[Mario Carneiro]

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/CAFXXJSsZM-syOfP_R0EaEZrghkTYH1Ci349FFdvUzauXoE7iPg%40mail.gmail.com.

Re: [Metamath] Question abouot indistopon

[heiphohmia via Metamath]

> 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.

Re: [Metamath] Question abouot indistopon

[Jim Kingdon]

On April 22, 2024 11:20:58 PM PDT, "'B. Wilson' via Metamath" 
 wrote:

>It looks suspiciously close to A e. _V which reas as "A is a set", but in this
>case the V is just floating. What are the semantics here?
>

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.

-- 
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/1AFA2722-4909-42DA-BCAF-CB0A15A882BD%40panix.com.

[Metamath] Question abouot indistopon

['B. Wilson' via Metamath]

The A e. V antecedent is confusing me. Might I ask for a quick pointer?

85195 indistopon $p |- ( A e. V -> { (/) , A } e. ( TopOn ` A ) ) $= ... $.

It looks suspiciously close to A e. _V which reas as "A is a set", but in this
case the V is just floating. What are the semantics here?

-- 
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/3UBII6CP7S76N.3E59KU168XFGI%40wilsonb.com.