The system \(LD\) is one of the systems introduced by the author in his “A theory of formal deducibility” [Notre Dame Math. Lectures. Vol. 6. Indiana: Notre Dame (1950; Zbl 0041.34807)]. It is substantially the minimal calculus with excluded middle first considered by I. Johannsson [Compos. Math. 4, 119–136 (1936; Zbl 0015.24102)] and in a sense is the natural system of strict implication, having the property that every proposition is either a theorem or is refutable. The present paper gives details of certain results concerning the system which have been reported in the Proc. Int. Congress of Mathematicians, Cambridge, Mass., USA Aug. 30 – Sept. 6th, 1950.
The author proves that if \(\mathfrak X\), \(\mathfrak Y\), \(A\) are positive (i. e. formed wholly without negation) and if \(\mathfrak X\), \(\neg\, \mathfrak Y|\!\!\vdash A\) in \(LD^*\); then \(\mathfrak X|\!\!\vdash A\) in \(LA^*\). Here \(LA\) is the intuitionist positive system and \(LA^*\), \(LD^*\) are the systems formed from \(LA\), \(LD\) by adjoining quantifiers. He then proves that if \(\mathfrak X|\!\!\vdash A\) holds in \(LD\) then \(\mathfrak X\neg A|\!\!\vdash A\) holds in \(LM\) (the minimal system for refutability); if \(\mathfrak X|\!\!\vdash\) (i. e. if \(\mathfrak X\) is refutable) holds in \(LD\) then it holds in \(LM\) also.
After deducing corollaries from these theorems he considers various other formulations for \(LD\) designed to overcome the objection that one of the rules of \(LD\) in its original formulation allows the elimination of a constituent of higher order than the one which is left. But it turns out that in none of these alternative systems does the elimination theorem hold. Finally he suggests that even in the classical systems \(LC\), \(LK\) it might be better to avoid the use of more than one proposition on the right of the entailment sign \(|\vdash\) and he indicates how this can be done.