In § 1 we introduce our system and prove a theorem about its syntax. In § 2 we recall some stock results about the propositional calculus. In § 3 we consider a method of deriving an expression from a given expression and a real number. In § 4 we use this to derive a sequence of expressions from a given expression. In § 5 this sequence is shown to be just all the terms of a conjunctive normal form of the given expression. In § 6 we note that we may not need to produce all of these terms. In § 7 we describe a practical method (suitable for a binary digital electronic computer) which results from all this, and in § 8 we attempt to explain just why this is so.