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