Stahl’s opposite system SP (originally called “top”) is the Hilbert- style propositional logic deriving all the well-formed formulas of which the negation is provable in classical propositional logic [{\it G. Stahl}, An opposite and an expanded system, Z. Math. Logik Grundlagen Math. 4, 244-247 (1958; Zbl 0201.005)]. It is a surprising fact that SP does not use the usual provability relation. The author reconsidered the system from a proof-theoretical point of view. As the result of reconsideration, he showed that Stahl’s simple, but ingenious and rather less intelligible idea used for the formulation of SP is in fact well correct and further applicable to the case of classical predicate logic, by giving Gentzen-style sequent calculi OP and OC corresponding to the Hilbert-style opposite systems SP and SC, respectively. This result is one of the very answers to Stahl’s suggestion in his paper cited above.
Reviewer: T.Inuoué