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
My guess was "(well-)founded relation" as well, but Takeuti and Zaring are
saying "foundational relation" in description of the 6.21 definition for Fr. If
the Fr syntax is riffing off T anyway, I think it'd be an epsilon improvement
to mention where the mnemonic comes from in the comment.
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
