ABSTRACT
Deductions in a pure modus ponens calculus cp w ill, unless they consist of an axiom alone, always make use of formulas containing the connective ->. Let H be a subset of the set of propositional connectives —> , A ,V , n ; cp will be called separated w ith respect to the connectives in H if the following holds: if M h v can be deduced in cp and if M, v contain only connectives from H then a cp-deduction of M h v can be constructed which uses only formulas containing -» and the connectives from H . It follows from Theorem 2g that eg is separated for each of the subsets of {"^,A,v} . Because a cgdeduction S of M h v can first be transformed into a K P -d erivation S* which, by the subformula principle, uses only formulas containing the connectives from H. It then follows from the constructions, performed in the proofs of Theorem 2d and its extensions, that the cp-deduction of M h v formed from S* uses formulas which, apart from -*, contain only connectives from H . -1In SCHMIDT 60 , § 117, it is shown that ce is separated for { —>,A} without making use of the correspondence between deductions and derivations.
