Our method is based on the same principles which we have assumed in a paper about the foundations of metamathematics which we published in collaboration with J. Herzberg some years ago. Nevertheless we have introduced some important modifications which enable us to use a very restricted preliminary language and to avoid any artificial construction.

The problem of a restricted language in mathematics appears to be a very important one, as our ordinary language is really ambiguous and obscure. On the other hand there is the problem of restricting the intuitive logic to be used in our construction. We shall see that for this purpose we need only substitutions and modus ponens.

If we avoided any abbreviation, we could reduce our preliminary language to propositions of the following forms:

X is a theorem.

If P, then Q.

But we have to do with very long symbolic expressions and as there is not yet any machine to build up such expressions we must use abbreviations. For this purpose we shall use propositions of the following forms in the preliminary language:

X is an expression.

X is an abbreviation of Y.

Any proposition which does not belong to one of our four forms will be excluded from our construction.

The completeness of the prepositional calculus was first proved by Post. His somewhat condensed proof has been succeeded by more detailed presentations of substantially the same argument, and also by several proofs of radically different forms. The present paper contains still another proof, offered because of its relative simplicity. In part this proof follows a plan which was sketched by Wajsberg for another purpose, viz. for proving the completeness of the sub-calculus involving only the material conditional.

For the present proof a systematization of the propositional calculus will be used which is due to Tarski, Bernays, and Wajsberg. It involves the material conditional “⊃” and the falsehood “F” as primitive; thus the formulae are recursively describable as comprising “F”, the variables “p”, “q”, “r”, …, and all results of putting formulae for “p” and “q” in “(p⊃q)”. The denial “˜p” is definable as “(p⊃F)”, and all other truth functions are then definable in familiar fashion. (Conversely, in a system admitting “˜” instead of “F” as primitive, “F” might be explained as an abbreviation of “˜(P⊃P)”.) The postulates are four:

(1) ((p⊃q)⊃((q⊃r)⊃ (p⊃ r)))

(2) (((p⊃(q⊃p)⊃p)

(3) (p⊃(q⊃p))

(4) (F⊃p).