A system of natural deduction rules is proposed for an idealized form of English. The rules presuppose a sharp distinction between proper names and such expressions as 'the c', 'a (an) c', 'some c', 'any c', and 'every e', where 'c' represents a common noun. These latter expressions are called quantifiers, and other expressions of the form 'that c' or 'that c itself', are called quantified terms. Introduction and elimination rules are presented for any, every, some, a (an), and the, and also for any which, every which, and so on, as well as rules for some other concepts. One outcome of these rules is that 'Every man loves some woman' is implied by, but does not imply, 'Some woman is loved by every man', since the latter is taken to mean the same as 'Some woman is loved by all men'. Also, 'Jack knows which woman came' is implied by 'Some woman is known by Jack to have come', but not by 'Jack knows that some woman came'.
Natural deduction rules ordinarily are applied only in the case of artificial languages, but it is interesting to try to formulate such rules for English, or rather for an idealized form of English.
The rules for the sentential connectives and, or, it is false that, and if... then would of course be essentially the usual ones. Let 'p', 'q', 'r' stand for arbitrary sentences. Let 'Np' stand for 'it is false that p', and let 'p=q' stand for 'ifp then q'. (Single quotes are being used to refer to the expressions written between them, except that metavariables between single quotes are to be replaced by instances of expressions that they stand for. Such replacement, however, of course would not occur in sentences in which the metavariables themselves are first introduced or in which the context indicates that the metavariables are themselves being referred to.) The rules for the above connectives could be chosen as follows, using proof methods like those of my book, Symbolic Logic (Ronald Press, 1952):
Rule of indirect proof: 'p' is a d.c. (direct consequence) of a proof having hypothesis ',-~p' (as its only hypothesis) and having contradictory steps 'q' and ',-~q'. (All the usual rules for negation are known to be derivable from this rule.)