I need help in understanding a device used bu Kurt Schütte, Proof Theory (1977).
In treating classical sentential calculus, he use - in place of truth-tables - the device of positive- and negative-forms [page 10-on], called "a sort of generalization of the notions of 2succedents and antecedents formulas' of Gentzen's sequence calculus".
The idea is that $A$ is a positive (negative) part of $F$ if it occurs in $F$ in such a way that the truth of $A$ (falsity of $A$) implies the truth of $F$.
The simplest example is given by $F = (A_1 \land ... \land A_n \rightarrow B_1 \lor ... \lor B_m)$ where each $A_i$ is a negative part of $F$ and each $B_j$ a positive part; similarly for $F = (\lnot A_1 \lor ... \lor \lnot A_n \lor B_1 \lor ... \lor B_m)$. The syntactic definition of these notions is given in terms of $P$-forms $\mathcal P[*]$ and $N$-forms $\mathcal N[*]$ so that $A$ is a positive part of $F$ if $F = \mathcal P[A]$ for a $P$-form $\mathcal P$ (similarly for negative parts and $N$-forms). It is also necessary for setting up the logical systems to consider $NP$-forms $\mathcal Q[*_1,*_2]$ which are $\mathcal N$-forms in $*_1$ and $\mathcal P$-forms in $*_2$.
Are there available some source explaining the "machinery" and supplying details about how they are used in Schütte's book for to proof the soundeness and completeness of classical propositional logic ?
There are some remarks about positively (negatively) occurring subformulas in Sam Buss' An Introduction to Proof Theory, an article from the Handbook of Proof Theory. The article is available online:
http://www.math.ucsd.edu/~sbuss/ResearchWeb/handbookI/ChapterI.pdf
and the remarks start in section 1.2.10. However, this section is rather a prelude to some syntactic results and so may not be what you are looking for.