Question abouot indistopon

[B. Wilson]

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?

[Jim Kingdon]

On April 22, 2024 11:20:58 PM PDT, "'B. Wilson' via Metamath" <meta...@googlegroups.com> 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 <https://us.metamath.org/mpeuni/elex.html> makes it clear.

[heiph...@wilsonb.com]

> 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 <https://us.metamath.org/mpeuni/elex.html> 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?

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

--
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/272R9VKF3UZLE.34NMDVUCB3A1P%40wilsonb.com.

[B. Wilson]

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]

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.

To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/2VC9HKX4Q39T0.1ZIJO4RNZ5BIT%40wilsonb.com.