Re: [Metamath] Question abouot indistopon

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

Re: [Metamath] Question abouot indistopon

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

Re: [Metamath] Question abouot indistopon

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

Re: [Metamath] Question abouot indistopon

> 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

Re: [Metamath] Question abouot indistopon

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

[Metamath] Question abouot indistopon

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