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 <di.g...@gmail.com> 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 <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? > > > > -- > > 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.
