SECTION A. The Theory of Deduction. The purpose of the present section is to set forth the first stage of the deduction of pure mathematics from its logical foundations. This first stage is necessarily concerned with deduction itself, i.e. with the principles by which conclusions are inferred from premisses. If it is our purpose to make all our assumptions explicit, and to effect the deduction of all our other propositions from these assumptions, it is obvious that the first assumptions we need are those that are required to make deduction possible. Symbolic logic is often regarded as consisting of two coordinate parts, the theory of classes and the theory of propositions. But from our point of view these two parts are not coordinate; for in the theory of classes we deduce one proposition from another by means of principles belonging to the theory of propositions, whereas in the theory of propositions we nowhere require the theory of classes. Hence, in a deductive system, the theory of propositions necessarily precedes the theory of classes.
But the subject to be treated in what follows is not quite properly described as the theory of propositions. It is in fact the theory of how one proposition can be inferred from another. Now in order that one proposition may be inferred from another, it is necessary that the two should have that relation which makes the one a consequence of the other. When a proposition π {\displaystyle \scriptstyle {q}} is a consequence of a proposition π {\displaystyle \scriptstyle {p}}, we say that π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}}. Thus deduction depends upon the relation of implication, and every deductive system must contain among its premisses as many of the properties of implication as are necessary to legitimate the ordinary procedure of deduction. In the present section, certain propositions will be stated as premisses, and it will be shown that they are sufficient for all common forms of inference. It will not be shown that they are all necessary, and it is possible that the number of them might be diminished. All that is affirmed concerning the premisses is (1) that they are true, (2) that they are sufficient for the theory of deduction, (3) that we do not know how to diminish their number. But with regard to (2), there must always be some element of doubt, since it is hard to be sure that one never uses some principle unconsciously. The habit of being rigidly guided by formal symbolic rules is a safeguard against unconscious assumptions; but even this safeguard is not always adequate.
*1. Primitive Ideas and Propositions. Since all definitions of terms are effected by means of other terms, every system of definitions which is not circular must start from a certain apparatus of undefined terms. It is to some extent optional what ideas we take as undefined in mathematics; the motives guiding our choice will be (1) to make the number of undefined ideas as small as possible, (2) as between two systems in which the number is equal, to choose the one which seems the simpler and easier. We know no way of proving that such and such a system of undefined ideas contains as few as will give such and such results[1]. Hence we can only say that such and such ideas are undefined in such and such a system, not that they are indefinable. Following Peano, we shall call the undefined ideas and the undemonstrated propositions primitive ideas and primitive propositions respectively. The primitive ideas are explained by means of descriptions intended to point out to the reader what is meant; but the explanations do not constitute definitions, because they really involve the ideas they explain.
In the present number, we shall first enumerate the primitive ideas required in this section; then we shall define implication; and then we shall enunciate the primitive propositions required in this section. Every definition or proposition in the work has a number, for purposes of reference. Following Peano, we use numbers having a decimal as well as an integral part, in order to be able to insert new propositions between any two. A change in the integral part of the number will be used to correspond to a new chapter. Definitions will generally have numbers whose decimal part is less than Β·1, and will be usually put at the beginning of chapters. In references, the integral parts of the numbers of propositions will be distinguished by being preceded by a star; thus "1Β·01" will mean the definition or proposition so numbered, and "1" will mean the chapter in which propositions have numbers whose integral part is 1, i.e. the present chapter. Chapters will generally be called "numbers."
Primitive Ideas.
(1) Elementary propositions. By an "elementary" proposition we mean one which does not involve any variables, or, in other language, one which does not involve such words as "all," "some," "the" or equivalents for such words. A proposition such as "this is red," where "this" is something given in sensation, will be elementary. Any combination of given elementary propositions by means of negation, disjunction or conjunction (see below) will be elementary. In the primitive propositions of the present number, and therefore in the deductions from these primitive propositions in 2β5, the letters π {\displaystyle \scriptstyle {p}}, π {\displaystyle \scriptstyle {q}}, π {\displaystyle \scriptstyle {r}}, π {\displaystyle \scriptstyle {s}} will be used to denote elementary propositions.
(2) Elementary propositional functions. By an "elementary propositional function" we shall mean an expression containing an undetermined constituent, i.e. a variable, or several such constituents, and such that, when the undetermined constituent or constituents are determined, i.e. when values are assigned to the variable or variables, the resulting value of the expression in question is an elementary proposition. Thus if π {\displaystyle \scriptstyle {p}} is an undetermined elementary proposition, "not- π {\displaystyle \scriptstyle {p}}" is an elementary propositional function.
We shall show in 9 how to extend the results of this and the following numbers (1β*5) to propositions which are not elementary.
(3) Assertion. Any proposition may be either asserted or merely considered. If I say "Caesar died," I assert the proposition "Caesar died," if I say "'Caesar died' is a proposition," I make a different assertion, and "Caesar died" is no longer asserted, but merely considered. Similarly in a hypothetical proposition, e.g. "if
π {\displaystyle \scriptstyle {a=b}}, then
π {\displaystyle \scriptstyle {b=a}}," we have two unasserted propositions, namely "
π {\displaystyle \scriptstyle {a=b}}" and "
π {\displaystyle \scriptstyle {b=a}}," while what is asserted is that the first of these implies the second. In language, we indicate when a proposition is merely considered by "if so-and-so" or "that so-and-so" or merely by inverted commas. In symbols, if π {\displaystyle \scriptstyle {p}} is a proposition, π {\displaystyle \scriptstyle {p}} by itself will stand for the unasserted proposition, while the asserted proposition will be designated by " β’ . π {\displaystyle \scriptstyle {\vdash .p}}."
The sign " β’{\displaystyle \scriptstyle {\vdash }}" is called the assertion-sign[2]; it may be read "it is true that" (although philosophically this is not exactly what it means). The dots after the assertion-sign indicate its range; that is to say, everything following is asserted until we reach either an equal number of dots preceding a sign of implication or the end of the sentence. Thus " β’: π . β . π {\displaystyle \scriptstyle {\vdash :p.\supset .q}}" means "it is true that π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}}," whereas " β’ . π . ββ’ . π {\displaystyle \scriptstyle {\vdash .p.\supset \vdash .q}}" means " π {\displaystyle \scriptstyle {p}} is true; therefore π {\displaystyle \scriptstyle {q}} is true[3]." The first of these does not necessarily involve the truth either of π {\displaystyle \scriptstyle {p}} or of π {\displaystyle \scriptstyle {q}}, while the second involves the truth of both. (4) Assertion of a propositional function. Besides the assertion of definite propositions, we need what we shall call "assertion of a propositional function." The general notion of asserting any propositional function is not used until *9, but we use at once the notion of asserting various special elementary propositional functions. Let π π₯ {\displaystyle \scriptstyle {\phi x}} be a propositional function whose argument is π₯ {\displaystyle \scriptstyle {x}}; then we may assert π π₯ {\displaystyle \scriptstyle {\phi x}} without assigning a value to π₯ {\displaystyle \scriptstyle {x}}. This is done, for example, when the law of identity is asserted in the form " π΄ {\displaystyle \scriptstyle {A}} is π΄ {\displaystyle \scriptstyle {A}}." Here π΄ {\displaystyle \scriptstyle {A}} is left undetermined, because, however π΄ {\displaystyle \scriptstyle {A}} may be determined, the result will be true. Thus when we assert π π₯ {\displaystyle \scriptstyle {\phi x}}, leaving π₯ {\displaystyle \scriptstyle {x}} undetermined, we are asserting an ambiguous value of our function. This is only legitimate if, however the ambiguity may be determined, the result will be true. Thus take, as an illustration, the primitive proposition *1Β·2 below, namely " β’: π β¨ π . β . π {\displaystyle \scriptstyle {\vdash :p\lor p.\supset .p}},"
i.e. "' π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {p}}' implies π {\displaystyle \scriptstyle {p}}." Here π {\displaystyle \scriptstyle {p}} may be any elementary proposition: by leaving π {\displaystyle \scriptstyle {p}} undetermined, we obtain an assertion which can be applied to any particular elementary proposition. Such assertions are like the particular enunciations in Euclid: when it is said "let π΄ π΅ πΆ {\displaystyle \scriptstyle {ABC}} be an isosceles triangle; then the angles at the base will be equal," what is said applies to any isosceles triangle; it is stated concerning one triangle, but not concerning a definite one. All the assertions in the present work, with a very few exceptions, assert propositional functions, not definite propositions. As a matter of fact, no constant elementary proposition will occur in the present work, or can occur in any work which employs only logical ideas. The ideas and propositions of logic are all general: an assertion (for example) which is true of Socrates but not of Plato, will not belong to logic[4], and if an assertion which is true of both is to occur in logic, it must not be made concerning either, but concerning a variable π₯ {\displaystyle \scriptstyle {x}}. In order to obtain, in logic, a definite proposition instead of a propositional function, it is necessary to take some propositional function and assert that it is true always or sometimes, i.e. with all possible values of the variable or with some possible value. Thus, giving the name "individual" to whatever there is that is neither a proposition nor a function, the proposition "every individual is identical with itself" or the proposition "there are individuals" will be a proposition belonging to logic. But these propositions are not elementary.
(5) Negation. If π {\displaystyle \scriptstyle {p}} is any proposition, the proposition "not- π {\displaystyle \scriptstyle {p}}," or " π {\displaystyle \scriptstyle {p}} is false," will be represented by " βΌ π {\displaystyle \scriptstyle {\sim p}}." For the present, π {\displaystyle \scriptstyle {p}} must be an elementary proposition.
(6) Disjunction. If π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are any propositions, the proposition " π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {q}}," i.e. "either π {\displaystyle \scriptstyle {p}} is true or π {\displaystyle \scriptstyle {q}} is true," where the alternatives are to be not mutually exclusive, will be represented by " π β¨ π {\displaystyle \scriptstyle {p\lor q}}."
This is called the disjunction or the logical sum of π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}}. Thus " βΌ π β¨ π {\displaystyle \scriptstyle {\sim p\lor q}}" will mean " π {\displaystyle \scriptstyle {p}} is false or π {\displaystyle \scriptstyle {q}} is true"; βΌ ( π β¨ π ) {\displaystyle \scriptstyle {\sim (p\lor q)}} will mean "it is false that either π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {q}} is true," which is equivalent to " π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are both false"; βΌ ( βΌ π β¨ βΌ π ) {\displaystyle \scriptstyle {\sim (\sim p\lor \sim q)}} will mean "it is false that either π {\displaystyle \scriptstyle {p}} is false or π {\displaystyle \scriptstyle {q}} is false," which is equivalent to " π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are both true"; and so on. For the present, π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} must be elementary propositions. The above are all the primitive ideas required in the theory of deduction. Other primitive ideas will be introduced in Section B.
Definition of Implication. When a proposition π {\displaystyle \scriptstyle {q}} follows from a proposition π {\displaystyle \scriptstyle {p}}, so that if π {\displaystyle \scriptstyle {p}} is true, π {\displaystyle \scriptstyle {q}} must also be true, we say that π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}}. The idea of implication, in the form in which we require it, can be defined. The meaning to be given to implication in what follows may at first sight appear somewhat artificial; but although there are other legitimate meanings, the one here adopted is very much more convenient for our purposes than any of its rivals. The essential property that we require of implication is this: "What is implied by a true proposition is true." It is in virtue of this property that implication yields proofs. But this property by no means determines whether anything, and if so what, is implied by a false proposition. What it does determine is that, if π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}}, then it cannot be the case that π {\displaystyle \scriptstyle {p}} is true and π {\displaystyle \scriptstyle {q}} is false, i.e. it must be the case that either π {\displaystyle \scriptstyle {p}} is false or π {\displaystyle \scriptstyle {q}} is true. The most convenient interpretation of implication is to say, conversely, that if either π {\displaystyle \scriptstyle {p}} is false or π {\displaystyle \scriptstyle {q}} is true, then " π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}}" is to be true. Hence " π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}}" is to be defined to mean: "Either π {\displaystyle \scriptstyle {p}} is false or π {\displaystyle \scriptstyle {q}} is true." Hence we put:
*1Β·01. π β π
. βΌ π β¨ π Df. {\displaystyle \scriptstyle {p\supset q.=.\sim p\lor q\quad {\text{Df.}}}}
Here the letters " Df {\displaystyle \scriptstyle {\text{Df}}}" stand for "definition." They and the sign of equality together are to be regarded as forming one symbol, standing for "is defined to mean[5]." Whatever comes to the left of the sign of equality is defined to mean the same as what comes to the right of it. Definition is not among the primitive ideas, because definitions are concerned solely with the symbolism, not with what is symbolised; they are introduced for practical convenience, and are theoretically unnecessary.
In virtue of the above definition, when " π β π {\displaystyle \scriptstyle {p\supset q}}" holds, then either π {\displaystyle \scriptstyle {p}} is false or π {\displaystyle \scriptstyle {q}} is true; hence if π {\displaystyle \scriptstyle {p}} is true, π {\displaystyle \scriptstyle {q}} must be true. Thus the above definition preserves the essential characteristic of implication; it gives, in fact, the most general meaning compatible with the preservation of this characteristic.
Primitive Propositions.
*1Β·1. Anything implied by a true elementary proposition is true. Pp {\displaystyle \scriptstyle {\text{Pp}}}[6].
The above principle will be extended in *9 to propositions which are not elementary. It is not the same as "if π {\displaystyle \scriptstyle {p}} is true, then if π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}}, π {\displaystyle \scriptstyle {q}} is true." This is a true proposition, but it holds equally when π {\displaystyle \scriptstyle {p}} is not true and when π {\displaystyle \scriptstyle {p}} does not imply π {\displaystyle \scriptstyle {q}}. It does not, like the principle we are concerned with, enable us to assert π {\displaystyle \scriptstyle {q}} simply, without any hypothesis. We cannot express the principle symbolically, partly because any symbolism in which π {\displaystyle \scriptstyle {p}} is variable only gives the hypothesis that π {\displaystyle \scriptstyle {p}} is true, not the fact that it is true[7].
The above principle is used whenever we have to deduce a proposition from a proposition. But the immense majority of the assertions in the present work are assertions of propositional functions, i.e. they contain an undetermined variable. Since the assertion of a propositional function is a different primitive idea from the assertion of a proposition, we require a primitive proposition different from *1Β·1, though allied to it, to enable us to deduce the assertion of a propositional function " π π₯ {\displaystyle \scriptstyle {\psi x}}" from the assertions of the two propositional functions " π π₯ {\displaystyle \scriptstyle {\phi x}}" and " π π₯ β π π₯ {\displaystyle \scriptstyle {\phi x\supset \psi x}}." This primitive proposition is as follows:
*1Β·11. When π π₯ {\displaystyle \scriptstyle {\phi x}} can be asserted, where π₯ {\displaystyle \scriptstyle {x}} is a real variable, and π π₯ β π π₯ {\displaystyle \scriptstyle {\phi x\supset \psi x}} can be asserted, where π₯ {\displaystyle \scriptstyle {x}} is a real variable, then π π₯ {\displaystyle \scriptstyle {\psi x}} can be asserted, where π₯ {\displaystyle \scriptstyle {x}} is a real variable. Pp. {\displaystyle \scriptstyle {\text{Pp.}}}
This principle is also to be assumed for functions of several variables.
Part of the importance of the above primitive proposition is due to the fact that it expresses in the symbolism a result following from the theory of types, which requires symbolic recognition. Suppose we have the two assertions of propositional functions " β’ . π π₯ {\displaystyle \scriptstyle {\vdash .\phi x}}" and " β’ . π π₯ β π π₯ {\displaystyle \scriptstyle {\vdash .\phi x\supset \psi x}}"; then the " π₯ {\displaystyle \scriptstyle {x}}" in π π₯ {\displaystyle \scriptstyle {\phi x}} is not absolutely anything, but anything for which as argument the function " π π₯ {\displaystyle \scriptstyle {\phi x}}" is significant; similarly in " π π₯ β π π₯ {\displaystyle \scriptstyle {\phi x\supset \psi x}}" the π₯ {\displaystyle \scriptstyle {x}} is anything for which " π π₯ β π π₯ {\displaystyle \scriptstyle {\phi x\supset \psi x}}" is significant. Apart from some axiom, we do not know that the π₯ {\displaystyle \scriptstyle {x}}'s for which " π π₯ β π π₯ {\displaystyle \scriptstyle {\phi x\supset \psi x}}" is significant are the same as those for which " π π₯ {\displaystyle \scriptstyle {\phi x}}" is significant. The primitive proposition *1Β·11, by securing that, as the result of the assertions of the propositional functions " π π₯ {\displaystyle \scriptstyle {\phi x}}" and " π π₯ β π π₯ {\displaystyle \scriptstyle {\phi x\supset \psi x}}," the propositional function π π₯ {\displaystyle \scriptstyle {\psi x}} can also be asserted, secures partial symbolic recognition, in the form most useful in actual deductions, of an important principle which follows from the theory of types, namely that, if there is any one argument π {\displaystyle \scriptstyle {a}} for which both " π π {\displaystyle \scriptstyle {\phi a}}" and " π π {\displaystyle \scriptstyle {\psi a}}" are significant, then the range of arguments for which " π π₯ {\displaystyle \scriptstyle {\phi x}}" is significant is the same as the range of arguments for which " π π₯ {\displaystyle \scriptstyle {\psi x}}" is significant. It is obvious that, if the propositional function " π π₯ β π π₯ {\displaystyle \scriptstyle {\phi x\supset \psi x}}" can be asserted, there must be arguments π {\displaystyle \scriptstyle {a}} for which " π π β π π {\displaystyle \scriptstyle {\phi a\supset \psi a}}" is significant, and for which, therefore, " π π {\displaystyle \scriptstyle {\phi a}}" and " π π {\displaystyle \scriptstyle {\psi a}}" must be significant. Hence, by our principle, the values of π₯ {\displaystyle \scriptstyle {x}} for which " π π₯ {\displaystyle \scriptstyle {\phi x}}" is significant are the same as those for which " π π₯ {\displaystyle \scriptstyle {\psi x}}" is significant, i.e. the type of possible arguments for π π₯ ^{\displaystyle \scriptstyle {\phi {\hat {x}}}} (cf. p. 15) is the same as that of possible arguments for π π₯ ^{\displaystyle \scriptstyle {\psi {\hat {x}}}}. The primitive proposition *1Β·11, since it states a practically important consequence of this fact, is called the "axiom of identification of type."
Another consequence of the principle that, if there is an argument π {\displaystyle \scriptstyle {a}} for which both π π {\displaystyle \scriptstyle {\phi a}} and π π {\displaystyle \scriptstyle {\psi a}} are significant, then π π₯ {\displaystyle \scriptstyle {\phi x}} is significant whenever π π₯ {\displaystyle \scriptstyle {\psi x}} is significant, and vice versa, will be given in the "axiom of identification of real variables," introduced in *1Β·72. These two propositions, *1Β·11 and *1Β·72, give what is symbolically essential to the conduct of demonstrations in accordance with the theory of types.
The above proposition *1Β·11 is used in every inference from one asserted propositional function to another. We will illustrate the use of this proposition by setting forth at length the way in which it is first used, in the proof of *2Β·06. That proposition is " β’: . π β π . β: π β π . β . π β π . {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :q\supset r.\supset .p\supset r.}}"
We have already proved, in *2Β·05, the proposition β’: . π β π . β: π β π . β . π β π . {\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :p\supset q.\supset .p\supset r.}}
It is obvious that *2Β·06 results from *2Β·05 by means of *2Β·04, which is β’: . π . β . π β π :β: π . β . π β π . {\displaystyle \scriptstyle {\vdash :.p.\supset .q\supset r:\supset :q.\supset .p\supset r.}}
For if, in this proposition, we replace π {\displaystyle \scriptstyle {p}} by π β π {\displaystyle \scriptstyle {q\supset r}}, π {\displaystyle \scriptstyle {q}} by π β π {\displaystyle \scriptstyle {p\supset q}}, and π {\displaystyle \scriptstyle {r}} by π β π {\displaystyle \scriptstyle {p\supset r}}, we obtain, as an instance of *2Β·04, the proposition β’:: π β π . β: π β π . β . π β π : . β: . π β π . β: π β π . β . π β π (1) {\displaystyle \scriptstyle {\vdash ::q\supset r.\supset :p\supset q.\supset .p\supset r:.\supset :.p\supset q.\supset :q\supset r.\supset .p\supset r\qquad {\text{(1)}}}},
and here the hypothesis is asserted by *2Β·05. Thus our primitive proposition *1Β·11 enables us to assert the conclusion. *1Β·2. β’: π β¨ π . β . π Pp. {\displaystyle \scriptstyle {\vdash :p\lor p.\supset .p\quad {\text{Pp.}}}}
This proposition states: "If either π {\displaystyle \scriptstyle {p}} is true or π {\displaystyle \scriptstyle {p}} is true, then π {\displaystyle \scriptstyle {p}} is true." It is called the "principle of tautology," and will be quoted by the abbreviated title of "Taut." It is convenient, for purposes of reference, to give names to a few of the more important propositions; in general, propositions will be referred to by their numbers.
*1Β·3. β’: π . β . π β¨ π Pp. {\displaystyle \scriptstyle {\vdash :q.\supset .p\lor q\quad {\text{Pp.}}}}
This principle states: "If π {\displaystyle \scriptstyle {q}} is true, then ' π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {q}}' is true." Thus e.g. if π {\displaystyle \scriptstyle {q}} is "to-day is Wednesday" and π {\displaystyle \scriptstyle {p}} is "to-day is Tuesday," the principle states: "If to-day is Wednesday, then to-day is either Tuesday or Wednesday." It is called the "principle of addition," because it states that if a proposition is true, any alternative may be added without making it false. The principle will be referred to as "Add."
*1Β·4. β’: π β¨ π . β . π β¨ π Pp. {\displaystyle \scriptstyle {\vdash :p\lor q.\supset .q\lor p\quad {\text{Pp.}}}}
This principle sates that " π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {q}}" implies " π {\displaystyle \scriptstyle {q}} or π {\displaystyle \scriptstyle {p}}." It states the permutative law for logical addition of propositions, and will be called the "principle of permutation." It will be referred to as "Perm."
*1Β·5. β’: π β¨ ( π β¨ π ) . β . π β¨ ( π β¨ π ) Pp. {\displaystyle \scriptstyle {\vdash :p\lor (q\lor r).\supset .q\lor (p\lor r)\quad {\text{Pp.}}}}
This principle states: "If either π {\displaystyle \scriptstyle {p}} is true, or ' π {\displaystyle \scriptstyle {q}} or π {\displaystyle \scriptstyle {r}}' is true, then either π {\displaystyle \scriptstyle {q}} is true, or ' π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {r}}' is true." It is a form of the associative law for logical addition, and will be called the "associative principle." It will be referred to as "Assoc." The proposition π β¨ ( π β¨ π ) . β . ( π β¨ π ) β¨ π {\displaystyle \scriptstyle {p\lor (q\lor r).\supset .(p\lor q)\lor r}},
which would be the natural form for the associative law, has less deductive power, and is therefore not taken as a primitive proposition. *1Β·6. β’: . π β π . β: π β¨ π . β . π β¨ π Pp. {\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :p\lor q.\supset .p\lor r\quad {\text{Pp.}}}}
This principle states: "If π {\displaystyle \scriptstyle {q}} implies π {\displaystyle \scriptstyle {r}}, then ' π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {q}}' implies ' π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {r}}.'" In other words, in an implication, an alternative may be added to both premiss and conclusion without impairing the truth of the implication. The principle will be called the "principle of summation," and will be referred to as "Sum."
*1Β·7. If π {\displaystyle \scriptstyle {p}} is an elementary proposition, βΌ π {\displaystyle \scriptstyle {\sim p}} is an elementary proposition. Pp. {\displaystyle \scriptstyle {\text{Pp.}}}
*1Β·71. If π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are elementary propositions, π β¨ π {\displaystyle \scriptstyle {p\lor q}} is an elementary proposition. Pp. {\displaystyle \scriptstyle {\text{Pp.}}}
*1Β·72. If π π {\displaystyle \scriptstyle {\phi p}} and π π {\displaystyle \scriptstyle {\psi p}} are elementary propositional functions which take elementary propositions as arguments, π π β¨ π π {\displaystyle \scriptstyle {\phi p\lor \psi p}} is an elementary propositional function. Pp. {\displaystyle \scriptstyle {\text{Pp.}}}
This axiom is to apply also to functions of two or more variables. It is called the "axiom of identification of real variables." It will be observed that if π{\displaystyle \scriptstyle {\phi }} and π{\displaystyle \scriptstyle {\psi }} are functions which take arguments of different types, there is no such function as " π π₯ β¨ π π₯ {\displaystyle \scriptstyle {\phi x\lor \psi x}}," because π{\displaystyle \scriptstyle {\phi }} and π{\displaystyle \scriptstyle {\psi }} cannot significantly have the same argument. A more general form of the above axiom will be given in *9.
The use of the above axioms will generally be tacit. It is only through them and the axioms of *9 that the theory of types explained in the Introduction becomes relevant, and any view of logic which justifies these axioms justifies such subsequent reasoning as employs the theory of types.
This completes the list of primitive propositions required for the theory of deduction as applied to elementary propositions.
*2. Immediate Consequences of the Primitive Propositions. Summary of *2.
The proofs of the earlier of the propositions of this number consist simply in noticing that they are instances of the general rules given in *1. In such cases, these rules are not premisses, since they assert any instance of themselves, not something other than their instances. Hence when a general rule is adduced in early proofs, it will be adduced in brackets[8], with indications, when required, as to the changes of letters from those given in the rule to those in the case considered. Thus "Taut βΌ π π {\displaystyle \scriptstyle {\frac {\sim p}{p}}}" will mean what "Taut" becomes when βΌ π {\displaystyle \scriptstyle {\sim p}} is written in place of π {\displaystyle \scriptstyle {p}}. If "Taut βΌ π π {\displaystyle \scriptstyle {\frac {\sim p}{p}}}" is enclosed in square brackets before an asserted proposition, that means that, in accordance with "Taut," we are asserting what "Taut" becomes when βΌ π {\displaystyle \scriptstyle {\sim p}} is written in place of π {\displaystyle \scriptstyle {p}}. The recognition that a certain proposition is an instance of some general proposition previously proved or assumed is essential to the process of deduction from general rules, but cannot itself be erected into a general rule, since the application required is particular, and no general rule can explicitly include a particular application.
Again, when two different sets of symbols express the same proposition in virtue of a definition, say 1Β·01, and one of these, which we will call (1), has been asserted, the assertion of the other is made by writing "[(1).(1Β·01)]" before it, meaning that, in virtue of *1Β·01, the new set of symbols asserts the same proposition as was asserted in (1). A reference to a definition is distinguished from a reference to a previous proposition by being enclosed in round brackets.
The propositions in this number are all, or nearly all, actually needed in deducing mathematics from our primitive propositions. Although certain abbreviating processes will be gradually introduced, proofs will be given very fully, because the importance of the present subject lies, not in the propositions themselves, but (1) in the fact that they follow from the primitive propositions, (2) in the fact that the subject is the easiest, simplest, and most elementary example of the symbolic method of dealing with the principles of mathematics generally. Later portionsβthe theories of classes, relations, cardinal numbers, series, ordinal numbers, geometry, etc.βall employ the same method, but with an increasing complexity in the entities and functions considered.
The most important propositions proved in the present number are the following:
*2Β·02. β’: π . β . π β π {\displaystyle \scriptstyle {\vdash :q.\supset .p\supset q}}
I.e. π {\displaystyle \scriptstyle {q}} implies that π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}}, i.e. a true proposition is implied by any proposition. This proposition is called the "principle of simplification" (referred to as "Simp."), because, as will appear later, it enables us to pass from the joint assumption of π {\displaystyle \scriptstyle {q}} and π {\displaystyle \scriptstyle {p}} to the assertion of π {\displaystyle \scriptstyle {q}} simply. When the special meaning which we have given to implication is remembered, it will be seen that this proposition is obvious.
*2Β·03. β’: π ββΌ π . β . π ββΌ π {\displaystyle \scriptstyle {\vdash :p\supset \sim q.\supset .q\supset \sim p}}
*2Β·15. β’:βΌ π β π . β . βΌ π β π {\displaystyle \scriptstyle {\vdash :\sim p\supset q.\supset .\sim q\supset p}}
*2Β·16. β’: π β π . β . βΌ π ββΌ π {\displaystyle \scriptstyle {\vdash :p\supset q.\supset .\sim q\supset \sim p}}
*2Β·17. β’:βΌ π ββΌ π . β . π β π {\displaystyle \scriptstyle {\vdash :\sim q\supset \sim p.\supset .p\supset q}}
These four analogous propositions constitute the "principle of transposition," referred to as "Transp." They lead to the rule that in an implication the two sides may be interchanged by turning negative into positive and positive into negative. They are thus analogous to the algebraical rule that the two sides of an equation may be interchanged by changing the signs.
*2Β·04. β’: . π . β . π β π :β: π . β . π β π {\displaystyle \scriptstyle {\vdash :.p.\supset .q\supset r:\supset :q.\supset .p\supset r}}
This is called the "commutative principle" and referred to as "Comm." It states that, if π {\displaystyle \scriptstyle {r}} follows from π {\displaystyle \scriptstyle {q}} provided π {\displaystyle \scriptstyle {p}} is true, then π {\displaystyle \scriptstyle {r}} follows from π {\displaystyle \scriptstyle {p}} provided π {\displaystyle \scriptstyle {q}} is true.
*2Β·05. β’: . π β π . β: π β π . β . π β π {\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :p\supset q.\supset .p\supset r}}
*2Β·06. β’: . π β π . β: π β π . β . π β π π {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :q\supset r.\supset .p\supset {\cancel {q}}r}}
These two propositions are the source of the syllogism in Barbara (as will be shown later) and are therefore called the "principle of the syllogism" (referred to as "Syll."). The first states that, if π {\displaystyle \scriptstyle {r}} follows from π {\displaystyle \scriptstyle {q}}, then if π {\displaystyle \scriptstyle {q}} follows from π {\displaystyle \scriptstyle {p}}, π {\displaystyle \scriptstyle {r}} follows from π {\displaystyle \scriptstyle {p}}. The second states the same thing with the premisses interchanged.
*2Β·08. β’ . π β π {\displaystyle \scriptstyle {\vdash .p\supset p}}
I.e. any proposition implies itself. This is called the "principle of identity" and referred to as "Id." It is not the same as the "law of identity" (" π₯ {\displaystyle \scriptstyle {x}} is identical with π₯ {\displaystyle \scriptstyle {x}}"), but the law of identity is inferred from it (cf. *13Β·15).
*2Β·21. β’:βΌ π . β . π β π {\displaystyle \scriptstyle {\vdash :\sim p.\supset .p\supset q}}
I.e. a false proposition implies any proposition.
The later propositions of the present number are mostly subsumed under propositions in *3 or *4, which give the same results in more compendious forms. We now proceed to formal deductions.
*2Β·01. β’: π ββΌ π . β . βΌ π {\displaystyle \scriptstyle {\vdash :p\supset \sim p.\supset .\sim p}} This proposition states that, if π {\displaystyle \scriptstyle {p}} implies its own falsehood, then π {\displaystyle \scriptstyle {p}} is false. It is called the "principle of the reductio ad absurdum," and will be referred to as "Abs."[9]. The proof is as follows (where "Dem." is short for demonstration"):
Dem.(1) [ Taut βΌ π π ] β’:βΌ π β¨ βΌ π . β . βΌ π [ ( 1 ) . ( β 1 β 01 ) ] β’: π ββΌ π . β . βΌ π {\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Taut}}{\frac {\sim p}{p}}\right]\quad }&\scriptstyle {\vdash :\sim p\lor \sim p.\supset .\sim p}\\scriptstyle {[(1).(*1\cdot 01)]\quad }&\scriptstyle {\vdash :p\supset \sim p.\supset .\sim p}\end{array}}}
*2Β·02. β’: π . β . π β π {\displaystyle \scriptstyle {\vdash :q.\supset .p\supset q}}
Dem.(1) [ Add βΌ π π ] β’: π . β . βΌ π β¨ π [ ( 1 ) . ( β 1 β 01 ) ] β’: π . β . π β π {\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Add}}{\frac {\sim p}{p}}\right]\quad }&\scriptstyle {\vdash :q.\supset .\sim p\lor q}\\scriptstyle {[(1).(*1\cdot 01)]\quad }&\scriptstyle {\vdash :q.\supset .p\supset q}\end{array}}}
*2Β·03. β’: π ββΌ π . β . π ββΌ π {\displaystyle \scriptstyle {\vdash :p\supset \sim q.\supset .q\supset \sim p}}
Dem.(1) [ Perm βΌ π , βΌ π π ,
π ] β’:βΌ π β¨ βΌ π . β . βΌ π β¨ βΌ π [ ( 1 ) . ( β 1 β 01 ) ] β’: π ββΌ π . β . π ββΌ π {\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Perm}}{\frac {\sim p,\sim q}{p,~~q}}\right]\quad }&\scriptstyle {\vdash :\sim p\lor \sim q.\supset .\sim q\lor \sim p}\\scriptstyle {[(1).(*1\cdot 01)]\quad }&\scriptstyle {\vdash :p\supset \sim q.\supset .q\supset \sim p}\end{array}}}
*2Β·04. β’: . π . β . π β π :β: π . β . π β π {\displaystyle \scriptstyle {\vdash :.p.\supset .q\supset r:\supset :q.\supset .p\supset r}}
Dem.(1) [ Assoc βΌ π , βΌ π π ,
π ] β’: . βΌ π β¨ ( βΌ π β¨ π ) . β . βΌ π β¨ ( βΌ π β¨ π ) [ ( 1 ) . ( β 1 β 01 ) ] β’: . π . β . π β π :β: π . β . π β π {\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Assoc}}{\frac {\sim p,\sim q}{p,~~q}}\right]\quad }&\scriptstyle {\vdash :.\sim p\lor (\sim q\lor r).\supset .\sim q\lor (\sim p\lor r)}\\scriptstyle {[(1).(*1\cdot 01)]\quad }&\scriptstyle {\vdash :.p.\supset .q\supset r:\supset :q.\supset .p\supset r}\end{array}}}
*2Β·05. β’: . π β π . β: π β π . β . π β π {\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :p\supset q.\supset .p\supset r}}
Dem.(1) [ Sum βΌ π π ] β’: . π β π . β:βΌ π β¨ π . β . βΌ π β¨ π [ ( 1 ) . ( β 1 β 01 ) ] β’: . π β π . β: π β π . β . π β π {\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Sum}}{\frac {\sim p}{p}}\right]\quad }&\scriptstyle {\vdash :.q\supset r.\supset :\sim p\lor q.\supset .\sim p\lor r}\\scriptstyle {[(1).(*1\cdot 01)]\quad }&\scriptstyle {\vdash :.q\supset r.\supset :p\supset q.\supset .p\supset r}\end{array}}}
*2Β·06. β’: . π β π . β: π β π . β . π β π {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :q\supset r.\supset .p\supset r}}
Dem.(1) (2) [ Comm π β π , π β π , π β π π ,
π ,
π ] β’:: π β π . β: π β π . β . π β π : . β: . π β π . β: π β π . β . π β π [ β 2 β 05 ] β’: . π β π . β: π β π . β . π β π [ ( 1 ) . ( 2 ) . β 1 β 11 ] β’: . π β π . β: π β π . β . π β π {\displaystyle {\begin{array}{lll}\scriptstyle {\left[{\text{Comm}}{\frac {q\supset r,p\supset q,p\supset r}{p,~~q,~~r}}\right]\quad }&\scriptstyle {\vdash ::}&\scriptstyle {q\supset r.\supset :p\supset q.\supset .p\supset r:.}\&&\scriptstyle {\supset :.p\supset q.\supset :q\supset r.\supset .p\supset r}\\scriptstyle {[2\cdot 05]\quad }&\scriptstyle {\vdash :.}&\scriptstyle {q\supset r.\supset :p\supset q.\supset .p\supset r}\\scriptstyle {[(1).(2).1\cdot 11]\quad }&\scriptstyle {\vdash :.}&\scriptstyle {p\supset q.\supset :q\supset r.\supset .p\supset r}\end{array}}}
In the last line of this proof, " ( 1 ) . ( 2 ) . β 1 β 11 {\displaystyle \scriptstyle {(1).(2).*1\cdot 11}}" means that we are inferring in accordance with *1Β·11, having before us a proposition, namely π β π . β: π β π . β . π β π {\displaystyle \scriptstyle {p\supset q.\supset :q\supset r.\supset .p\supset r}}, which, by (1), is implied by π β π . β: π β π . β . π β π {\displaystyle \scriptstyle {q\supset r.\supset :p\supset q.\supset .p\supset r}}, which, by (2), is true. In general, in such cases, we shall omit the reference to *1Β·11.
The above two propositions will both be referred to as the "principle of the syllogism" (shortened to "Syll."), because, as will appear later, the syllogism in Barbara is derived from them.
2Β·07. β’: π . β . π β¨ π [ β 1 β 3 π π ] {\displaystyle \scriptstyle {\vdash :p.\supset .p\lor p\quad \left[1\cdot 3{\frac {p}{q}}\right]}}
Here we put nothing beyond " β 1 β 3 π π {\displaystyle \scriptstyle {*1\cdot 3{\frac {p}{q}}}}," because the proposition to be proved is what *1Β·3 becomes when π {\displaystyle \scriptstyle {p}} is written in place of π {\displaystyle \scriptstyle {q}}.
*2Β·08. β’ . π β π {\displaystyle \scriptstyle {\vdash .p\supset p}}
Dem. [ β 2 β 05 π β¨ π , π π ,
π ] β’:: π β¨ π . β . π :β: . π . β . π β¨ π :β . π β π ( 1 ) [ Taut ] β’: π β¨ π . β . π ( 2 ) [ ( 1 ) . ( 2 ) . β 1 β 11 ] β’: . π . β . π β¨ π :β . π β π ( 3 ) [ 2 β 07 ] β’: π . β . π β¨ π ( 4 ) [ ( 3 ) . ( 4 ) . β 1 β 11 ] β’ . π β π {\displaystyle {\begin{array}{lll}\scriptstyle {\left[2\cdot 05{\frac {p\lor p,p}{q,~~r}}\right]\quad }&\scriptstyle {\vdash ::p\lor p.\supset .p:\supset :.p.\supset .p\lor p:\supset .p\supset p\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {[{\text{Taut}}]\quad }&\scriptstyle {\vdash :p\lor p.\supset .p\qquad \qquad }&\scriptstyle {(2)}\\scriptstyle {[(1).(2).1\cdot 11]\quad }&\scriptstyle {\vdash :.p.\supset .p\lor p:\supset .p\supset p\qquad \qquad }&\scriptstyle {(3)}\\scriptstyle {[2\cdot 07]\quad }&\scriptstyle {\vdash :p.\supset .p\lor p\qquad \qquad }&\scriptstyle {(4)}\\scriptstyle {[(3).(4).*1\cdot 11]\quad }&\scriptstyle {\vdash .p\supset p\qquad \qquad }&\end{array}}}
2Β·1. β’ . βΌ π β¨ π [ Id. ( β 1 β 01 ) ] {\displaystyle \scriptstyle {\vdash .\sim p\lor p\quad [{\text{Id.}}(*1\cdot 01)]}}
*2Β·11. β’ . π β¨ βΌ π {\displaystyle \scriptstyle {\vdash .p\lor \sim p}}
Dem. [ Perm βΌ π , π π ,
π ] β’:βΌ π β¨ π . β . π β¨ βΌ π ( 1 ) [ ( 1 ) . β 2 β 1. β 1 β 11 ] β’ . π β¨ βΌ π {\displaystyle {\begin{array}{lll}\scriptstyle {\left[{\text{Perm}}{\frac {\sim p,p}{p,~~q}}\right]\quad }&\scriptstyle {\vdash :\sim p\lor p.\supset .p\lor \sim p\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {[(1).2\cdot 1.1\cdot 11]\quad }&\scriptstyle {\vdash .p\lor \sim p\qquad \qquad }&\end{array}}}
This is the law of excluded middle.
*2Β·12. β’ . π ββΌ ( βΌ π ) {\displaystyle \scriptstyle {\vdash .p\supset \sim (\sim p)}}
Dem. [ β 2 β 11 βΌ π π ] β’ . βΌ π β¨ βΌ ( βΌ π ) ( 1 ) [ ( 1 ) . ( β 1 β 01 ) ] β’ . π ββΌ ( βΌ π ) {\displaystyle {\begin{array}{lll}\scriptstyle {\left[2\cdot 11{\frac {\sim p}{p}}\right]\quad }&\scriptstyle {\vdash .\sim p\lor \sim (\sim p)\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {[(1).(1\cdot 01)]\quad }&\scriptstyle {\vdash .p\supset \sim (\sim p)\qquad \qquad }&\end{array}}}
*2Β·13. β’ . π β¨ βΌ { βΌ ( βΌ π ) } {\displaystyle \scriptstyle {\vdash .p\lor \sim {\sim (\sim p)}}}
This proposition is a lemma for *2Β·14, which, with *2Β·12, constitutes the principle of double negation.
Dem. [ Sum βΌ π , βΌ { βΌ ( βΌ π ) } π ,
π ] β’: . βΌ π . β . βΌ { βΌ ( βΌ π ) } . β: π β¨ βΌ π . β . π β¨ βΌ { βΌ ( βΌ π ) } ( 1 ) [ β 2 β 12 βΌ π π ] β’:βΌ π . β . βΌ { βΌ ( βΌ π ) } ( 2 ) [ ( 1 ) . ( 2 ) . β 1 β 11 ] β’: π β¨ βΌ π . β . π β¨ βΌ { βΌ ( βΌ π ) } ( 3 ) [ ( 3 ) . β 2 β 11. β 1 β 11 ] β’: π β¨ βΌ { βΌ ( βΌ π ) } {\displaystyle {\begin{array}{lll}\scriptstyle {\left[{\text{Sum}}{\frac {\sim p,\sim {\sim (\sim p)}}{q,~~~~~~r}}\right]\quad }&\scriptstyle {\vdash :.\sim p.\supset .\sim {\sim (\sim p)}.\supset :}&\&\scriptstyle {\qquad p\lor \sim p.\supset .p\lor \sim {\sim (\sim p)}\qquad }&\scriptstyle {(1)}\\scriptstyle {\left[2\cdot 12{\frac {\sim p}{p}}\right]}&\scriptstyle {\vdash :\sim p.\supset .\sim {\sim (\sim p)}}&\scriptstyle {(2)}\\scriptstyle {[(1).(2).1\cdot 11]}&\scriptstyle {\vdash :p\lor \sim p.\supset .p\lor \sim {\sim (\sim p)}}&\scriptstyle {(3)}\\scriptstyle {[(3).2\cdot 11.1\cdot 11]}&\scriptstyle {\vdash :p\lor \sim {\sim (\sim p)}}&\end{array}}}
*2Β·14. β’ . βΌ ( βΌ π ) β π {\displaystyle \scriptstyle {\vdash .\sim (\sim p)\supset p}}
Dem. [ Perm βΌ { βΌ ( βΌ π ) } π ] β’: π β¨ βΌ { βΌ ( βΌ π ) } . β . βΌ { βΌ ( βΌ π ) } β¨ π ( 1 ) [ ( 1 ) . β 2 β 13. β 1 β 11 ] β’ . βΌ { βΌ ( βΌ π ) } β¨ π ( 2 ) [ ( 2 ) . ( β 1 β 01 ) ] β’ . βΌ ( βΌ π ) β π {\displaystyle {\begin{array}{lll}\scriptstyle {\left[{\text{Perm}}{\frac {\sim {\sim (\sim p)}}{q}}\right]\quad }&\scriptstyle {\vdash :p\lor \sim {\sim (\sim p)}.\supset .\sim {\sim (\sim p)}\lor p\qquad }&\scriptstyle {(1)}\\scriptstyle {[(1).2\cdot 13.1\cdot 11]}&\scriptstyle {\vdash .\sim {\sim (\sim p)}\lor p}&\scriptstyle {(2)}\\scriptstyle {[(2).(*1\cdot 01)]}&\scriptstyle {\vdash .\sim (\sim p)\supset p}&\end{array}}}
*2Β·15 β’:βΌ π β π . β . βΌ π β π {\displaystyle \scriptstyle {\vdash :\sim p\supset q.\supset .\sim q\supset p}}
Dem. {{centre|}}
Note on the proof of *2Β·15. In the above proof, it will be seen that (3), (4), (6) are respectively of the forms π 1 β π 2 {\displaystyle \scriptstyle {p{1}\supset p{2}}}, π 2 β π 3 {\displaystyle \scriptstyle {p{2}\supset p{3}}}, π 3 β π 4 {\displaystyle \scriptstyle {p{3}\supset p{4}}}, where π 1 β π 4 {\displaystyle \scriptstyle {p{1}\supset p{4}}} is the proposition to be proved. From π 1 β π 2 {\displaystyle \scriptstyle {p{1}\supset p{2}}}, π 2 β π 3 {\displaystyle \scriptstyle {p{2}\supset p{3}}}, π 3 β π 4 {\displaystyle \scriptstyle {p{3}\supset p{4}}} the proposition π 1 β π 4 {\displaystyle \scriptstyle {p{1}\supset p{4}}} results by repeated applications of *2Β·05 or *2Β·06 (both of which are called "Syll."). It is tedious and unnecessary to repeat this process every time it is used; it will therefore be abbreviated into " [ Syll ]
β’ . ( π ) . ( π ) . ( π ) . ββ’ . ( π ) {\displaystyle \scriptstyle {[{\text{Syll}}]~\vdash .(a).(b).(c).\supset \vdash .(d)}},"
where ( π ) {\displaystyle \scriptstyle {(a)}} is of the form π 1 β π 2 {\displaystyle \scriptstyle {p{1}\supset p{2}}}, ( π ) {\displaystyle \scriptstyle {(b)}} of the form π 2 β π 3 {\displaystyle \scriptstyle {p{2}\supset p{3}}}, ( π ) {\displaystyle \scriptstyle {(c)}} of the form π 3 β π 4 {\displaystyle \scriptstyle {p{3}\supset p{4}}}, and ( π ) {\displaystyle \scriptstyle {(d)}} of the form π 1 β π 4 {\displaystyle \scriptstyle {p{1}\supset p{4}}}. The same abbreviation will be applied to a sorites of any length. Also where we have " β’ . π 1 {\displaystyle \scriptstyle {\vdash .p{1}}}" and " β’ . π 1 β π 2 {\displaystyle \scriptstyle {\vdash .p{1}\supset p{2}}}," and π 2 {\displaystyle \scriptstyle {p{2}}} is the proposition to be proved, it is convenient to write simply " β’ . π 1 . β{\displaystyle \scriptstyle {\vdash .p_{1}.\supset }}
[etc.] β’ . π 2 {\displaystyle \scriptstyle {\vdash .p_{2}}},"
where "etc." will be a reference to the previous propositions in virtue of which the implication " π 1 β π 2 {\displaystyle \scriptstyle {p{1}\supset p{2}}}" holds. This form embodies the use of *1Β·11 or *1Β·1, and makes many proofs at once shorter and easier to follow. It is used in the first two lines of the following proof. *2Β·16. β’: π β π . β . βΌ π ββΌ π {\displaystyle \scriptstyle {\vdash :p\supset q.\supset .\sim q\supset \sim p}}
Dem.
[
β
2
β
12
]
β’
.
π
ββΌ
(
βΌ
π
)
.
β
[
β
2
β
05
]
β’:
π
β
π
.
β
.
π
ββΌ
(
βΌ
π
)
(
1
)
[
β
2
β
03
βΌ
π
π
]
β’:
π
ββΌ
(
βΌ
π
)
.
β
.
βΌ
π
ββΌ
π
(
2
)
[
Syll
]
β’
.
(
1
)
.
(
2
)
.
ββ’:
π
β
π
.
β
.
βΌ
π
ββΌ
π
{\displaystyle {\begin{array}{lll}\scriptstyle {[2\cdot 12]\quad }&\scriptstyle {\vdash .q\supset \sim (\sim q).\supset }&\\scriptstyle {[2\cdot 05]}&\scriptstyle {\vdash :p\supset q.\supset .p\supset \sim (\sim q)}&\scriptstyle {(1)}\\scriptstyle {\left[*2\cdot 03{\frac {\sim q}{q}}\right]}&\scriptstyle {\vdash :p\supset \sim (\sim q).\supset .\sim q\supset \sim p}&\scriptstyle {(2)}\\scriptstyle {[{\text{Syll}}]}&\scriptstyle {\vdash .(1).(2).\supset \vdash :p\supset q.\supset .\sim q\supset \sim p}&\end{array}}}
Note. The proposition to be proved will be called " Prop {\displaystyle \scriptstyle {\text{Prop}}}," and when a proof ends, like that of *2Β·16, by an implication between asserted propositions, of which the consequent is the proposition to be proved, we shall write " β’ . etc. ββ’ . Prop {\displaystyle \scriptstyle {\vdash .{\text{etc.}}\supset \vdash .{\text{Prop}}}}". Thus " ββ’ . Prop {\displaystyle \scriptstyle {\supset \vdash .{\text{Prop}}}}" ends a proof, and more or less corresponds to "q.e.d."
*2Β·17. β’:βΌ π ββΌ π . β . π β π {\displaystyle \scriptstyle {\vdash :\sim q\supset \sim p.\supset .p\supset q}}
Dem. [ β 2 β 03 βΌ π , π π ,
π
]
β’:βΌ
π
ββΌ
π
.
β
.
π
ββΌ
(
βΌ
π
)
(
1
)
[
β
2
β
14
]
β’:βΌ
(
βΌ
π
)
β
π
:β
[
β
2
β
05
]
β’:
π
ββΌ
(
βΌ
π
)
.
β
.
π
β
π
(
2
)
[
Syll
]
β’
.
(
1
)
.
(
2
)
.
ββ’
.
Prop
{\displaystyle {\begin{array}{lll}\scriptstyle {\left[2\cdot 03{\frac {\sim q,p}{p,~q}}\right]\quad }&\scriptstyle {\vdash :\sim q\supset \sim p.\supset .p\supset \sim (\sim q)\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {[2\cdot 14]\quad }&\scriptstyle {\vdash :\sim (\sim q)\supset q:\supset }&\\scriptstyle {[*2\cdot 05]\quad }&\scriptstyle {\vdash :p\supset \sim (\sim q).\supset .p\supset q\qquad \qquad }&\scriptstyle {(2)}\\scriptstyle {[{\text{Syll}}]\quad }&\scriptstyle {\vdash .(1).(2).\supset \vdash .{\text{Prop}}}\end{array}}}
2Β·15, *2Β·16 and *2Β·17 are forms of the principle of transposition, and will be all referred to as "Transp." *2Β·18. β’:βΌ π β π . β . π {\displaystyle \scriptstyle {\vdash :\sim p\supset p.\supset .p}}
Dem. [ β 2 β 12 ] β’ . π ββΌ ( βΌ π ) . β [ β 2 β 05 ] β’ . βΌ π β π . β . βΌ π ββΌ ( βΌ π ) ( 1 ) [ β 2 β 01 βΌ π π ] β’:βΌ π ββΌ ( βΌ π ) . β . βΌ ( βΌ π ) ( 2 ) [ Syll ] β’ . ( 1 ) . ( 2 ) . ββ’:βΌ π β π . β . βΌ ( βΌ π ) ( 3 ) [ β 2 β 14 ] β’ . βΌ ( βΌ π ) β π ( 4 ) [ Syll ] β’ . ( 3 ) . ( 4 ) . ββ’ . Prop {\displaystyle {\begin{array}{lll}\scriptstyle {[2\cdot 12]\quad }&\scriptstyle {\vdash .p\supset \sim (\sim p).\supset }\\scriptstyle {[2\cdot 05]\quad }&\scriptstyle {\vdash .\sim p\supset p.\supset .\sim p\supset \sim (\sim p)\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {\left[2\cdot 01{\frac {\sim p}{p}}\right]\quad }&\scriptstyle {\vdash :\sim p\supset \sim (\sim p).\supset .\sim (\sim p)\qquad \qquad }&\scriptstyle {(2)}\\scriptstyle {[{\text{Syll}}]\quad }&\scriptstyle {\vdash .(1).(2).\supset \vdash :\sim p\supset p.\supset .\sim (\sim p)\qquad \qquad }&\scriptstyle {(3)}\\scriptstyle {[2\cdot 14]\quad }&\scriptstyle {\vdash .\sim (\sim p)\supset p\qquad \qquad }&\scriptstyle {(4)}\\scriptstyle {[{\text{Syll}}]\quad }&\scriptstyle {\vdash .(3).(4).\supset \vdash .{\text{Prop}}}\end{array}}}
This is the complement of the principle of the reductio ad absurdum. It states that a proposition which follows from the hypothesis of its own falsehood is true.
*2Β·2. β’: π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :p.\supset .p\lor q}}
Dem. β’ . Add . ββ’: π . β . π β¨ π ( 1 ) [ Perm ] β’: π β¨ π . β . π β¨ π ( 2 ) [ Syll ]
β’ . ( 1 ) . ( 2 ) . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .{\text{Add}}.\supset \vdash :p.\supset .q\lor p\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {[{\text{Perm}}]\vdash :q\lor p.\supset .p\lor q\qquad \qquad }&\scriptstyle {(2)}\\scriptstyle {[{\text{Syll}}]~~\vdash .(1).(2).\supset \vdash .{\text{Prop}}}\end{array}}}
2Β·21. β’:βΌ π . β . π β π [ β 2 β 2 βΌ π π ] {\displaystyle \scriptstyle {\vdash :\sim p.\supset .p\supset q\quad \left[2\cdot 2{\frac {\sim p}{p}}\right]}}
The above two propositions are very frequently used.
2Β·24. β’: π . β . βΌ π β π [ β 2 β 21. Comm ] {\displaystyle \scriptstyle {\vdash :p.\supset .\sim p\supset q\quad [2\cdot 21.{\text{Comm}}]}}
*2Β·25. β’: . π : β¨ : π β¨ π . β . π {\displaystyle \scriptstyle {\vdash :.p:\lor :p\lor q.\supset .q}}
Dem. β’ . β 2 β 1. ββ’:βΌ ( π β¨ π ) . β¨ . ( π β¨ π ) : [ Assoc ] ββ’: π . β¨ . { βΌ ( π β¨ π ) . β¨ . π } :ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .*2\cdot 1.}&\scriptstyle {\supset \vdash :\sim (p\lor q).\lor .(p\lor q):}\\scriptstyle {[{\text{Assoc}}]}&\scriptstyle {\supset \vdash :p.\lor .{\sim (p\lor q).\lor .q}:\supset \vdash .{\text{Prop}}}\end{array}}}
2Β·26. β’: . βΌ π : β¨ : π β π . β . π [ β 2 β 25 βΌ π π ] {\displaystyle \scriptstyle {\vdash :.\sim p:\lor :p\supset q.\supset .q\quad \left[2\cdot 25{\frac {\sim p}{p}}\right]}}
2Β·27. β’: . π . β: π β π . β . π [ β 2 β 26 ] {\displaystyle \scriptstyle {\vdash :.p.\supset :p\supset q.\supset .q\quad [2\cdot 26]}}
*2Β·3. β’: π β¨ ( π β¨ π ) . β . π β¨ ( π β¨ π ) {\displaystyle \scriptstyle {\vdash :p\lor (q\lor r).\supset .p\lor (r\lor q)}}
Dem. [ Perm π , π π , π ] β’: π β¨ π . β . π β¨ π : [ Sum π β¨ π , π β¨ π π ,
π
]
β
β’:
π
β¨
(
π
β¨
π
)
.
β
.
π
β¨
(
π
β¨
π
)
{\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Perm}}{\frac {q,r}{p,q}}\right]\quad }&\scriptstyle {\vdash :q\lor r.\supset .r\lor q:}\\scriptstyle {\left[{\text{Sum}}{\frac {q\lor r,r\lor q}{q,~~~r}}\right]\supset }&\scriptstyle {\vdash :p\lor (q\lor r).\supset .p\lor (r\lor q)}\end{array}}}
*2Β·31. β’: π β¨ ( π β¨ π ) . β . ( π β¨ π ) β¨ π {\displaystyle \scriptstyle {\vdash :p\lor (q\lor r).\supset .(p\lor q)\lor r}}
This proposition and 2Β·32 together constitute the associative law for logical addition of propositions. In the proof, the following abbreviation (constantly used hereafter) will be employed[10]: When we have a series of propositions of the form π β π {\displaystyle \scriptstyle {a\supset b}}, π β π {\displaystyle \scriptstyle {b\supset c}}, π β π {\displaystyle \scriptstyle {c\supset d}}, all asserted, and " π β π {\displaystyle \scriptstyle {a\supset d}}" is the proposition to be proved, the proof in full is as follows: [ Syll ] β’: . π β π . β: π β π . β . π β π ( 1 ) β’: π . β . π ( 2 ) [ ( 1 ) . ( 2 ) . β 1 β 11 ] β’: π β π . β . π β π ( 3 ) β’: π . β . π ( 4 ) [ ( 3 ) . ( 4 ) . β 1 β 11 ] β’: π . β . π ( 5 ) [ Syll ] β’: . π β π . β: π β π . β . π β π ( 6 ) [ ( 5 ) . ( 6 ) . β 1 β 11 ] β’: π β π . β . π β π ( 7 ) β’: π . β . π ( 8 ) [ ( 7 ) . ( 8 ) . β 1 β 11 ] β’: π . β . π {\displaystyle {\begin{array}{lll}\scriptstyle {[{\text{Syll}}]\quad }&\scriptstyle {\vdash :.a\supset b.\supset :b\supset c.\supset .a\supset c\qquad \qquad }&\scriptstyle {(1)}\&\scriptstyle {\vdash :a.\supset .b}&\scriptstyle {(2)}\\scriptstyle {[(1).(2).1\cdot 11]}&\scriptstyle {\vdash :b\supset c.\supset .a\supset c}&\scriptstyle {(3)}\&\scriptstyle {\vdash :b.\supset .c}&\scriptstyle {(4)}\\scriptstyle {[(3).(4).1\cdot 11]}&\scriptstyle {\vdash :a.\supset .c}&\scriptstyle {(5)}\\scriptstyle {[{\text{Syll}}]}&\scriptstyle {\vdash :.a\supset c.\supset :c\supset d.\supset .a\supset d}&\scriptstyle {(6)}\\scriptstyle {[(5).(6).1\cdot 11]}&\scriptstyle {\vdash :c\supset d.\supset .a\supset d}&\scriptstyle {(7)}\&\scriptstyle {\vdash :c.\supset .d}&\scriptstyle {(8)}\\scriptstyle {[(7).(8).*1\cdot 11]}&\scriptstyle {\vdash :a.\supset .d}\end{array}}}
It is tedious to write out this process in full; we therefore write simply β’: π . β . π . [ etc. ] β . π . [ etc. ] β . π :ββ’ . Prop, {\displaystyle {\begin{aligned}\scriptstyle {\vdash :a.}&\scriptstyle {\supset .b.}\\scriptstyle {[{\text{etc.}}]}&\scriptstyle {\supset .c.}\\scriptstyle {[{\text{etc.}}]}&\scriptstyle {\supset .d:\supset \vdash .{\text{Prop,}}}\end{aligned}}}
where " π β π {\displaystyle \scriptstyle {a\supset d}}" is the proposition to be proved. We indicate on the left by references in square brackets the propositions in virtue of which the successive implications hold. We put one dot (not two) after " π {\displaystyle \scriptstyle {b}}," to show that it is π {\displaystyle \scriptstyle {b}}, not " π β π {\displaystyle \scriptstyle {a\supset b}}," that implies π {\displaystyle \scriptstyle {c}}. But we put two dots after π {\displaystyle \scriptstyle {d}}, to show that now the whole proposition " π β π {\displaystyle \scriptstyle {a\supset d}}" is concerned. If " π β π {\displaystyle \scriptstyle {a\supset d}}" is not the proposition to be proved, but is to be used subsequently in the proof, we put β’: π . β . π . [ etc. ] β . π . [ etc. ] β . π (1), {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash :a.}&\scriptstyle {\supset .b.}\\scriptstyle {[{\text{etc.}}]}&\scriptstyle {\supset .c.}\\scriptstyle {[{\text{etc.}}]}&\scriptstyle {\supset .d\qquad \qquad \qquad \qquad \qquad {\text{(1),}}}\end{array}}}
and then " ( 1 ) {\displaystyle \scriptstyle {(1)}}" means " π β π {\displaystyle \scriptstyle {a\supset d}}." The proof of *2Β·31 is as follows: Dem. [ β 2 β 3 ] β’: π β¨ ( π β¨ π ) . β . π β¨ ( π β¨ π ) . [ Assoc π , π π , π ] β . π β¨ ( π β¨ π ) . [ Perm π , π β¨ π π ,
π ] β . ( π β¨ π ) β¨ π :ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {[*2\cdot 3]\vdash :p\lor (q\lor r).}&\scriptstyle {\supset .p\lor (r\lor q).}\\scriptstyle {\left[{\text{Assoc}}{\frac {r,q}{q,r}}\right]\quad }&\scriptstyle {\supset .r\lor (p\lor q).}\\scriptstyle {[{\text{Perm}}{\frac {r,p\lor q}{p,~~q}}]\quad }&\scriptstyle {\supset .(p\lor q)\lor r:\supset \vdash .{\text{Prop}}}\end{array}}}
*2Β·32. β’: ( π β¨ π ) β¨ π . β . π β¨ ( π β¨ π ) {\displaystyle \scriptstyle {\vdash :(p\lor q)\lor r.\supset .p\lor (q\lor r)}}
Dem. [ Perm π β¨ π , π π ,
π ] β’: ( π β¨ π ) β¨ π . β . π β¨ ( π β¨ π ) [ Assoc π , π , π π , π , π ] β . π β¨ ( π β¨ π ) [ β 2 β 3 ] β . π β¨ ( π β¨ π ) :ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Perm}}{\frac {p\lor q,r}{p,~q}}\right]\vdash :(p\lor q)\lor r.}&\scriptstyle {\supset .r\lor (p\lor q)}\\scriptstyle {\left[{\text{Assoc}}{\frac {r,p,q}{p,q,r}}\right]}&\scriptstyle {\supset .p\lor (r\lor q)}\\scriptstyle {[*2\cdot 3]}&\scriptstyle {\supset .p\lor (q\lor r):\supset \vdash .{\text{Prop}}}\end{array}}}
*2Β·33. π β¨ π β¨ π
. ( π β¨ π ) β¨ π Df {\displaystyle \scriptstyle {p\lor q\lor r.=.(p\lor q)\lor r\quad {\text{Df}}}}
This definition serves only for the avoidance of brackets.
*2Β·36. β’: . π β π . β: π β¨ π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :p\lor q.\supset .r\lor p}}
Dem. [ Perm ] β’: π β¨ π . β . π β¨ π : [ Syll π β¨ π , π β¨ π , π β¨ π π ,
π ,
π
]
β
β’:
.
π
β¨
π
.
β
.
π
β¨
π
:β:
π
β¨
π
.
β
.
π
β¨
π
(
1
)
[
Sum
]
β’:
.
π
β
π
.
β:
π
β¨
π
.
β
.
π
β¨
π
(
2
)
β’
.
(
1
)
.
(
2
)
.
π
π¦
π
π
.
ββ’
.
Prop
{\displaystyle {\begin{array}{lll}\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\vdash :p\lor r.\supset .r\lor p:}\\scriptstyle {\left[{\text{Syll}}{\frac {p\lor q,p\lor r,r\lor p}{p,~~q,~~r}}\right]\supset }&\scriptstyle {\vdash :.p\lor q.\supset .p\lor r:\supset :p\lor q.\supset .r\lor p\quad }&\scriptstyle {(1)}\\scriptstyle {[{\text{Sum}}]}&\scriptstyle {\vdash :.q\supset r.\supset :p\lor q.\supset .p\lor r}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).Syll.\supset \vdash .{\text{Prop}}}\end{array}}}
*2Β·37. β’: . π β π . β: π β¨ π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :q\lor p.\supset .p\lor r}} [ Syll . Perm . Sum ] {\displaystyle \scriptstyle {[{\text{Syll}}.{\text{Perm}}.{\text{Sum}}]}}
*2Β·38. β’: . π β π . β: π β¨ π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :q\lor p.\supset .r\lor p}} [ Syll . Perm . Sum ] {\displaystyle \scriptstyle {[{\text{Syll}}.{\text{Perm}}.{\text{Sum}}]}}
The proofs of *2Β·37Β·38 are exactly analogous to that of *2Β·36. (We use "2Β·37Β·38" as an abbreviation for "2Β·37 and *2Β·38." Such abbreviations will be used throughout.)
The use of a general principle of deduction, such as either form of " π π¦ π π {\displaystyle \scriptstyle {Syll}}," in a proof, is different from the use of the particular premisses to which the principle of deduction is applied. The principle of deduction gives the general rule according to which the inference is made, but is not itself a premiss in the inference. If we treated it as a premiss, we should need either it or some other general rule to enable us to infer the desired conclusion, and thus we should gradually acquire an increasing accumulation of premisses without ever being able to make any inference. Thus when a general rule is adduced in drawing an inference, as when we write " [ Syll ] β’ . ( 1 ) . ( 2 ) . ββ’ . Prop {\displaystyle \scriptstyle {[{\text{Syll}}]\vdash .(1).(2).\supset \vdash .{\text{Prop}}}}," the mention of " Syll {\displaystyle \scriptstyle {\text{Syll}}}" is only required in order to remind the reader how the inference is drawn.
The rule of inference may, however, also occur as one of the ordinary premisses, that is to say, in the case of " Syll {\displaystyle \scriptstyle {\text{Syll}}}" for example, the proposition " π β π . β: π β π . β . π β π {\displaystyle \scriptstyle {p\supset q.\supset :q\supset r.\supset .p\supset r}}" may be one of those to which our rules of deduction are applied, and it is then an ordinary premiss. The distinction between the two uses of principles of deduction is of some philosophical importance, and in the above proofs we have indicated it by putting the rule of inference in square brackets. It is, however, practically inconvenient to continue to distinguish in the manner of the reference. We shall therefore henceforth both adduce ordinary premisses in square brackets where convenient, and adduce rules of inference, along with other propositions, in asserted premisses, i.e. we shall write e.g. " β’ . ( 1 ) . ( 2 ) . Syll . ββ’ . Prop {\displaystyle \scriptstyle {\vdash .(1).(2).{\text{Syll}}.\supset \vdash .{\text{Prop}}}}"
rather than " [ Syll ] β’ . ( 1 ) . ( 2 ) . ββ’ . Prop {\displaystyle \scriptstyle {[{\text{Syll}}]\vdash .(1).(2).\supset \vdash .{\text{Prop}}}}"
*2Β·4. β’: . π . β¨ . π β¨ π :β . π β¨ π {\displaystyle \scriptstyle {\vdash :.p.\lor .p\lor q:\supset .p\lor q}}
Dem. β’ . β 2 β 31. ββ’: . π . β¨ . π β¨ π : β: π β¨ π . β¨ π : [ Taut . β 2 β 38 ] β: π β¨ π : . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .2\cdot 31.\supset \vdash :.p.\lor .p\lor q:}&\scriptstyle {\supset :p\lor p.\lor q:}\\scriptstyle {[{\text{Taut}}.2\cdot 38]}&\scriptstyle {\supset :p\lor q:.\supset \vdash .{\text{Prop}}}\end{array}}}
*2Β·41. β’: . π . β¨ . π β¨ π :β . π β¨ π {\displaystyle \scriptstyle {\vdash :.q.\lor .p\lor q:\supset .p\lor q}}
Dem. [ Assoc π , π , π π , π , π ] β’: . π . β¨ . π β¨ π : β: π . β¨ . π β¨ π : [ Taut . Sum ] β: π β¨ π : . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\left[{\text{Assoc}}{\frac {q,p,q}{p,q,r}}\right]\vdash :.q.\lor .p\lor q:}&\scriptstyle {\supset :p.\lor .q\lor q:}\\scriptstyle {[{\text{Taut}}.{\text{Sum}}]}&\scriptstyle {\supset :p\lor q:.\supset \vdash .{\text{Prop}}}\end{array}}}
*2Β·42. β’: . βΌ π . β¨ . π β π :β . π β π
[ β 2 β 4 βΌ π π ] {\displaystyle \scriptstyle {\vdash :.\sim p.\lor .p\supset q:\supset .p\supset q~\left[*2\cdot 4{\frac {\sim p}{p}}\right]}}
2Β·43. β’: . π . β . π β π :β . π β π [ β 2 β 42 ] {\displaystyle \scriptstyle {\vdash :.p.\supset .p\supset q:\supset .p\supset q\quad [2\cdot 42]}}
2Β·45. β’:βΌ ( π β¨ π ) . β . βΌ π [ β 2 β 2. Transp ] {\displaystyle \scriptstyle {\vdash :\sim (p\lor q).\supset .\sim p\qquad [2\cdot 2.{\text{Transp}}]}}
2Β·46. β’:βΌ ( π β¨ π ) . β . βΌ π [ β 1 β 3. Transp ] {\displaystyle \scriptstyle {\vdash :\sim (p\lor q).\supset .\sim q\qquad [1\cdot 3.{\text{Transp}}]}}
2Β·47. β’:βΌ ( π β¨ π ) . β . βΌ π β¨ π [ β 2 β 45. β 2 β 2 βΌ π π . Syll ] {\displaystyle \scriptstyle {\vdash :\sim (p\lor q).\supset .\sim p\lor q\qquad \left[2\cdot 45.*2\cdot 2{\frac {\sim p}{p}}.{\text{Syll}}\right]}}
2Β·48. β’:βΌ ( π β¨ π ) . β . π β¨ βΌ π [ β 2 β 46. β 1 β 3 βΌ π π . Syll ] {\displaystyle \scriptstyle {\vdash :\sim (p\lor q).\supset .p\lor \sim q\qquad \left[2\cdot 46.*1\cdot 3{\frac {\sim q}{q}}.{\text{Syll}}\right]}}
*2Β·49. β’:βΌ ( π β¨ π ) . β . βΌ π β¨ βΌ π [ β 2 β 45. β 2 β 2 βΌ π , βΌ π π ,
π . Syll ] {\displaystyle \scriptstyle {\vdash :\sim (p\lor q).\supset .\sim p\lor \sim q\qquad \left[2\cdot 45.2\cdot 2{\frac {\sim p,\sim q}{p,~~q}}.{\text{Syll}}\right]}}
2Β·5. β’:βΌ ( π β π ) . β . βΌ π β π [ β 2 β 47 βΌ π π ] {\displaystyle \scriptstyle {\vdash :\sim (p\supset q).\supset .\sim p\supset q\qquad \left[2\cdot 47{\frac {\sim p}{p}}\right]}}
2Β·51. β’:βΌ ( π β π ) . β . π ββΌ π [ β 2 β 48 βΌ π π ] {\displaystyle \scriptstyle {\vdash :\sim (p\supset q).\supset .p\supset \sim q\qquad \left[2\cdot 48{\frac {\sim p}{p}}\right]}}
2Β·52. β’:βΌ ( π β π ) . β . π ββΌ π [ β 2 β 49 βΌ π π ] {\displaystyle \scriptstyle {\vdash :\sim (p\supset q).\supset .p\supset \sim q\qquad \left[2\cdot 49{\frac {\sim p}{p}}\right]}}
2Β·521. β’:βΌ ( π β π ) . β . π β π [ β 2 β 52 β 17 ] {\displaystyle \scriptstyle {\vdash :\sim (p\supset q).\supset .q\supset p\qquad [2\cdot 52\cdot 17]}}
*2Β·53. β’: π β¨ π . β . βΌ π β π {\displaystyle \scriptstyle {\vdash :p\lor q.\supset .\sim p\supset q}}
Dem. β’ . β 2 β 12 β 38. ββ’: π β¨ π . β . βΌ ( βΌ π ) β¨ π :ββ’ . Prop {\displaystyle \scriptstyle {\vdash .*2\cdot 12\cdot 38.\supset \vdash :p\lor q.\supset .\sim (\sim p)\lor q:\supset \vdash .{\text{Prop}}}}
2Β·54. β’:βΌ π β π . β . π β¨ π [ β 2 β 14 β 38 ] {\displaystyle \scriptstyle {\vdash :\sim p\supset q.\supset .p\lor q\qquad [2\cdot 14\cdot 38]}}
2Β·55. β’: . βΌ π . β: π β¨ π . β . π [ β 2 β 53. Comm ] {\displaystyle \scriptstyle {\vdash :.\sim p.\supset :p\lor q.\supset .q\quad [2\cdot 53.{\text{Comm}}]}}
2Β·56. β’: . βΌ π . β: π β¨ π . β . π [ β 2 β 55 π , π π , π . Perm ] {\displaystyle \scriptstyle {\vdash :.\sim q.\supset :p\lor q.\supset .p\quad \left[2\cdot 55{\frac {q,p}{p,q}}.{\text{Perm}}\right]}}
*2Β·6. β’: . βΌ π β π . β: π β π . β . π {\displaystyle \scriptstyle {\vdash :.\sim p\supset q.\supset :p\supset q.\supset .q}}
Dem. [ β 2 β 38 ] β’: . βΌ π β π . β:βΌ π β¨ π . β . π β¨ π ( 1 ) [ Taut . Syll ] β’: . βΌ π β¨ π . β . π β¨ π :β:βΌ π β¨ π . β . π ( 2 ) β’ . ( 1 ) . ( 2 ) . Syll . ββ’: . βΌ π β π . β:βΌ π β¨ π . β . π : . ββ’ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{lll}\scriptstyle {[*2\cdot 38]}&\scriptstyle {\vdash :.\sim p\supset q.\supset :\sim p\lor q.\supset .q\lor q}&\scriptstyle {(1)}\\scriptstyle {[{\text{Taut}}.{\text{Syll}}]}&\scriptstyle {\vdash :.\sim p\lor q.\supset .q\lor q:\supset :\sim p\lor q.\supset .q\qquad }&\scriptstyle {(2)}\end{array}}\&\scriptstyle {\vdash .(1).(2).{\text{Syll}}.\supset \vdash :.\sim p\supset q.\supset :\sim p\lor q.\supset .q:.\supset \vdash .{\text{Prop}}}\end{aligned}}}
2Β·61. β’: . π β π . β:βΌ π β π . β . π [ β 2 β 6. Comm ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :\sim p\supset q.\supset .q\quad [2\cdot 6.{\text{Comm}}]}}
2Β·61. β’: . π β π . β:βΌ π β π . β . π [ β 2 β 6. Comm ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :\sim p\supset q.\supset .q\qquad [2\cdot 6.{\text{Comm}}]}}
2Β·62. β’: . π β¨ π . β: π β π . β . π [ β 2 β 53 β 6. Syll ] {\displaystyle \scriptstyle {\vdash :.p\lor q.\supset :p\supset q.\supset .q\qquad [2\cdot 53\cdot 6.{\text{Syll}}]}}
2Β·621. β’: . π β π . β: π β¨ π . β . π [ β 2 β 62. Comm ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :p\lor q.\supset .q\qquad [2\cdot 62.{\text{Comm}}]}}
2Β·63. β’: . π β¨ π . β:βΌ π β¨ π . β . π [ β 2 β 62 ] {\displaystyle \scriptstyle {\vdash :.p\lor q.\supset :\sim p\lor q.\supset .q\qquad [2\cdot 62]}}
2Β·64. β’: . π β¨ π . β: π β¨ βΌ π . β . π [ β 2 β 63 π , π π , π . Perm ] {\displaystyle \scriptstyle {\vdash :.p\lor q.\supset :p\lor \sim q.\supset .p\qquad \left[2\cdot 63{\frac {q,p}{p,q}}.{\text{Perm}}\right]}}
2Β·65. β’: . π β π . β: π ββΌ π . β . βΌ π [ β 2 β 64 βΌ π π ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :p\supset \sim q.\supset .\sim p\quad \left[2\cdot 64{\frac {\sim p}{p}}\right]}}
*2Β·67. β’: . π β¨ π . β . π :β . π β π {\displaystyle \scriptstyle {\vdash :.p\lor q.\supset .q:\supset .p\supset q}}
Dem. [ β 2 β 54. Syll ]
β’: . π β¨ π . β . π :β:βΌ π β π . β . π ( 1 ) [ β 2 β 24. Syll ] β’: . βΌ π β π . β . π :β . π β π ( 2 ) β’ . ( 1 ) . ( 2 ) . Syll . ββ’ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{lll}\scriptstyle {[2\cdot 54.{\text{Syll}}]~}&\scriptstyle {\vdash :.p\lor q.\supset .q:\supset :\sim p\supset q.\supset .q\qquad }&\scriptstyle {(1)}\\scriptstyle {[2\cdot 24.{\text{Syll}}]}&\scriptstyle {\vdash :.\sim p\supset q.\supset .q:\supset .p\supset q}&\scriptstyle {(2)}\end{array}}\&\scriptstyle {\vdash .(1).(2).{\text{Syll}}.\supset \vdash .{\text{Prop}}}\end{aligned}}}
*2Β·68. β’: . π β π . β . π :β . π β¨ π {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset .q:\supset .p\lor q}}
Dem. [ β 2 β 67 βΌ π π ] β’: . π β π . β . π :β . βΌ π β π ( 1 ) β’ . ( 1 ) . β 2 β 54. ββ’ . Prop {\displaystyle {\begin{aligned}&\scriptstyle {\left[2\cdot 67{\frac {\sim p}{p}}\right]\vdash :.p\supset q.\supset .q:\supset .\sim p\supset q\qquad \qquad \qquad (1)}\&\scriptstyle {\vdash .(1).2\cdot 54.\supset \vdash .{\text{Prop}}}\end{aligned}}}
2Β·69. β’: . π β π . β . π :β: π β π . β . π [ β 2 β 68. Perm . β 2 β 62 π , π π , π ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset .q:\supset :q\supset p.\supset .p\qquad \left[2\cdot 68.{\text{Perm}}.*2\cdot 62{\frac {q,p}{p,q}}\right]}}
2Β·73. β’: . π β π . β: π β¨ π β¨ π . β . π β¨ π [ β 2 β 621 β 38 ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :p\lor q\lor r.\supset .q\lor r\qquad [2\cdot 621\cdot 38]}}
2Β·74. β’: . π β π . β: π β¨ π β¨ π . β . π β¨ π [ β 2 β 73 π , π π , π . Assoc . Syll ] {\displaystyle \scriptstyle {\vdash :.q\supset p.\supset :p\lor q\lor r.\supset .p\lor r\qquad \left[2\cdot 73{\frac {q,p}{p,q}}.{\text{Assoc}}.{\text{Syll}}\right]}}
2Β·75. β’:: π β¨ π . β: . π . β¨ . π β π :β . π β¨ π [ β 2 β 74 βΌ π π . β 2 β 53 β 31 ] {\displaystyle \scriptstyle {\vdash ::p\lor q.\supset :.p.\lor .q\supset r:\supset .p\lor r\qquad \left[2\cdot 74{\frac {\sim q}{q}}.*2\cdot 53\cdot 31\right]}}
2Β·76. β’: . π . β¨ . π β π :β: π β¨ π . β . π β¨ π [ β 2 β 75. Comm ] {\displaystyle \scriptstyle {\vdash :.p.\lor .q\supset r:\supset :p\lor q.\supset .p\lor r\qquad [2\cdot 75.{\text{Comm}}]}}
2Β·77. β’: . π . β . π β π :β: π β π . β . π β π [ β 2 β 76 βΌ π π ] {\displaystyle \scriptstyle {\vdash :.p.\supset .q\supset r:\supset :p\supset q.\supset .p\supset r\qquad \left[2\cdot 76{\frac {\sim p}{p}}\right]}}
*2Β·8. β’: . π β¨ π . β:βΌ π β¨ π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :.q\lor r.\supset :\sim r\lor s.\supset .q\lor s}}
Dem. β’ . β 2 β 53. Perm . ββ’: . π β¨ π . β:βΌ π β π : [ β 2 β 38 ] β:βΌ π β¨ π . β . π β¨ π : . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .2\cdot 53.{\text{Perm}}.\supset \vdash :.q\lor r.}&\scriptstyle {\supset :\sim r\supset q:}\\scriptstyle {[2\cdot 38]}&\scriptstyle {\supset :\sim r\lor s.\supset .q\lor s:.\supset \vdash .{\text{Prop}}}\end{array}}}
*2Β·81. β’:: π . β . π β π :β: . π β¨ π . β: π β¨ π . β . π β¨ π {\displaystyle \scriptstyle {\vdash ::q.\supset .r\supset s:\supset :.p\lor q.\supset :p\lor r.\supset .p\lor s}}
Dem.
β’
.
Sum
.
ββ’::
π
.
β
.
π
β
π
:β:
.
π
β¨
π
.
β:
π
.
β¨
.
π
β
π
(
1
)
β’
.
β
2
β
76.
Syll
.
ββ’::
π
β¨
π
.
β:
π
.
β¨
.
π
β
π
:
.
β:
.
π
β¨
π
.
β:
π
β¨
π
.
β
.
π
β¨
π
(
2
)
β’
.
(
1
)
.
(
2
)
.
ββ’
.
Prop
{\displaystyle {\begin{array}{lll}\scriptstyle {\vdash .{\text{Sum}}.\supset \vdash ::q.\supset .r\supset s:\supset :.p\lor }&\scriptstyle {q.\supset :p.\lor .r\supset s\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {\vdash .*2\cdot 76.{\text{Syll}}.\supset \vdash ::p\lor q.\supset :p.\lor }&\scriptstyle {.r\supset s:.\supset :.}\&\scriptstyle {p\lor q.\supset :p\lor r.\supset .p\lor s}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).\supset \vdash .{\text{Prop}}}\end{array}}}
2Β·82. β’: . π β¨ π β¨ π . β: π β¨ βΌ π β¨ π . β . π β¨ π β¨ π [ β 2 β 8. β 2 β 81 π β¨ π , βΌ π β¨ π , π β¨ π π , π , π ] {\displaystyle {\begin{aligned}\scriptstyle {\vdash :.p\lor q\lor r.\supset :p\lor \sim r\lor s.\supset .p\lor }&\scriptstyle {q\lor s}\&\scriptstyle {\left[2\cdot 8.*2\cdot 81{\frac {q\lor r,\sim r\lor s,q\lor s}{q,\quad r,\quad s}}\right]}\end{aligned}}}
*2Β·83. β’:: π . β . π β π :β: . π . β . π β π : β: π . β . π β π [ β 2 β 82 βΌ π , βΌ π π ,
π ] {\displaystyle {\begin{aligned}\scriptstyle {\vdash ::p.\supset .q\supset r:\supset :.p.\supset .r\supset s:}&\scriptstyle {\supset :p.\supset .q\supset s}\&\scriptstyle {\left[*2\cdot 82{\frac {\sim p,\sim q}{p,~~q}}\right]}\end{aligned}}}
*2Β·85. β’: . π β¨ π . β . π β¨ π :β: π . β¨ . π β π {\displaystyle \scriptstyle {\vdash :.p\lor q.\supset .p\lor r:\supset :p.\lor .q\supset r}}
Dem.
[
Add
.
Syll
]
β’:
.
π
β¨
π
.
β
.
π
:β
.
π
β
π
(
1
)
β’
.
β
2
β
55.
β
β’::βΌ
π
.
β:
.
π
β¨
π
.
β
.
π
:
.
[
Syll
]
β:
.
π
β¨
π
.
β
.
π
β¨
π
:
β:
π
β¨
π
.
β
.
π
:
.
[
(
1
)
.
β
2
β
83
]
β:
.
π
β¨
π
.
β
.
π
β¨
π
:
β:
π
β
π
(
2
)
β’
.
(
2
)
.
Com
m
.
ββ’:
.
π
β¨
π
.
β
.
π
β¨
π
:
β:βΌ
π
.
β
.
π
β
π
:
[
β
2
β
54
]
β:
π
.
β¨
.
π
β
π
:
.
ββ’
.
Prop
{\displaystyle {\begin{array}{lllll}\scriptstyle {[{\text{Add}}.{\text{Syll}}]}&\scriptstyle {\vdash :.p\lor q}&\scriptstyle {.\supset .r:\supset .q\supset r}&&\scriptstyle {(1)}\\scriptstyle {\vdash .2\cdot 55.\supset }&\scriptstyle {\vdash ::\sim p.}&\scriptstyle {\supset :.p\lor r.\supset .r:.}\\scriptstyle {[{\text{Syll}}]}&&\scriptstyle {\supset :.p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :p\lor q.\supset .r:.}\\scriptstyle {[(1).2\cdot 83]}&&\scriptstyle {\supset :.p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :q\supset r}&\scriptstyle {(2)}\\scriptstyle {\vdash .(2).{\text{Com}}}&\scriptstyle {{\text{m}}.\supset \vdash :.}&\scriptstyle {\quad p\lor q.\supset .p\lor r:}&\scriptstyle {\supset :\sim p.\supset .q\supset r:}\\scriptstyle {[*2\cdot 54]}&&&\scriptstyle {\supset :p.\lor .q\supset r:.\supset \vdash .}&\scriptstyle {\text{Prop}}\end{array}}}
2Β·86. β’: . π β π . β . π β π :β: π . β . π β π [ β 2 β 85 βΌ π π ] {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset .p\supset r:\supset :p.\supset .q\supset r\quad \left[2\cdot 85{\frac {\sim p}{p}}\right]}}
*3. The Logical Product of two Propositions Summary of *3.
The logical product of two propositions π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} is practically the proposition " π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are both true." But this as it stands would have to be a new primitive idea. We therefore take as the logical product the proposition βΌ ( βΌ π β¨ βΌ π ) {\displaystyle \scriptstyle {\sim (\sim p\lor \sim q)}}, i.e. "it is false that either π {\displaystyle \scriptstyle {p}} is false or π {\displaystyle \scriptstyle {q}} is false," which is obviously true when and only when π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are both true. Thus we put
*3Β·01. π . π
. βΌ ( βΌ π β¨ βΌ π ) Df {\displaystyle \scriptstyle {p.q.=.\sim (\sim p\lor \sim q)\quad {\text{Df}}}}
where " π . π {\displaystyle \scriptstyle {p.q}}" is the logical product of π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}}.
*3Β·02. π β π β π
. π β π . π β π Df {\displaystyle \scriptstyle {p\supset q\supset r.=.p\supset q.q\supset r\quad {\text{Df}}}}
This definition serves merely to abbreviate proofs.
When we are given two asserted propositional functions " β’ . π π₯ {\displaystyle \scriptstyle {\vdash .\phi x}}" and " β’ . π π₯ {\displaystyle \scriptstyle {\vdash .\psi x}}," we shall have " β’ . π π₯ . π π₯ {\displaystyle \scriptstyle {\vdash .\phi x.\psi x}}" whenever π{\displaystyle \scriptstyle {\phi }} and π{\displaystyle \scriptstyle {\psi }} take arguments of the same type. This will be proved for any functions in *9; for the present, we are confined to elementary propositional functions of elementary propositions. In this case, the result is proved as follows:
By *1Β·7, βΌ π π {\displaystyle \scriptstyle {\sim \phi p}} and βΌ π π {\displaystyle \scriptstyle {\sim \psi p}} are elementary propositional functions, and therefore, by *1Β·72, βΌ π π β¨ βΌ π π {\displaystyle \scriptstyle {\sim \phi p\lor \sim \psi p}} is an elementary propositional function. Hence by *2Β·11, β’:βΌ π π β¨ βΌ π π . β¨ . βΌ ( βΌ π π β¨ βΌ π π ) {\displaystyle \scriptstyle {\vdash :\sim \phi p\lor \sim \psi p.\lor .\sim (\sim \phi p\lor \sim \psi p)}}.
Hence by *2Β·32 and *1Β·01, β’: . π π . β: π π . β . βΌ ( βΌ π π β¨ βΌ π π ) {\displaystyle \scriptstyle {\vdash :.\phi p.\supset :\psi p.\supset .\sim (\sim \phi p\lor \sim \psi p)}},
i.e. by *3Β·01, β’: . π π . β: π π . β . π π . π π {\displaystyle \scriptstyle {\vdash :.\phi p.\supset :\psi p.\supset .\phi p.\psi p}}.
Hence by *1Β·11, when we have " β’ . π π {\displaystyle \scriptstyle {\vdash .\phi p}}" and " β’ . π π {\displaystyle \scriptstyle {\vdash .\psi p}}" we have " β’ . π π . π π {\displaystyle \scriptstyle {\vdash .\phi p.\psi p}}." This proposition is *3Β·03. It is to be understood, like *1Β·72, as applying also to functions of two or more variables.
The above is the practically most useful form of the axiom of identification of real variables (cf. *1Β·72). In practice, when the restriction to elementary propositions and propositional functions has been removed, a convenient means by which two functions can often be recognized as taking arguments of the same type is the following:
If π π₯ {\displaystyle \scriptstyle {\phi x}} contains, in any way, a constituent π ( π₯ , π¦ , π§ , β¦ ) {\displaystyle \scriptstyle {\chi (x,y,z,\ldots )}} and π π₯ {\displaystyle \scriptstyle {\psi x}} contains, in any way, a constituent π ( π₯ , π’ , π£ , β¦ ) {\displaystyle \scriptstyle {\chi (x,u,v,\ldots )}}, then both π π₯ {\displaystyle \scriptstyle {\phi x}} and π π₯ {\displaystyle \scriptstyle {\psi x}} take arguments of the type of the argument π₯ {\displaystyle \scriptstyle {x}} in π ( π₯ , π¦ , π§ , β¦ ) {\displaystyle \scriptstyle {\chi (x,y,z,\ldots )}}, and therefore both π π₯ {\displaystyle \scriptstyle {\phi x}} and π π₯ {\displaystyle \scriptstyle {\psi x}} take arguments of the same type. Hence, in such a case, if both π π₯ {\displaystyle \scriptstyle {\phi x}} and π π₯ {\displaystyle \scriptstyle {\psi x}} can be asserted, so can π π₯ . π π₯ {\displaystyle \scriptstyle {\phi x.\psi x}}.
As an example of the use of this proposition, take the proof of *3Β·47. We there proveand β’: . π β π . π β π . β: π . π . β . π . π ( 1 ) β’: . π β π . π β π . β: π . π . β . π . π ( 2 ) {\displaystyle {\begin{array}{lr}\scriptstyle {\vdash :.p\supset r.q\supset s.\supset :p.q.\supset .q.r\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {\vdash :.p\supset r.q\supset s.\supset :q.r.\supset .r.s}&\scriptstyle {(2)}\end{array}}}
and what we wish to prove is π β π . π β π . β: π . π . β . π . π {\displaystyle \scriptstyle {p\supset r.q\supset s.\supset :p.q.\supset .r.s}},
which is *3Β·47. Now in (1) and (2), π {\displaystyle \scriptstyle {p}}, π {\displaystyle \scriptstyle {q}}, π {\displaystyle \scriptstyle {r}}, π {\displaystyle \scriptstyle {s}} are elementary propositions (as everywhere in Section A); hence by *1Β·7Β·71, applied repeatedly, " π β π . π β π . β: π . π . β . π . π {\displaystyle \scriptstyle {p\supset r.q\supset r.\supset :p.q.\supset .q.r}}" and " π β π . π β π . β: π . π . β . π . π {\displaystyle \scriptstyle {p\supset r.q\supset s.\supset :q.r.\supset .r.s}}" are elementary propositional functions. Hence by *3Β·03, we have β’:: π β π . π β π . β: π . π . β . π . π : . π β π . π β π . β: π . π . β . π . π {\displaystyle \scriptstyle {\vdash ::p\supset r.q\supset s.\supset :p.q.\supset .q.r:.p\supset r.q\supset s.\supset :q.r.\supset .r.s}},
whence the result follows by *3Β·43 and *3Β·33. The principal propositions of the present number are the following:
*3Β·2. β’: . π . β: π . β . π . π {\displaystyle \scriptstyle {\vdash :.p.\supset :q.\supset .p.q}}
I.e. " π {\displaystyle \scriptstyle {p}} implies that π {\displaystyle \scriptstyle {q}} implies π . π {\displaystyle \scriptstyle {p.q}}," i.e. if each of two propositions is true, so is their logical product.
*3Β·26. β’: π . π . β . π {\displaystyle \scriptstyle {\vdash :p.q.\supset .p}}
*3Β·27. β’: π . π . β . π {\displaystyle \scriptstyle {\vdash :p.q.\supset .q}}
I.e. if the logical product of two propositions is true, then each of the two propositions severally is true.
*3Β·3. β’: . π . π . β . π :β: π . β . π β π {\displaystyle \scriptstyle {\vdash :.p.q.\supset .r:\supset :p.\supset .q\supset r}}
I.e. if π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} jointly imply π {\displaystyle \scriptstyle {r}}, then π {\displaystyle \scriptstyle {p}} implies that π {\displaystyle \scriptstyle {q}} implies π {\displaystyle \scriptstyle {r}}. This principle (following Peano) will be called "exportation," because π {\displaystyle \scriptstyle {q}} is "exported" from the hypothesis. It will be referred to as "Exp."
*3Β·31. β’: . π . β . π β π :β: π . π . β . π {\displaystyle \scriptstyle {\vdash :.p.\supset .q\supset r:\supset :p.q.\supset .r}}
This is the correlative of the above, and will be called (following Peano) "importation" (referred to as "Imp").
*3Β·35. β’: π . π β π . β . π {\displaystyle \scriptstyle {\vdash :p.p\supset q.\supset .q}}
I.e. "if π {\displaystyle \scriptstyle {p}} is true, and π {\displaystyle \scriptstyle {q}} follows from it, then π {\displaystyle \scriptstyle {q}} is true." This will be called the "principle of assertion" (referred to as "Ass"). It differs from *1Β·1 by the fact that it does not apply only when π {\displaystyle \scriptstyle {p}} really is true, but requires merely the hypothesis that π {\displaystyle \scriptstyle {p}} is true.
*3Β·43. β’: . π β π . π β π . β: π . β . π . π {\displaystyle \scriptstyle {\vdash :.p\supset q.p\supset r.\supset :p.\supset .q.r}}
I.e. if a proposition implies each of two propositions, then it implies their logical product. This is called by Peano the "principle of composition." It will be referred to as "Comp."
*3Β·45. β’: . π β π . β: π . π . β . π . π {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :p.r.\supset .q.r}}
I.e. both sides of an implication may be multiplied by a common factor. This is called by Peano the "principle of the factor." It will be referred to as "Fact."
*3Β·47. β’: . π β π . π β π . β: π . π . β . π . π {\displaystyle \scriptstyle {\vdash :.p\supset r.q\supset s.\supset :p.q.\supset .r.s}}
I.e. if π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}} and π {\displaystyle \scriptstyle {r}} implies π {\displaystyle \scriptstyle {s}}, then π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} jointly imply π {\displaystyle \scriptstyle {r}} and π {\displaystyle \scriptstyle {s}} jointly. The law of contradiction, " β’ . βΌ ( π . βΌ π ) {\displaystyle \scriptstyle {\vdash .\sim (p.\sim p)}}," is proved in this number (*3Β·24); but in spite of its fame we have found few occasions for its use.
*3Β·01. π . π
. βΌ ( βΌ π β¨ βΌ π ) Df {\displaystyle \scriptstyle {p.q.=.\sim (\sim p\lor \sim q)\quad {\text{Df}}}}
*3Β·02. π β π β π
. π β π . π β π Df {\displaystyle \scriptstyle {p\supset q\supset r.=.p\supset q.q\supset r\quad {\text{Df}}}}
*3Β·03.Given two asserted elementary propositional functions " β’ . π π {\displaystyle \scriptstyle {\vdash .\phi p}}" and " β’ . π π {\displaystyle \scriptstyle {\vdash .\psi p}}" whose arguments are elementary propositions, we have β’ . π π . π π {\displaystyle \scriptstyle {\vdash .\phi p.\psi p}}.
Dem. β’ . β 1 β 7 β 72. β 2 β 11. ββ’:βΌ π π β¨ βΌ π π . β¨ βΌ ( βΌ π π β¨ βΌ π π ) ( 1 ) β’ . ( 1 ) . β 2 β 32. ( β 1 β 01 ) . ββ’: . π π . β: π π . β . βΌ ( βΌ π π β¨ βΌ π π ) ( 2 ) β’ . ( 2 ) . ( β 3 β 03 ) . ββ’: . π π . β: π π . β . π π . π π ( 3 ) β’ . ( 3 ) . β 1 β 11. ββ’ . Prop {\displaystyle {\begin{array}{lr}\scriptstyle {\vdash .1\cdot 7\cdot 72.2\cdot 11.\supset \vdash :\sim \phi p\lor \sim \psi p.\lor \sim (\sim \phi p\lor \sim \psi p)\quad }&\scriptstyle {(1)}\\scriptstyle {\vdash .(1).2\cdot 32.(1\cdot 01).\supset \vdash :.\phi p.\supset :\psi p.\supset .\sim (\sim \phi p\lor \sim \psi p)}&\scriptstyle {(2)}\\scriptstyle {\vdash .(2).(3\cdot 03).\supset \vdash :.\phi p.\supset :\psi p.\supset .\phi p.\psi p}&\scriptstyle {(3)}\\scriptstyle {\vdash .(3).1\cdot 11.\supset \vdash .{\text{Prop}}}\end{array}}}
3Β·1. β’: π . π . β . βΌ ( βΌ π β¨ βΌ π ) [ Id . ( β 3 β 01 ) ] {\displaystyle \scriptstyle {\vdash :p.q.\supset .\sim (\sim p\lor \sim q)\quad [{\text{Id}}.(3\cdot 01)]}}
3Β·11. β’:βΌ ( βΌ π β¨ βΌ π ) . β . π . π [ Id . ( β 3 β 01 ) ] {\displaystyle \scriptstyle {\vdash :\sim (\sim p\lor \sim q).\supset .p.q\quad [{\text{Id}}.(3\cdot 01)]}}
3Β·12. β’:βΌ π . β¨ . βΌ π . β¨ . π . π [ β 2 β 11 βΌ π β¨ βΌ π π ] {\displaystyle \scriptstyle {\vdash :\sim p.\lor .\sim q.\lor .p.q\quad \left[2\cdot 11{\frac {\sim p\lor \sim q}{p}}\right]}}
3Β·13. β’:βΌ ( π . π ) . β . βΌ π β¨ βΌ π [ β 3 β 11. Transp ] {\displaystyle \scriptstyle {\vdash :\sim (p.q).\supset .\sim p\lor \sim q\quad [3\cdot 11.{\text{Transp}}]}}
3Β·14. β’:βΌ π β¨ βΌ π . β . βΌ ( π . π ) [ β 3 β 1. Transp ] {\displaystyle \scriptstyle {\vdash :\sim p\lor \sim q.\supset .\sim (p.q)\quad [3\cdot 1.{\text{Transp}}]}}
3Β·2. β’: . π . β: π . β . π . π [ β 3 β 12 ] {\displaystyle \scriptstyle {\vdash :.p.\supset :q.\supset .p.q\qquad [3\cdot 12]}}
3Β·21. β’: . π . β: π . β . π . π [ β 3 β 2. Comm ] {\displaystyle \scriptstyle {\vdash :.q.\supset :p.\supset .p.q\qquad [3\cdot 2.{\text{Comm}}]}}
*3Β·22. β’: π . π . β . π . π {\displaystyle \scriptstyle {\vdash :p.q.\supset .q.p}}
This is one form of the commutative law for logical multiplication, A more complete form is given in *4Β·3.
Dem. [ β 3 β 13 π , π π , π ] β’:βΌ ( π . π ) . β . βΌ π β¨ βΌ π . [ Perm ] β . βΌ π β¨ βΌ π . [ β 3 β 14 ] β . βΌ ( π . π ) ( 1 ) β’ . ( 1 ) . Transp . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\left[3\cdot 13{\frac {q,p}{p,q}}\right]\quad \vdash :\sim (q.p).}&\scriptstyle {\supset .\sim q\lor \sim p.}\\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\supset .\sim p\lor \sim q.}\\scriptstyle {[3\cdot 14]}&\scriptstyle {\supset .\sim (p.q)\qquad \qquad (1)}\\scriptstyle {\vdash .(1).{\text{Transp}}.\supset \vdash .{\text{Prop}}}\end{array}}}
Note that, in the above proof, "(1)" stands for the proposition " βΌ ( π . π ) . β . βΌ ( π . π ) {\displaystyle \scriptstyle {\sim (q.p).\supset .\sim (p.q)}},"
as was explained in the proof of *2Β·31. *3Β·24. β’ . βΌ ( π . βΌ π ) {\displaystyle \scriptstyle {\vdash .\sim (p.\sim p)}}
Dem. [ β 2 β 11 βΌ π π ] β’ . βΌ π β¨ βΌ ( βΌ π ) . β [ β 3 β 14 βΌ π π ] β’ . βΌ ( π . βΌ π ) {\displaystyle {\begin{array}{ll}\scriptstyle {\left[2\cdot 11{\frac {\sim p}{p}}\right]\quad }&\scriptstyle {\vdash .\sim p\lor \sim (\sim p).\supset }\\scriptstyle {\left[3\cdot 14{\frac {\sim p}{q}}\right]}&\scriptstyle {\vdash .\sim (p.\sim p)}\end{array}}}
The above is the law of contradiction.
*3Β·26. β’: π . π . β . π {\displaystyle \scriptstyle {\vdash :p.q.\supset .p}}
Dem. [ β 2 β 02 π , π π , π ]
β’: π . β . π β π ( 1 ) [ ( 1 ) . ( β 1 β 01 ) ]
β’:βΌ π . β¨ . βΌ π β¨ π : [ β 2 β 31 ] ββ’:βΌ π β¨ βΌ π . β¨ . π : [ β 2 β 53 βΌ π β¨ βΌ π , π π , π ] ββ’:βΌ ( βΌ π β¨ βΌ π ) . β . π ( 2 ) [ ( 2 ) . ( β 3 β 01 ) ]
β’: π . π . β . π {\displaystyle {\begin{array}{llr}\scriptstyle {\left[2\cdot 02{\frac {q,p}{p,q}}\right]}&\scriptstyle {~\vdash :p.\supset .q\supset p\qquad }&\scriptstyle {(1)}\\scriptstyle {[(1).(1\cdot 01)]}&\scriptstyle {~\vdash :\sim p.\lor .\sim q\lor p:}\\scriptstyle {[2\cdot 31]}&\scriptstyle {\supset \vdash :\sim p\lor \sim q.\lor .p:}\\scriptstyle {\left[2\cdot 53{\frac {\sim p\lor \sim q,p}{p,\quad q}}\right]}&\scriptstyle {\supset \vdash :\sim (\sim p\lor \sim q).\supset .p\qquad }&\scriptstyle {(2)}\\scriptstyle {[(2).(*3\cdot 01)]}&\scriptstyle {~\vdash :p.q.\supset .p}\end{array}}}
*3Β·27. β’: π . π . β . π {\displaystyle \scriptstyle {\vdash :p.q.\supset .q}}
Dem. [ β 3 β 22 ] β’: π . π . β . π . π . [ β 3 β 26 π , π π , π ] β . π :ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {[3\cdot 22]\quad \vdash :p.q.}&\scriptstyle {\supset .q.p.}\\scriptstyle {\left[3\cdot 26{\frac {q,p}{p,q}}\right]}&\scriptstyle {\supset .q:\supset \vdash .{\text{Prop}}}\end{array}}}
3Β·26Β·27 will both be called the "principle of simplification," like *2Β·02, from which they are deduced. They will be referred to as "Simp." *3Β·3. β’: . π . π . β . π :β: π . β . π β π {\displaystyle \scriptstyle {\vdash :.p.q.\supset .r:\supset :p.\supset .q\supset r}}
Dem. [ Id . ( β 3 β 01 ) ] β’: . π . π . β . π : β:βΌ ( βΌ π β¨ βΌ π ) . β . π : [ Transp ] β:βΌ π . β . βΌ π β¨ βΌ π : [ Id . ( β 1 β 01 ) ] β:βΌ π . β . π ββΌ π : [ Comm ] β: π . β . βΌ π ββΌ π : [ Transp . Syll ] β: π . β . π β π : . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {[{\text{Id}}.(3\cdot 01)]\quad \vdash :.p.q.\supset .r:}&\scriptstyle {\supset :\sim (\sim p\lor \sim q).\supset .r:}\\scriptstyle {[{\text{Transp}}]}&\scriptstyle {\supset :\sim r.\supset .\sim p\lor \sim q:}\\scriptstyle {[{\text{Id}}.(1\cdot 01)]}&\scriptstyle {\supset :\sim r.\supset .p\supset \sim q:}\\scriptstyle {[{\text{Comm}}]}&\scriptstyle {\supset :p.\supset .\sim r\supset \sim q:}\\scriptstyle {[{\text{Transp}}.{\text{Syll}}]}&\scriptstyle {\supset :p.\supset .q\supset r:.\supset \vdash .{\text{Prop}}}\end{array}}}
*3Β·31. β’: . π . β . π β π :β: π . π . β . π {\displaystyle \scriptstyle {\vdash :.p.\supset .q\supset r:\supset :p.q.\supset .r}}
Dem. [ Id . ( β 1 β 01 ) ] β’: . π . β . π β π : β:βΌ π . β¨ . βΌ π β¨ π : [ β 2 β 31 ] β:βΌ π β¨ βΌ π . β¨ . π : [ β 2 β 53 βΌ π β¨ βΌ π , π π , π ] β:βΌ ( βΌ π β¨ βΌ π ) . β . π : [ Id . ( β 3 β 01 ) ] β: π . π . β . π : . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {[{\text{Id}}.(1\cdot 01)]\quad \vdash :.p.\supset .q\supset r:}&\scriptstyle {\supset :\sim p.\lor .\sim q\lor r:}\\scriptstyle {[2\cdot 31]}&\scriptstyle {\supset :\sim p\lor \sim q.\lor .r:}\\scriptstyle {\left[2\cdot 53{\frac {\sim p\lor \sim q,r}{p,\quad q}}\right]}&\scriptstyle {\supset :\sim (\sim p\lor \sim q).\supset .r:}\\scriptstyle {[{\text{Id}}.(3\cdot 01)]}&\scriptstyle {\supset :p.q.\supset .r:.\supset \vdash .{\text{Prop}}}\end{array}}}
*3Β·33. β’: π β π . π β π . β . π β π [ Syll . Imp ] {\displaystyle \scriptstyle {\vdash :p\supset q.q\supset r.\supset .p\supset r\quad [{\text{Syll}}.{\text{Imp}}]}}
*3Β·34. β’: π β π . π β π . β . π β π Syll . Imp ] {\displaystyle \scriptstyle {\vdash :q\supset r.p\supset q.\supset .p\supset r\quad {\text{Syll}}.{\text{Imp}}]}}
These two propositions will hereafter be referred to as "Syll"; they are usually more convenient than either *2Β·05 or *2Β·06.
3Β·35. β’: π . π β π . β . π [ β 2 β 27. Imp ] {\displaystyle \scriptstyle {\vdash :p.p\supset q.\supset .q\quad [2\cdot 27.{\text{Imp}}]}}
*3Β·37. β’: . π . π . β . π :β: π . βΌ π . β . βΌ π {\displaystyle \scriptstyle {\vdash :.p.q.\supset .r:\supset :p.\sim r.\supset .\sim q}}
Dem. β’ . Transp . ββ’: π β π . β . βΌ π ββΌ π : [ Syll ] ββ’: . π . β . π β π :β: π . β . βΌ π ββΌ π ( 1 ) β’ . Exp . ββ’: . π . π . β . π :β: π . β . π β π ( 2 ) β’ . Imp . ββ’: . π . β . βΌ π ββΌ π :β: π . βΌ π . β . βΌ π ( 3 ) β’ . ( 2 ) . ( 1 ) . ( 3 ) . Syll . ββ’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .{\text{Transp}}.}&\scriptstyle {\supset \vdash :q\supset r.\supset .\sim r\supset \sim q:}\\scriptstyle {[{\text{Syll}}]}&\scriptstyle {\supset \vdash :.p.\supset .q\supset r:\supset :p.\supset .\sim r\supset \sim q\qquad }&\scriptstyle {(1)}\\scriptstyle {\vdash .{\text{Exp}}.}&\scriptstyle {\supset \vdash :.p.q.\supset .r:\supset :p.\supset .q\supset r}&\scriptstyle {(2)}\\scriptstyle {\vdash .{\text{Imp}}.}&\scriptstyle {\supset \vdash :.p.\supset .\sim r\supset \sim q:\supset :p.\sim r.\supset .\sim q}&\scriptstyle {(3)}\\scriptstyle {\vdash .(2).(1).}&\scriptstyle {(3).{\text{Syll}}.\supset \vdash .{\text{Prop}}}\end{array}}}
This is another form of transposition.
3Β·4. β’: π . π . β . π β π [ β 2 β 51. Transp . ( β 1 β 01. β 3 β 01 ) ] {\displaystyle \scriptstyle {\vdash :p.q.\supset .p\supset q\qquad [2\cdot 51.{\text{Transp}}.(1\cdot 01.3\cdot 01)]}}
3Β·41. β’: . π β π . β: π . π . β . π [ β 3 β 26. Syll ] {\displaystyle \scriptstyle {\vdash :.p\supset r.\supset :p.q.\supset .r\quad [3\cdot 26.{\text{Syll}}]}}
3Β·42. β’: . π β π . β: π . π . β . π [ β 3 β 27. Syll ] {\displaystyle \scriptstyle {\vdash :.q\supset r.\supset :p.q.\supset .r\quad [3\cdot 27.{\text{Syll}}]}}
*3Β·43. β’: . π β π . π β π . β: π . β . π . π {\displaystyle \scriptstyle {\vdash :.p\supset q.p\supset r.\supset :p.\supset .q.r}}
Dem.
β’
.
β
3
β
2.
ββ’:
.
π
.
β:
π
.
β
.
π
.
π
(
1
)
β’
.
(
1
)
.
Syll
.
ββ’::
π
β
π
.
β:
.
π
.
β:
π
.
β
.
π
.
π
:
.
[
β
2
β
77
]
β:
.
π
β
π
.
β:
π
.
β
.
π
.
π
(
2
)
β’
.
(
2
)
.
Imp
.
ββ’
.
Prop
{\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .3\cdot 2.\supset \vdash :.q.\supset :r.\supset }&\scriptstyle {.q.r}&\scriptstyle {(1)}\\scriptstyle {\vdash .(1).{\text{Syll}}.\supset \vdash ::p\supset q.}&\scriptstyle {\supset :.p.\supset :r.\supset .q.r:.}\\scriptstyle {[2\cdot 77]}&\scriptstyle {\supset :.p\supset r.\supset :p.\supset .q.r\qquad }&\scriptstyle {(2)}\\scriptstyle {\vdash .(2).{\text{Imp}}.\supset \vdash .{\text{Prop}}}\end{array}}}
*3Β·44. β’: . π β π . π β π . β: π β¨ π . β . π {\displaystyle \scriptstyle {\vdash :.q\supset p.r\supset p.\supset :q\lor r.\supset .p}}
This principle is analogous to *3Β·43. The analogy between *3Β·43 and *3Β·44 is of a sort which generally subsists between formulae concerning products and formulae concerning sums.
Dem. β’ . Syll . ββ’: . βΌ π β π . π β π . β:βΌ π β π : [ β 2 β 6 ]
β: π β π . β . π ( 1 ) β’ . ( 1 ) . Exp . ββ’::βΌ π β π . β: . π β π . β: π β π . β . π : . [ Comm . Imp ] β: . π β π . π β π . β . π ( 2 ) β’ . ( 2 ) . Comm . ββ’: . π β π . π β π . β:βΌ π β π . β . π : . [ β 2 β 53. Syll ] ββ’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .{\text{Syll}}.\supset \vdash :.\sim q\supset r.r\supset p}&\scriptstyle {.\supset :\sim q\supset p:}\\scriptstyle {[2\cdot 6]}&\scriptstyle {~\supset :q\supset p.\supset .p}&\scriptstyle {(1)}\\scriptstyle {\vdash .(1).{\text{Exp}}.\supset \vdash ::\sim q\supset r.}&\scriptstyle {\supset :.r\supset p.\supset :q\supset p.\supset .p:.}\\scriptstyle {[{\text{Comm}}.{\text{Imp}}]}&\scriptstyle {\supset :.q\supset p.r\supset p.\supset .p\qquad }&\scriptstyle {(2)}\\scriptstyle {\vdash .(2).{\text{Comm}}.\supset \vdash :.q\supset p.}&\scriptstyle {r\supset p.\supset :\sim q\supset r.\supset .p:.}\\scriptstyle {[2\cdot 53.{\text{Syll}}]\quad \supset \vdash .{\text{Prop}}}\end{array}}}
*3Β·45. β’: . π β π . β: π . π . β . π . π {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset :p.r.\supset .q.r}}
This principle shows that we may multiply both sides of an implication by a common factor; hence it is called by Peano the "principle of the factor." We shall refer to it as "Fact." It is the analogue, for multiplication, of the primitive proposition *1Β·6.
Dem. β’ . Syll βΌ π π . ββ’: . π β π . β: π ββΌ π . β . π ββΌ π : [ Transp ] β:βΌ ( π ββΌ π ) . β . βΌ ( π ββΌ π ) : .
[ Id . ( β 1 β 01. β 3 β 01 ) ] ββ’ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{ll}\scriptstyle {\vdash .{\text{Syll}}{\frac {\sim r}{r}}.\supset \vdash :.p\supset q.}&\scriptstyle {\supset :q\supset \sim r.\supset .p\supset \sim r:}\\scriptstyle {[{\text{Transp}}]}&\scriptstyle {\supset :\sim (p\supset \sim r).\supset .\sim (q\supset \sim r):.}\end{array}}\&\scriptstyle {~[{\text{Id}}.(1\cdot 01.3\cdot 01)]\supset \vdash .{\text{Prop}}}\end{aligned}}}
*3Β·47. β’: . π β π . π β π . β: π . π . β . π . π {\displaystyle \scriptstyle {\vdash :.p\supset r.q\supset s.\supset :p.q.\supset .r.s}}
This proposition, or rather its analogue for classes, was proved by Leibniz, and evidently pleased him, since he calls it "præclarum theorema[11]."
Dem. β’ . β 3 β 26. ββ’: . π β π . π β π . β: π β π : [ Fact ] β: π . π . β . π . π : [ β 3 β 22 ] β: π . π . β . π . π ( 1 ) β’ . β 3 β 27. ββ’: . π β π . π β π . β: π β π : [ Fact ] β: π . π . β . π . π : [ β 3 β 22 ] β: π . π . β . π . π ( 2 )
β’ . ( 1 ) . ( 2 ) . β 3 β 03. β 2 β 83. β β’: . π β π . π β π . β: π . π . β . π . π : . ββ’ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{llr}\scriptstyle {\vdash .3\cdot 26.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :p\supset r:}\\scriptstyle {[{\text{Fact}}]}&\scriptstyle {\supset :p.q.\supset .r.q:}\\scriptstyle {[3\cdot 22]}&\scriptstyle {\supset :p.q.\supset .q.r\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {\vdash .3\cdot 27.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :q\supset s:}\\scriptstyle {[{\text{Fact}}]}&\scriptstyle {\supset :q.r.\supset .s.r:}\\scriptstyle {[3\cdot 22]}&\scriptstyle {\supset :q.r.\supset .r.s}&\scriptstyle {(2)}\end{array}}\&\scriptstyle {~\vdash .(1).(2).3\cdot 03.2\cdot 83.\supset }\&\scriptstyle {\qquad \qquad \vdash :.p\supset r.q\supset s.\supset :p.q.\supset .r.s:.\supset \vdash .{\text{Prop}}}\end{aligned}}}
*3Β·48. β’: . π β π . π β π . β: π β¨ π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :.p\supset r.q\supset s.\supset :p\lor q.\supset .r\lor s}}
This theorem is the analogue of *3Β·47.
Dem. β’ . β 3 β 26. ββ’: . π β π . π β π . β: π β π : [ Sum ] β: π β¨ π . β . π β¨ π : [ Perm ] β: π β¨ π . β . π β¨ π ( 1 ) β’ . β 3 β 27. ββ’: . π β π . π β π . β: π β π : [ Sum ] β: π β¨ π . β . π β¨ π : [ Perm ] β: π β¨ π . β . π β¨ π ( 2 )
β’ . ( 1 ) . ( 2 ) . β 2 β 83. β β’: . π β π . π β π . β: π β¨ π . β . π β¨ π : . ββ’ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{llr}\scriptstyle {\vdash .3\cdot 26.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :p\supset r:}\\scriptstyle {[{\text{Sum}}]}&\scriptstyle {\supset :p\lor q.\supset .r\lor q:}\\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\supset :p\lor q.\supset .q\lor r\qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {\vdash .3\cdot 27.\supset \vdash :.p\supset r.q\supset s.}&\scriptstyle {\supset :q\supset s:}\\scriptstyle {[{\text{Sum}}]}&\scriptstyle {\supset :q\lor r.\supset .s\lor r:}\\scriptstyle {[{\text{Perm}}]}&\scriptstyle {\supset :q\lor r.\supset .r\lor s}&\scriptstyle {(2)}\end{array}}\&\scriptstyle {~\vdash .(1).(2).*2\cdot 83.\supset }\&\scriptstyle {\qquad \qquad \vdash :.p\supset r.q\supset s.\supset :p\lor q.\supset .r\lor s:.\supset \vdash .{\text{Prop}}}\end{aligned}}}
*4. Equivalence and Formal Rules. Summary of *4.
In this number, we shall be concerned with rules analogous, more or less, to those of ordinary algebra. It is from these rules that the usual "calculus of formal logic" starts. Treated as a "calculus," the rules of deduction are capable of many other interpretations. But all other interpretations depend upon the one here considered, since in all of them we deduce consequences from our rules, and thus presuppose the theory of deduction. One very simple interpretation of the "calculus" is as follows: The entities considered are to be numbers which are all either 0 or 1; " π β π {\displaystyle \scriptstyle {p\supset q}}" is to have the value 0 if π {\displaystyle \scriptstyle {p}} is 1 and π {\displaystyle \scriptstyle {q}} is 0; otherwise it is to have the value 1; βΌ π {\displaystyle \scriptstyle {\sim p}} is to be 1 if π {\displaystyle \scriptstyle {p}} is 0, and 0 if π {\displaystyle \scriptstyle {p}} is 1; π . π {\displaystyle \scriptstyle {p.q}} is to be 1 if π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are both 1, and is to be 0 in any other case; π β¨ π {\displaystyle \scriptstyle {p\lor q}} is to be 0 if π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are both 0, and is to be 1 in any other case; and the assertion-sign is to mean that what follows has the value 1. Symbolic logic considered as a calculus has undoubtedly much interest on its own account; but in our opinion this aspect has hitherto been too much emphasized, at the expense of the aspect in which symbolic logic is merely the most elementary part of mathematics, and the logical pre-requisite of all the rest. For this reason, we shall only deal briefly with what is required for the algebra of symbolic logic.
When each of two propositions implies the other, we say that the two are equivalent, which we write " π β‘ π {\displaystyle \scriptstyle {p\equiv q}}." We put
*4Β·01. π β‘ π
. π β π β π Df {\displaystyle \scriptstyle {p\equiv q.=.p\supset q\supset p\quad {\text{Df}}}}
It is obvious that two propositions are equivalent when, and only when, both are true or both are false. Following Frege, we shall call the truth-value of a proposition truth if it is true, and falsehood if it is false. Thus two propositions are equivalent when they have the same truth-value.
It should be observed that, if π β‘ π {\displaystyle \scriptstyle {p\equiv q}}, π {\displaystyle \scriptstyle {q}} may be substituted for π {\displaystyle \scriptstyle {p}} without altering the truth-value of any function of π {\displaystyle \scriptstyle {p}} which involves no primitive ideas except those enumerated in *1. This can be proved in each separate case, but not generally, because we have no means of specifying (with our apparatus of primitive ideas) that a function is one which can be built up out of these ideas alone. We shall give the name of a truth-function to a function π ( π ) {\displaystyle \scriptstyle {f(p)}} whose argument is a proposition, and whose truth-value depends only upon the truth-value of its argument. All the functions of propositions with which we shall be specially concerned will be truth-functions, i.e. we shall have π β‘ π . β . π ( π ) β‘ π ( π ) {\displaystyle \scriptstyle {p\equiv q.\supset .f(p)\equiv f(q)}}.
The reason of this is, that the functions of propositions with which we deal are all built up by means of the primitive ideas of *1. But it is not a universal characteristic of functions of propositions to be truth-functions. For example, " π΄ {\displaystyle \scriptstyle {A}} believes π {\displaystyle \scriptstyle {p}}" may be true for one true value of π {\displaystyle \scriptstyle {p}} and false for another. The principal propositions of this number are the following:
*4Β·1. β’: π β π . β‘ . βΌ π ββΌ π {\displaystyle \scriptstyle {\vdash :p\supset q.\equiv .\sim q\supset \sim p}}
*4Β·11. β’: π β‘ π . β‘ . βΌ π β‘βΌ π {\displaystyle \scriptstyle {\vdash :p\equiv q.\equiv .\sim p\equiv \sim q}}
These are both forms of the "principle of transposition."
*4Β·13. β’ . π β‘βΌ ( βΌ π ) {\displaystyle \scriptstyle {\vdash .p\equiv \sim (\sim p)}}
This is the principle of double negation, i.e. a proposition is equivalent to the falsehood of its negation.
*4Β·2. β’ . π β‘ π {\displaystyle \scriptstyle {\vdash .p\equiv p}}
*4Β·21. β’: π β‘ π . β‘ . π β‘ π {\displaystyle \scriptstyle {\vdash :p\equiv q.\equiv .q\equiv p}}
*4Β·22. β’: π β‘ π . π β‘ π . β . π β‘ π {\displaystyle \scriptstyle {\vdash :p\equiv q.q\equiv r.\supset .p\equiv r}}
These propositions assert that equivalence is reflexive, symmetrical and transitive.
*4Β·24. β’: π . β‘ . π β¨ π {\displaystyle \scriptstyle {\vdash :p.\equiv .p\lor p}}
I.e. π {\displaystyle \scriptstyle {p}} is equivalent to " π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {p}}" and to " π {\displaystyle \scriptstyle {p}} or π {\displaystyle \scriptstyle {p}}," which are two forms of the law of tautology, and are the source of the principal differences between the algebra of symbolic logic and ordinary algebra.
*4Β·3. β’: π . π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :p.q.\equiv .q.p}}
This is the commutative law for the product of propositions.
*4Β·31. β’: π β¨ π . β‘ . π β¨ π {\displaystyle \scriptstyle {\vdash :p\lor q.\equiv .q\lor p}}
This is the commutative law for the sum of propositions.
The associative laws for multiplication and addition of propositions, namely
*4Β·32. β’: ( π . π ) . π . β‘ . π . ( π . π ) {\displaystyle \scriptstyle {\vdash :(p.q).r.\equiv .p.(q.r)}}
*4Β·33. β’: ( π β¨ π ) β¨ π . β‘ . π β¨ ( π β¨ π ) {\displaystyle \scriptstyle {\vdash :(p\lor q)\lor r.\equiv .p\lor (q\lor r)}}
The distributive law in the two forms
*4Β·4. β’: . π . π β¨ π . β‘: π . π . β¨ . π . π {\displaystyle \scriptstyle {\vdash :.p.q\lor r.\equiv :p.q.\lor .p.r}}
*4Β·41. β’: π β¨ . π . π :β‘ . π β¨ π . π β¨ π {\displaystyle \scriptstyle {\vdash :p\lor .q.r:\equiv .p\lor q.p\lor r}}
The second of these forms has no analogue in ordinary algebra.
*4Β·71. β’: . π β π . β‘: π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :.p\supset q.\equiv :p.\equiv .p.q}}
I.e. π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}} when, and only when, π {\displaystyle \scriptstyle {p}} is equivalent to π . π {\displaystyle \scriptstyle {p.q}}. This proposition is used constantly; it enables us to replace any implication by an equivalence.
*4Β·73. β’: . π . β: π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :.q.\supset :p.\equiv .p.q}}
I.e. a true factor may be dropped from or added to a proposition without altering the truth-value of the proposition.
4Β·01. π β‘ π
. π β π . π β π Df {\displaystyle \scriptstyle {p\equiv q.=.p\supset q.q\supset p\quad {\text{Df}}}} *4Β·02. π β‘ π β‘ π
. π β‘ π . π β‘ π Df {\displaystyle \scriptstyle {p\equiv q\equiv r.=.p\equiv q.q\equiv r\quad {\text{Df}}}}
This definition serves merely to provide a convenient abbreviation.
4Β·1. β’: π β π . β‘ . βΌ π ββΌ π {\displaystyle \scriptstyle {\vdash :p\supset q.\equiv .\sim q\supset \sim p}} [ β 2 β 16 β 17 ] {\displaystyle \scriptstyle {[2\cdot 16\cdot 17]}} 4Β·11. β’: π β‘ π . β‘ . βΌ π β‘βΌ π {\displaystyle \scriptstyle {\vdash :p\equiv q.\equiv .\sim p\equiv \sim q}} [ β 2 β 16 β 17. β 3 β 47 β 22 ] {\displaystyle \scriptstyle {[2\cdot 16\cdot 17.*3\cdot 47\cdot 22]}} *4Β·12. β’: π β‘βΌ π . β‘ . π β‘βΌ π {\displaystyle \scriptstyle {\vdash :p\equiv \sim q.\equiv .q\equiv \sim p}} [ β 2 β 03 β 15 ] {\displaystyle \scriptstyle {[*2\cdot 03\cdot 15]}}
4Β·13. β’ . π β‘βΌ ( βΌ π ) {\displaystyle \scriptstyle {\vdash .p\equiv \sim (\sim p)}} [ β 2 β 12 β 14 ] {\displaystyle \scriptstyle {[*2\cdot 12\cdot 14]}} *4Β·14. β’: . π . π . β . π :β‘: π . βΌ π . β . βΌ π {\displaystyle \scriptstyle {\vdash :.p.q.\supset .r:\equiv :p.\sim r.\supset .\sim q}} [ β 3 β 37. β 4 β 13 ] {\displaystyle \scriptstyle {[3\cdot 37.4\cdot 13]}}
4Β·15. β’: . π . π . β . βΌ π :β‘: π . π . β . βΌ π {\displaystyle \scriptstyle {\vdash :.p.q.\supset .\sim r:\equiv :q.r.\supset .\sim p}} [ β 3 β 22. β 4 β 13 β 14 ] {\displaystyle \scriptstyle {[3\cdot 22.*4\cdot 13\cdot 14]}}
4Β·2. β’ . π β‘ π {\displaystyle \scriptstyle {\vdash .p\equiv p}} [ Id . β 3 β 2 ] {\displaystyle \scriptstyle {[{\text{Id}}.3\cdot 2]}} 4Β·21. β’: π β‘ π . β‘ . π β‘ π {\displaystyle \scriptstyle {\vdash :p\equiv q.\equiv .q\equiv p}} [ β 3 β 22 ] {\displaystyle \scriptstyle {[3\cdot 22]}} 4Β·22. β’: π β‘ π . π β‘ π . β . π β‘ π {\displaystyle \scriptstyle {\vdash :p\equiv q.q\equiv r.\supset .p\equiv r}} Dem. β’ . β 3 β 26. ββ’: π β‘ π . π β‘ π . β . π β‘ π . [ β 3 β 26 ] β . π β π ( 1 ) β’ . β 3 β 27. ββ’: π β‘ π . π β‘ π . β . π β‘ π . [ β 3 β 26 ] β . π β π ( 2 ) β’ . ( 1 ) . ( 2 ) . β 2 β 83. ββ’: π β‘ π . π β‘ π . β . π β π ( 3 ) β’ . β 3 β 27. ββ’: π β‘ π . π β‘ π . β . π β‘ π . [ β 3 β 27 ] β . π β π ( 4 ) β’ . β 3 β 26. ββ’: π β‘ π . π β‘ π . β . π β‘ π . [ β 3 β 27 ] β . π β π ( 5 ) β’ . ( 4 ) . ( 5 ) . β 2 β 83. ββ’: π β‘ π . π β‘ π . β . π β π ( 6 ) β’ . ( 3 ) . ( 6 ) . Comp . ββ’ . Prop {\displaystyle {\begin{array}{lllr}\scriptstyle {\vdash .3\cdot 26.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .p\equiv q.}\\scriptstyle {[3\cdot 26]}&&\scriptstyle {\supset .p\supset q\qquad }&\scriptstyle {(1)}\\scriptstyle {\vdash .3\cdot 27.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .q\equiv r.}\\scriptstyle {[3\cdot 26]}&&\scriptstyle {\supset .q\supset r}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).2\cdot 83.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .p\supset r}&\scriptstyle {(3)}\\scriptstyle {\vdash .3\cdot 27.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .q\equiv r.}\\scriptstyle {[3\cdot 27]}&&\scriptstyle {\supset .r\supset q}&\scriptstyle {(4)}\\scriptstyle {\vdash .3\cdot 26.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .p\equiv q.}\\scriptstyle {[3\cdot 27]}&&\scriptstyle {\supset .q\supset p}&\scriptstyle {(5)}\\scriptstyle {\vdash .(4).(5).2\cdot 83.}&\scriptstyle {\supset \vdash :p\equiv q.q\equiv r.}&\scriptstyle {\supset .r\supset p}&\scriptstyle {(6)}\\scriptstyle {\vdash .(3).(6).{\text{Comp}}.}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}}
Note. The above three propositions show that the relation of equivalence is reflexive (4Β·2), symmetrical (4Β·21), and transitive (*4Β·22). Implication is reflexive and transitive, but not symmetrical. The properties of being symmetrical, transitive, and (at least within a certain field) reflexive are essential to any relation which is to have the formal characters of equality.
4Β·24. β’: π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :p.\equiv .p.p}} Dem. β’ . β 3 β 26. ββ’: π . π . β . π ( 1 ) β’ . β 3 β 2. ββ’: . π . β: π . β . π . π : [ β 2 β 43 ] ββ’: π . β . π . π ( 2 )
β’ . ( 1 ) . ( 2 ) . β 3 β 2. ββ’ . Prop {\displaystyle {\begin{aligned}&{\begin{array}{llr}\scriptstyle {\vdash .3\cdot 26.}&\scriptstyle {\supset \vdash :p.p.\supset .p\qquad \qquad \qquad \qquad }&\scriptstyle {(1)}\\scriptstyle {\vdash .3\cdot 2.}&\scriptstyle {\supset \vdash :.p.\supset :p.\supset .p.p:}\\scriptstyle {[2\cdot 43]}&\scriptstyle {\supset \vdash :p.\supset .p.p}&\scriptstyle {(2)}\end{array}}\&\scriptstyle {~\vdash .(1).(2).3\cdot 2.\supset \vdash .{\text{Prop}}}\end{aligned}}}
4Β·25. β’: π . β‘ . π β¨ π [ Taut . Add π π ] {\displaystyle \scriptstyle {\vdash :p.\equiv .p\lor p\quad \left[{\text{Taut}}.{\text{Add}}{\frac {p}{q}}\right]}} Note. *4Β·24Β·25 are two forms of the law of tautology, which is what chiefly distinguishes the algebra of symbolic logic from ordinary algebra.
4Β·3. β’: π . π . β‘ . π . π [ β 3 β 22 ] {\displaystyle \scriptstyle {\vdash :p.q.\equiv .q.p\quad [*3\cdot 22]}} Note. Whenever we have, whatever values π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} may have, π ( π , π ) . β . π ( π , π ) {\displaystyle \scriptstyle {\phi (p,q).\supset .\phi (q,p)}},
we have also π ( π , π ) . β‘ . π ( π , π ) {\displaystyle \scriptstyle {\phi (p,q).\equiv .\phi (q,p)}}.
For { π ( π , π ) . β . π ( π , π ) } π , π π , π . β: π ( π , π ) . β . π ( π , π ) {\displaystyle \scriptstyle {{\phi (p,q).\supset .\phi (q,p)}{\frac {q,p}{p,q}}.\supset :\phi (q,p).\supset .\phi (p,q)}}.
4Β·31.
β’:
π
β¨
π
.
β‘
.
π
β¨
π
[
Perm
]
{\displaystyle \scriptstyle {\vdash :p\lor q.\equiv .q\lor p\quad [{\text{Perm}}]}}
4Β·32.
β’:
(
π
.
π
)
.
π
.
β‘
.
π
.
(
π
.
π
)
{\displaystyle \scriptstyle {\vdash :(p.q).r.\equiv .p.(q.r)}}
Dem.
β’
.
β
4
β
15.
ββ’:
.
π
.
π
.
β
.
βΌ
π
:
β‘:
π
.
π
.
β
.
βΌ
π
:
[
β
4
β
12
]
β‘:
π
.
β
.
βΌ
(
π
.
π
)
(
1
)
β’
.
(
1
)
.
β
4
β
11.
ββ’:βΌ
(
π
.
π
.
β
.
βΌ
π
)
.
β‘
.
βΌ
{
π
.
β
.
βΌ
(
π
.
π
)
}
:
[
(
β
1
β
01.
β
3
β
01
)
]
ββ’
.
Prop
{\displaystyle {\begin{array}{lllr}\scriptstyle {\vdash .4\cdot 15.}&\scriptstyle {\supset \vdash :.p.q.\supset .\sim r:}&\scriptstyle {\equiv :q.r.\supset .\sim p:}\\scriptstyle {[4\cdot 12]}&&\scriptstyle {\equiv :p.\supset .\sim (q.r)\qquad }&\scriptstyle {(1)}\\scriptstyle {\vdash .(1).4\cdot 11.}&\scriptstyle {\supset \vdash :\sim (p.q.\supset .\sim }&\scriptstyle {r).\equiv .\sim {p.\supset .\sim (q.r)}:}\\scriptstyle {[(1\cdot 01.*3\cdot 01)]}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}}
Note. Here "(1)" stands for " β’: . π . π . β . βΌ π :β‘: π . β . βΌ ( π . π ) {\displaystyle \scriptstyle {\vdash :.p.q.\supset .\sim r:\equiv :p.\supset .\sim (q.r)}}," which is obtained from the above steps by *4Β·22. The use of *4Β·22 will often be tacit, as above. The principle is the same as that explained in respect of implication in *2Β·31.
4Β·33. β’: ( π β¨ π ) β¨ π . β‘ . π β¨ ( π β¨ π ) [ β 2 β 31 β 32 ] {\displaystyle \scriptstyle {\vdash :(p\lor q)\lor r.\equiv .p\lor (q\lor r)\quad [*2\cdot 31\cdot 32]}} The above are the associative laws for multiplication and addition. To avoid brackets, we introduce the following definition:
*4Β·34. π . π . π
. ( π . π ) . π Df {\displaystyle \scriptstyle {p.q.r.=.(p.q).r\quad {\text{Df}}}}
4Β·36. β’: . π β‘ π . β: π . π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :.p\equiv q.\supset :p.r.\equiv .q.r}} [ Fact . β 3 β 47 ] {\displaystyle \scriptstyle {[{\text{Fact}}.3\cdot 47]}}
4Β·37. β’: . π β‘ π . β: π β¨ π . β‘ . π β¨ π {\displaystyle \scriptstyle {\vdash :.p\equiv q.\supset :p\lor r.\equiv .q\lor r}} [ Sum . β 3 β 47 ] {\displaystyle \scriptstyle {[{\text{Sum}}.3\cdot 47]}}
4Β·38. β’: . π β‘ π . π β‘ π . β: π . π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :.p\equiv r.q\equiv s.\supset :p.q.\equiv .r.s}} [ β 3 β 47. β 4 β 32. β 3 β 22 ] {\displaystyle \scriptstyle {[3\cdot 47.4\cdot 32.3\cdot 22]}}
4Β·39. β’: . π β‘ π . π β‘ π . β: π β¨ π . β‘ . π β¨ π {\displaystyle \scriptstyle {\vdash :.p\equiv r.q\equiv s.\supset :p\lor q.\equiv .r\lor s}} [ β 3 β 48. β 4 β 32. β 3 β 22 ] {\displaystyle \scriptstyle {[3\cdot 48.4\cdot 32.3\cdot 22]}}
4Β·4. β’: . π . π β¨ π . β‘: π . π . β¨ . π . π {\displaystyle \scriptstyle {\vdash :.p.q\lor r.\equiv :p.q.\lor .p.r}} This is the first form of the distributive law.
Dem. β’ . β 3 β 2. ββ’:: π . β: π . β . π . π : . π . β: π . β . π . π :: [ Comp ] ββ’:: π . β: . π . β . π . π : π . β . π . π : . [ β 3 β 48 ] β: . π β¨ π . β: π . π . β¨ . π . π ( 1 ) β’ . ( 1 ) . Imp . ββ’: . π . π β¨ π . β: π . π . β¨ . π . π ( 2 ) β’ . β 3 β 26. ββ’: . π . π . β . π : π . π . β . π : . [ β 3 β 44 ] ββ’: . π . π . β¨ . π . π :β . π ( 3 ) β’ . β 3 β 27. ββ’: . π . π . β . π : π . π . β . π : . [ β 3 β 48 ] ββ’: . π . π . β¨ . π . π :β . π β¨ π ( 4 ) β’ . ( 3 ) . ( 4 ) . Comp . ββ’: . π . π . β¨ . π . π :β . π . π β¨ π ( 5 ) β’ . ( 2 ) . ( 5 ) . ββ’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .3\cdot 2.}&\scriptstyle {\supset \vdash ::p.\supset :q.\supset .p.q:.p.\supset :r.\supset .p.r::}\\scriptstyle {[{\text{Comp}}]}&\scriptstyle {\supset \vdash ::p.\supset :.q.\supset .p.q:r.\supset .p.r:.}\\scriptstyle {[3\cdot 48]}&\scriptstyle {\qquad \supset :.q\lor r.\supset :p.q.\lor .p.r}&\scriptstyle {\qquad (1)}\\scriptstyle {\vdash .(1).{\text{Imp}}.}&\scriptstyle {\supset \vdash :.p.q\lor r.\supset :p.q.\lor .p.r}&\scriptstyle {(2)}\\scriptstyle {\vdash .3\cdot 26.}&\scriptstyle {\supset \vdash :.p.q.\supset .p:p.r.\supset .p:.}\\scriptstyle {[3\cdot 44]}&\scriptstyle {\supset \vdash :.p.q.\lor .p.r:\supset .p}&\scriptstyle {(3)}\\scriptstyle {\vdash .3\cdot 27.}&\scriptstyle {\supset \vdash :.p.q.\supset .q:p.r.\supset .r:.}\\scriptstyle {[3\cdot 48]}&\scriptstyle {\supset \vdash :.p.q.\lor .p.r:\supset .q\lor r}&\scriptstyle {(4)}\\scriptstyle {\vdash .(3).(4).{\text{Comp}}.}&\scriptstyle {\supset \vdash :.p.q.\lor .p.r:\supset .p.q\lor r}&\scriptstyle {(5)}\\scriptstyle {\vdash .(2).(5).}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}}
4Β·41. β’: . π . β¨ . π . π :β‘ . π β¨ π . π β¨ π {\displaystyle \scriptstyle {\vdash :.p.\lor .q.r:\equiv .p\lor q.p\lor r}} This is the second form of the distributive lawβa form to which there is nothing analogous in ordinary algebra. By the conventions as to dots, " π . β¨ . π . π {\displaystyle \scriptstyle {p.\lor .q.r}}" means " π β¨ ( π . π ) {\displaystyle \scriptstyle {p\lor (q.r)}}."
Dem. β’ . β 3 β 26. Sum . ββ’: . π . β¨ . π . π : β . π β¨ π ( 1 ) β’ . β 3 β 27. Sum . ββ’: . π . β¨ . π . π : β . π β¨ π ( 2 ) β’ . ( 1 ) . ( 2 ) . Comp . ββ’: . π β¨ . π . π : β . π β¨ π . π β¨ π ( 3 ) β’ . β 2 β 53. β 3 β 47. ββ’: . π β¨ π . π β¨ π . β:βΌ π β π . βΌ π β π : [ Comp ] β:βΌ π . β . π . π : [ β 2 β 54 ] β: π . β¨ . π . π ( 4 ) β’ . ( 3 ) . ( 4 ) . ββ’ . Prop {\displaystyle {\begin{array}{lllr}\scriptstyle {\vdash .3\cdot 26.{\text{Sum}}.}&\scriptstyle {\supset \vdash :.p.\lor .q.r:}&\scriptstyle {\supset .p\lor q}&\scriptstyle {\qquad (1)}\\scriptstyle {\vdash .3\cdot 27.{\text{Sum}}.}&\scriptstyle {\supset \vdash :.p.\lor .q.r:}&\scriptstyle {\supset .p\lor r}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).{\text{Comp}}.}&\scriptstyle {\supset \vdash :.p\lor .q.r:}&\scriptstyle {\supset .p\lor q.p\lor r}&\scriptstyle {(3)}\\scriptstyle {\vdash .2\cdot 53.3\cdot 47.}&\scriptstyle {\supset \vdash :.p\lor q.p\lor r.}&\scriptstyle {\supset :\sim p\supset q.\sim p\supset r:}\\scriptstyle {[{\text{Comp}}]}&&\scriptstyle {\supset :\sim p.\supset .q.r:}\\scriptstyle {[*2\cdot 54]}&&\scriptstyle {\supset :p.\lor .q.r}&\scriptstyle {(4)}\\scriptstyle {\vdash .(3).(4).}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}}
*4Β·42. β’: . π . β‘: π . π . β¨ . π . βΌ π {\displaystyle \scriptstyle {\vdash :.p.\equiv :p.q.\lor .p.\sim q}}
Dem. β’ . β 3 β 21. ββ’: . π β¨ βΌ π . β: π . β . π . π β¨ βΌ π : . [ β 2 β 11 ] ββ’: π . β . π . π β¨ βΌ π ( 1 ) β’ . β 3 β 26. ββ’: π . π β¨ βΌ π . β . π ( 2 ) β’ . ( 1 ) . ( 2 ) . ββ’: . π . β‘: π . π β¨ βΌ π : [ β 4 β 4 ] β‘: π . π . β¨ . π . βΌ π : . ββ’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .3\cdot 21.}&\scriptstyle {\supset \vdash :.q\lor \sim q.\supset :p.\supset .p.q\lor \sim q:.}\\scriptstyle {[2\cdot 11]}&\scriptstyle {\supset \vdash :p.\supset .p.q\lor \sim q}&\scriptstyle {\qquad (1)}\\scriptstyle {\vdash .3\cdot 26.}&\scriptstyle {\supset \vdash :p.q\lor \sim q.\supset .p}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\supset \vdash :.p.\equiv :p.q\lor \sim q:}\\scriptstyle {[4\cdot 4]}&\scriptstyle {\qquad \equiv :p.q.\lor .p.\sim q:.\supset \vdash .{\text{Prop}}}\end{array}}}
*4Β·43. β’: . π . β‘: π β¨ π . π β¨ βΌ π {\displaystyle \scriptstyle {\vdash :.p.\equiv :p\lor q.p\lor \sim q}}
Dem. β’ . β 2 β 2. ββ’: π . β . π β¨ π : π . β . π β¨ βΌ π : [ Comp ] ββ’: π . β . π β¨ π . π β¨ βΌ π ( 1 ) β’ . β 2 β 65 βΌ π π . ββ’: . βΌ π β π . β:βΌ π ββΌ π . β . π : . [ Imp ] ββ’: . βΌ π β π . βΌ π ββΌ π . β . π : . [ β 2 β 53. β 3 β 47 ] ββ’: . π β¨ π . π β¨ βΌ π . β . π ( 2 ) β’ . ( 1 ) . ( 2 ) . ββ’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .2\cdot 2.}&\scriptstyle {\supset \vdash :p.\supset .p\lor q:p.\supset .p\lor \sim q:}\\scriptstyle {[{\text{Comp}}]}&\scriptstyle {\supset \vdash :p.\supset .p\lor q.p\lor \sim q}&\scriptstyle {\qquad (1)}\\scriptstyle {\vdash .2\cdot 65{\frac {\sim p}{p}}.}&\scriptstyle {\supset \vdash :.\sim p\supset q.\supset :\sim p\supset \sim q.\supset .p:.}\\scriptstyle {[{\text{Imp}}]}&\scriptstyle {\supset \vdash :.\sim p\supset q.\sim p\supset \sim q.\supset .p:.}\\scriptstyle {[2\cdot 53.3\cdot 47]}&\scriptstyle {\supset \vdash :.p\lor q.p\lor \sim q.\supset .p}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}} *4Β·44. β’: . π . β‘: π . β¨ . π . π {\displaystyle \scriptstyle {\vdash :.p.\equiv :p.\lor .p.q}}
Dem. β’ . β 2 β 2. ββ’: . π . β: π . β¨ . π . π ( 1 ) β’ . Id . β 3 β 26. ββ’: . π β π : π . π . β . π : . [ β 3 β 44 ] ββ’: . π . β¨ . π . π :β . π ( 2 ) β’ . ( 1 ) . ( 2 ) . ββ’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .2\cdot 2.}&\scriptstyle {\supset \vdash :.p.\supset :p.\lor .p.q}&\scriptstyle {\qquad (1)}\\scriptstyle {\vdash .{\text{Id}}.3\cdot 26.}&\scriptstyle {\supset \vdash :.p\supset p:p.q.\supset .p:.}\\scriptstyle {[*3\cdot 44]}&\scriptstyle {\supset \vdash :.p.\lor .p.q:\supset .p}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}} *4Β·45. β’: π . β‘ . π . π β¨ π [ β 3 β 26. β 2 β 2 ] {\displaystyle \scriptstyle {\vdash :p.\equiv .p.p\lor q\quad [3\cdot 26.2\cdot 2]}}
The following formulae are due to De Morgan, or rather, are the propositional analogues of formulae given by De Morgan for classes. The first of them, it will be observed, merely embodies our definition of the logical product.
4Β·5.β β’: π . π . β‘ . βΌ ( βΌ π β¨ βΌ π ) {\displaystyle \scriptstyle {\vdash :\qquad \,p.q.\equiv .\sim (\sim p\lor \sim q)}} [ β 4 β 2. ( β 3 β 01 ) ] {\displaystyle \scriptstyle {[4\cdot 2.(*3\cdot 01)]}}
4Β·51. β’: βΌ ( π . π ) . β‘ . βΌ π β¨ βΌ π {\displaystyle \scriptstyle {\vdash :\quad \,\sim (p.q).\equiv .\sim p\lor \sim q}} [ β 4 β 5 β 12 ] {\displaystyle \scriptstyle {[4\cdot 5\cdot 12]}}
*4Β·52. β’:
π . βΌ π . β‘ . βΌ ( βΌ π β¨ π ) {\displaystyle \scriptstyle {\vdash :\quad ~~p.\sim q.\equiv .\sim (\sim q\lor q)}} [ β 4 β 5 βΌ π π . β 4 β 13 ] {\displaystyle \scriptstyle {\left[4\cdot 5{\frac {\sim q}{q}}.4\cdot 13\right]}}
*4Β·53. β’:
βΌ ( π . βΌ π ) . β‘ . βΌ π β¨ π {\displaystyle \scriptstyle {\vdash :~\,\sim (p.\sim q).\equiv .\sim p\lor q}} [ β 4 β 52 β 12 ] {\displaystyle \scriptstyle {[*4\cdot 52\cdot 12]}}
*4Β·54. β’:
βΌ π . π . β‘ . βΌ ( π β¨ βΌ π ) {\displaystyle \scriptstyle {\vdash :\quad ~\,\sim p.q.\equiv .\sim (p\lor \sim q)}} [ β 4 β 5 βΌ π π . β 4 β 13 ] {\displaystyle \scriptstyle {\left[4\cdot 5{\frac {\sim p}{p}}.4\cdot 13\right]}}
*4Β·55. β’:
βΌ ( βΌ π . π ) . β‘ . π β¨ βΌ π {\displaystyle \scriptstyle {\vdash :~\,\sim (\sim p.q).\equiv .p\lor \sim q}} [ β 4 β 54 β 12 ] {\displaystyle \scriptstyle {[*4\cdot 54\cdot 12]}}
*4Β·56. β’:
βΌ π . βΌ π . β‘ . βΌ ( π β¨ π ) {\displaystyle \scriptstyle {\vdash :~~~\,\sim p.\sim q.\equiv .\sim (p\lor q)}} [ β 4 β 54 βΌ π π . β 4 β 13 ] {\displaystyle \scriptstyle {\left[4\cdot 54{\frac {\sim q}{q}}.4\cdot 13\right]}}
4Β·57. β’:βΌ ( βΌ π . βΌ π ) . β‘ . π β¨ π {\displaystyle \scriptstyle {\vdash :\sim (\sim p.\sim q).\equiv .p\lor q}} [ β 4 β 56 β 12 ] {\displaystyle \scriptstyle {[4\cdot 56\cdot 12]}}
The following formulae are obtained immediately from the above. They are important as showing how to transform implications into sums or into denials of products, and vice versa. It will be observed that the first of them merely embodies the definition *1Β·01.
*4Β·6.β β’:
π β π . β‘ . βΌ π β¨ π {\displaystyle \scriptstyle {\vdash :\qquad ~p\supset q.\equiv .\sim p\lor q}} [ β 4 β 2. ( β 1 β 01 ) ] {\displaystyle \scriptstyle {[4\cdot 2.(1\cdot 01)]}}
4Β·61. β’: βΌ ( π β π ) . β‘ . π . βΌ π {\displaystyle \scriptstyle {\vdash :\quad \,\sim (p\supset q).\equiv .p.\sim q}} [ β 4 β 6 β 11 β 52 ] {\displaystyle \scriptstyle {[4\cdot 6\cdot 11\cdot 52]}}
*4Β·62. β’:
π ββΌ π . β‘ . βΌ π β¨ βΌ π {\displaystyle \scriptstyle {\vdash :\quad ~~p\supset \sim q.\equiv .\sim p\lor \sim q}} [ β 4 β 6 βΌ π π ] {\displaystyle \scriptstyle {\left[*4\cdot 6{\frac {\sim q}{q}}\right]}}
*4Β·63. β’:
βΌ ( π ββΌ π ) . β‘ . π . π {\displaystyle \scriptstyle {\vdash :~~\sim (p\supset \sim q).\equiv .p.q}} [ β 4 β 62 β 11 β 5 ] {\displaystyle \scriptstyle {[*4\cdot 62\cdot 11\cdot 5]}}
*4Β·64. β’:
βΌ π β π . β‘ . π β¨ π {\displaystyle \scriptstyle {\vdash :\quad ~~\sim p\supset q.\equiv .p\lor q}} [ β 2 β 53 β 54 ] {\displaystyle \scriptstyle {[*2\cdot 53\cdot 54]}}
*4Β·65. β’:
βΌ ( βΌ π β π ) . β‘ . βΌ π . βΌ π {\displaystyle \scriptstyle {\vdash :~~\sim (\sim p\supset q).\equiv .\sim p.\sim q}} [ β 4 β 64 β 11 β 56 ] {\displaystyle \scriptstyle {[*4\cdot 64\cdot 11\cdot 56]}}
4Β·66. β’: βΌ π ββΌ π . β‘ . π β¨ βΌ π {\displaystyle \scriptstyle {\vdash :\quad \,\sim p\supset \sim q.\equiv .p\lor \sim q}} [ β 4 β 64 βΌ π π ] {\displaystyle \scriptstyle {\left[4\cdot 64{\frac {\sim q}{q}}\right]}}
4Β·67. β’:βΌ ( βΌ π ββΌ π ) . β‘ . βΌ π . π {\displaystyle \scriptstyle {\vdash :\sim (\sim p\supset \sim q).\equiv .\sim p.q}} [ β 4 β 66 β 11 β 54 ] {\displaystyle \scriptstyle {[4\cdot 66\cdot 11\cdot 54]}}
*4Β·7.β β’: . π β π . β‘: π . β . π . π {\displaystyle \scriptstyle {\vdash :.p\supset q.\equiv :p.\supset .p.q}}
Dem. β’ . β 3 β 27. Syll . ββ’: . π . β . π . π :β . π β π ( 1 ) β’ . Comp ββ’: . π β . π . π β π . β: π . β . π . π : . [ Exp ] ββ’:: π β π . β: . π β π . β: π . β . π . π :: [ Id ] ββ’: . π β π . β: π . β . π . π ( 2 ) β’ . ( 1 ) . ( 2 ) . β’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .*3\cdot 27.{\text{Syll}}.}&\scriptstyle {\supset \vdash :.p.\supset .p.q:\supset .p\supset q}&\scriptstyle {\quad (1)}\\scriptstyle {\vdash .{\text{Comp}}}&\scriptstyle {\supset \vdash :.p\supset .p.p\supset q.\supset :p.\supset .p.q:.}\\scriptstyle {[{\text{Exp}}]}&\scriptstyle {\supset \vdash ::p\supset p.\supset :.p\supset q.\supset :p.\supset .p.q::}\\scriptstyle {[{\text{Id}}]}&\scriptstyle {\supset \vdash :.p\supset q.\supset :p.\supset .p.q}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\vdash .{\text{Prop}}}\end{array}}}
4Β·71. β’: . π β π . β‘: π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :.p\supset q.\equiv :p.\equiv .p.q}} Dem. β’ . β 3 β 21. ββ’:: π . π . β . π :β: . π . β . π . π :β: π . β‘ . π . π :: [ β 3 β 26 ] ββ’: . π . β . π . π :β: π . β‘ . π . π ( 1 ) β’ . β 3 β 26. ββ’: . π . β‘ . π . π :β: π . β . π . π ( 2 ) β’ . ( 1 ) . ( 2 ) . ββ’: . π . β . π . π :β‘: π . β‘ . π . π ( 3 ) β’ . ( 3 ) . β 4 β 7 β 22. β’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .3\cdot 21.}&\scriptstyle {\supset \vdash ::p.q.\supset .p:\supset :.p.\supset .p.q:\supset :p.\equiv .p.q::}\\scriptstyle {[3\cdot 26]}&\scriptstyle {\supset \vdash :.p.\supset .p.q:\supset :p.\equiv .p.q}&\scriptstyle {(1)}\\scriptstyle {\vdash .3\cdot 26.}&\scriptstyle {\supset \vdash :.p.\equiv .p.q:\supset :p.\supset .p.q}&\scriptstyle {(2)}\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {\supset \vdash :.p.\supset .p.q:\equiv :p.\equiv .p.q}&\scriptstyle {(3)}\\scriptstyle {\vdash .(3).4\cdot 7\cdot 22.}&\scriptstyle {\vdash .{\text{Prop}}}\end{array}}}
The above proposition is constantly used. It enables us to transform every implication into an equivalence, which is an advantage if we wish to assimilate symbolic logic as far as possible to ordinary algebra. But when symbolic logic is regarded as an instrument of proof, we need implications, and it is usually inconvenient to substitute equivalences. Similar remarks apply to the following proposition.
*4Β·72. β’: . π β π . β‘: π . β‘ . π β¨ π {\displaystyle \scriptstyle {\vdash :.p\supset q.\equiv :q.\equiv .p\lor q}}
Dem. β’ . β 4 β 1. ββ’: . π β π . β‘:βΌ π ββΌ π : [ β 4 β 71 βΌ π , βΌ π π ,
π ] β‘:βΌ π . β‘ . βΌ π . βΌ π : [ β 4 β 12 ] β‘: π . β‘ . βΌ ( βΌ π . βΌ π ) : [ 4 β 57 ] β‘: π . β‘ . π β¨ π : [ β 4 β 31 ] β‘: π . β‘ . π β¨ π : . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .4\cdot 1.\supset \vdash :.p\supset q.}&\scriptstyle {\equiv :\sim q\supset \sim p:}\\scriptstyle {\left[4\cdot 71{\frac {\sim q,\sim p}{p,~~q}}\right]}&\scriptstyle {\equiv :\sim q.\equiv .\sim q.\sim p:}\\scriptstyle {[4\cdot 12]}&\scriptstyle {\equiv :q.\equiv .\sim (\sim q.\sim p):}\\scriptstyle {[4\cdot 57]}&\scriptstyle {\equiv :q.\equiv .q\lor p:}\\scriptstyle {[4\cdot 31]}&\scriptstyle {\equiv :q.\equiv .p\lor q:.\supset \vdash .{\text{Prop}}}\end{array}}}
4Β·73. β’: . π . β: π . β‘ . π . π [ Simp . β 4 β 71 ] {\displaystyle \scriptstyle {\vdash :.q.\supset :p.\equiv .p.q\quad [{\text{Simp}}.4\cdot 71]}}
This proposition is very useful, since it shows that a true factor may be omitted from a product without altering its truth or falsehood, just as a true hypothesis may be omitted from an implication.
4Β·74. β’: . βΌ π . β: π . β‘ . π β¨ π {\displaystyle \scriptstyle {\vdash :.\sim p.\supset :q.\equiv .p\lor q}} [ β 2 β 21. β 4 β 72 ] {\displaystyle \scriptstyle {[2\cdot 21.*4\cdot 72]}}
4Β·76. β’: . π β π . π β π . β‘: π . β . π . π {\displaystyle \scriptstyle {\vdash :.p\supset q.p\supset r.\equiv :p.\supset .q.r}} [ β 4 β 41 βΌ π π . ( β 1 β 01 ) ] {\displaystyle \scriptstyle {\left[4\cdot 41{\frac {\sim p}{p}}.(*1\cdot 01)\right]}}
4Β·77. β’: . π β π . π β π . β‘: π β¨ π . β . π {\displaystyle \scriptstyle {\vdash :.q\supset p.r\supset p.\equiv :q\lor r.\supset .p}} [ β 3 β 44. Add . β 2 β 2 ] {\displaystyle \scriptstyle {[3\cdot 44.{\text{Add}}.*2\cdot 2]}}
*4Β·78. β’: . π β π . β¨ . π β π :β‘: π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :.p\supset q.\lor .p\supset r:\equiv :p.\supset .q\lor r}}
Dem.
β’ . β 4 β 2. ( β 1 β 01 ) . ββ’: . π β π . β¨ . π β π : β‘:βΌ π β¨ π . β¨ . βΌ π β¨ π : [ β 4 β 33 ] β‘ . βΌ π . β¨ . π β¨ βΌ π β¨ π : [ β 4 β 31 β 37 ] β‘:βΌ π . β¨ . βΌ π β¨ π β¨ π : [ β 4 β 33 ] β‘:βΌ π β¨ βΌ π . β¨ . π β¨ π : [ β 4 β 25 β 37 ] β‘:βΌ π . β¨ . π β¨ π : [ β 4 β 2. ( β 1 β 01 ) ] β‘: π . β . π β¨ π : . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .4\cdot 2.(1\cdot 01).\supset \vdash :.p\supset q.\lor .p\supset r:}&\scriptstyle {\equiv :\sim p\lor q.\lor .\sim p\lor r:}\\scriptstyle {[4\cdot 33]}&\scriptstyle {\equiv .\sim p.\lor .q\lor \sim p\lor r:}\\scriptstyle {[4\cdot 31\cdot 37]}&\scriptstyle {\equiv :\sim p.\lor .\sim p\lor q\lor r:}\\scriptstyle {[4\cdot 33]}&\scriptstyle {\equiv :\sim p\lor \sim p.\lor .q\lor r:}\\scriptstyle {[4\cdot 25\cdot 37]}&\scriptstyle {\equiv :\sim p.\lor .q\lor r:}\\scriptstyle {[4\cdot 2.(1\cdot 01)]}&\scriptstyle {\equiv :p.\supset .q\lor r:.\supset \vdash .{\text{Prop}}}\end{array}}}
*4Β·79. β’: . π β π . β¨ . π β π :β‘: π . π . β . π {\displaystyle \scriptstyle {\vdash :.q\supset p.\lor .r\supset p:\equiv :q.r.\supset .p}}
Dem. β’ . β 4 β 1 β 39. ββ’: . π β π . β¨ . π β π : β‘:βΌ π ββΌ π . β¨ . βΌ π ββΌ π : [ β 4 β 78 ] β‘:βΌ π . β . βΌ π β¨ βΌ π : [ β 2 β 15 ] β‘:βΌ ( βΌ π β¨ βΌ π ) . β . π : [ β 4 β 2. ( β 3 β 01 ) ] β‘: π . π . β . π : . ββ’ . Prop {\displaystyle {\begin{array}{ll}\scriptstyle {\vdash .4\cdot 1\cdot 39.\supset \vdash :.q\supset p.\lor .r\supset p:}&\scriptstyle {\equiv :\sim p\supset \sim q.\lor .\sim p\supset \sim r:}\\scriptstyle {[4\cdot 78]}&\scriptstyle {\equiv :\sim p.\supset .\sim q\lor \sim r:}\\scriptstyle {[2\cdot 15]}&\scriptstyle {\equiv :\sim (\sim q\lor \sim r).\supset .p:}\\scriptstyle {[4\cdot 2.(*3\cdot 01)]}&\scriptstyle {\equiv :q.r.\supset .p:.\supset \vdash .{\text{Prop}}}\end{array}}}
Note. The analogues, for classes, of *4Β·78Β·79 are false. Take, e.g. *4Β·78, and put
{\displaystyle \scriptstyle {p=}}English people,
{\displaystyle \scriptstyle {q=}}men,
{\displaystyle \scriptstyle {r=}}women. Then π {\displaystyle \scriptstyle {p}} is contained in π {\displaystyle \scriptstyle {q}} or π {\displaystyle \scriptstyle {r}}, but is not contained in π {\displaystyle \scriptstyle {q}} and is not contained in π {\displaystyle \scriptstyle {r}}.
4Β·8. β’: π ββΌ π . β‘ . βΌ π {\displaystyle \scriptstyle {\vdash :p\supset \sim p.\equiv .\sim p}} [ β 2 β 01. Simp ] {\displaystyle \scriptstyle {[2\cdot 01.{\text{Simp}}]}}
4Β·81. β’:βΌ π β π . β‘ . π {\displaystyle \scriptstyle {\vdash :\sim p\supset p.\equiv .p}} [ β 2 β 18. Simp ] {\displaystyle \scriptstyle {[2\cdot 18.{\text{Simp}}]}}
4Β·82. β’: π β π . π ββΌ π . β‘ . βΌ π {\displaystyle \scriptstyle {\vdash :p\supset q.p\supset \sim q.\equiv .\sim p}} [ β 2 β 65. Imp . β 2 β 21. Comp ] {\displaystyle \scriptstyle {[2\cdot 65.{\text{Imp}}.*2\cdot 21.{\text{Comp}}]}}
4Β·83. β’: π β π . βΌ π β π . β‘ . π {\displaystyle \scriptstyle {\vdash :p\supset q.\sim p\supset q.\equiv .q}} [ β 2 β 61. Imp . Simp . Comp ] {\displaystyle \scriptstyle {[2\cdot 61.{\text{Imp}}.{\text{Simp}}.{\text{Comp}}]}}
Note. *4Β·82Β·83 may also be obtained from *4Β·43, of which they are virtually other forms.
4Β·84. β’: . π β‘ π . β: π β π . β‘ . π β π {\displaystyle \scriptstyle {\vdash :.p\equiv q.\supset :p\supset r.\equiv .q\supset r}} [ β 2 β 06. β 3 β 47 ] {\displaystyle \scriptstyle {[2\cdot 06.*3\cdot 47]}}
4Β·85. β’: . π β‘ π . β: π β π . β‘ . π β π {\displaystyle \scriptstyle {\vdash :.p\equiv q.\supset :r\supset p.\equiv .r\supset q}} [ β 2 β 05. β 3 β 47 ] {\displaystyle \scriptstyle {[2\cdot 05.*3\cdot 47]}}
4Β·86. β’: . π β‘ π . β: π β‘ π . β‘ . π β‘ π {\displaystyle \scriptstyle {\vdash :.p\equiv q.\supset :p\equiv r.\equiv .q\equiv r}} [ β 4 β 21 β 22 ] {\displaystyle \scriptstyle {[4\cdot 21\cdot 22]}}
*4Β·87. β’: . π . π . β . π :β‘: π . β . π β π :β‘: π . β . π β π :β‘: π . π . β . π {\displaystyle \scriptstyle {\vdash :.p.q.\supset .r:\equiv :p.\supset .q\supset r:\equiv :q.\supset .p\supset r:\equiv :q.p.\supset .r}}
[ Exp . Comm . Imp ] {\displaystyle \scriptstyle {[{\text{Exp}}.{\text{Comm}}.{\text{Imp}}]}} *4Β·87 embodies in one proposition the principles of exportation and importation and the commutative principle.
*5. Miscellaneous Propositions. Summary of *5.
The present number consists chiefly of propositions of two sorts: (1) those which will be required as lemmas in one or more subsequent proofs, (2) those which are on their own account illustrative, or would be important in other developments than those that we wish to make. A few of the propositions of this number, however, will be used very frequently. These are:
*5Β·1. β’: π . π . β . π β‘ π {\displaystyle \scriptstyle {\vdash :p.q.\supset .p\equiv q}}
I.e. two propositions are equivalent if they are both true. (The statement that two propositions are equivalent if they are both false is *5Β·21.)
*5Β·32. β’: . π . β . π β‘ π :β‘: π . π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :.p.\supset .q\equiv r:\equiv :p.q.\equiv .p.r}}
I.e. to say that, on the hypothesis π {\displaystyle \scriptstyle {p}}, π {\displaystyle \scriptstyle {q}} and π {\displaystyle \scriptstyle {r}} are equivalent, is equivalent to saying that the joint assertion of π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} is equivalent to the joint assertion of π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {r}}. This is a very useful rule in inference.
*5Β·6. β’: . π . βΌ π . β . π :β‘: π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :.p.\sim q.\supset .r:\equiv :p.\supset .q\lor r}}
I.e. " π {\displaystyle \scriptstyle {p}} and not- π {\displaystyle \scriptstyle {q}} imply π {\displaystyle \scriptstyle {r}}" is equivalent to " π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}} or π {\displaystyle \scriptstyle {r}}."
Among propositions never subsequently referred to, but inserted for their intrinsic interest, are the following: *5Β·11Β·12Β·13Β·14, which state that, given any two propositions π {\displaystyle \scriptstyle {p}}, π {\displaystyle \scriptstyle {q}}, either π {\displaystyle \scriptstyle {p}} or βΌ π {\displaystyle \scriptstyle {\sim p}} must imply π {\displaystyle \scriptstyle {q}}, and π {\displaystyle \scriptstyle {p}} must imply either π {\displaystyle \scriptstyle {q}} or not- π {\displaystyle \scriptstyle {q}}, and either π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}} or π {\displaystyle \scriptstyle {q}} implies π {\displaystyle \scriptstyle {p}}; and given any third proposition π {\displaystyle \scriptstyle {r}}, either π {\displaystyle \scriptstyle {p}} implies π {\displaystyle \scriptstyle {q}} or π {\displaystyle \scriptstyle {q}} implies π {\displaystyle \scriptstyle {r}}[12].
Other propositions not subsequently referred to are 5Β·22Β·23Β·24; in these it is shown that two propositions are not equivalent when, and only when, one is true and the other false, and that two propositions are equivalent when, and only when, both are true or both false. It follows (5Β·24) that the negation of " π . π . β¨ . βΌ π . βΌ π {\displaystyle \scriptstyle {p.q.\lor .\sim p.\sim q}}" is equivalent to " π . βΌ π . β¨ . π . βΌ π {\displaystyle \scriptstyle {p.\sim q.\lor .q.\sim p}}." *5Β·54Β·55 state that both the product and the sum of π {\displaystyle \scriptstyle {p}} and π {\displaystyle \scriptstyle {q}} are equivalent, respectively, either to π {\displaystyle \scriptstyle {p}} or to π {\displaystyle \scriptstyle {q}}.
The proofs of the following propositions are all easy, and we shall therefore often merely indicate the propositions used in the proofs.
5Β·1.β β’: π . π . β . π β‘ π {\displaystyle \scriptstyle {\vdash :p.q.\supset .p\equiv q}} [ β 3 β 4 β 22 ] {\displaystyle \scriptstyle {[3\cdot 4\cdot 22]}} 5Β·11. β’: π β π . β¨ . βΌ π β π {\displaystyle \scriptstyle {\vdash :p\supset q.\lor .\sim p\supset q}} [ β 2 β 51 β 54 ] {\displaystyle \scriptstyle {[2\cdot 51\cdot 54]}}
5Β·12. β’: π β π . β¨ . π ββΌ π {\displaystyle \scriptstyle {\vdash :p\supset q.\lor .p\supset \sim q}} [ β 2 β 52 β 54 ] {\displaystyle \scriptstyle {[2\cdot 52\cdot 54]}}
5Β·13. β’: π β π . β¨ . π β π {\displaystyle \scriptstyle {\vdash :p\supset q.\lor .q\supset p}} [ β 2 β 5 β 21 ] {\displaystyle \scriptstyle {[2\cdot 5\cdot 21]}}
5Β·14. β’: π β π . β¨ . π β π {\displaystyle \scriptstyle {\vdash :p\supset q.\lor .q\supset r}} [ Simp . Transp . β 2 β 21 ] {\displaystyle \scriptstyle {[{\text{Simp}}.{\text{Transp}}.2\cdot 21]}}
*5Β·15. β’: π β‘ π . β¨ . π β‘βΌ π {\displaystyle \scriptstyle {\vdash :p\equiv q.\lor .p\equiv \sim q}}
Dem. β’ . β 4 β 61. ββ’:βΌ ( π β π ) . β . π . βΌ π . [ β 5 β 1 ] β . π β‘βΌ π : [ β 2 β 54 ] ββ’: π β π . β¨ . π β‘βΌ π (1) β’ . β 4 β 61. ββ’:βΌ ( π β π ) . β . π . βΌ π . [ β 5 β 1 ] β . π β‘βΌ π . [ β 4 β 12 ] β . π β‘βΌ π : [ β 2 β 54 ] ββ’: π β π . β¨ . π β‘βΌ π (2) β’ . ( 1 ) . ( 2 ) . β 4 β 41. ββ’ . Prop {\displaystyle {\begin{array}{lllr}\scriptstyle {\vdash .4\cdot 61.}&\scriptstyle {\supset \vdash :\sim (p\supset q).}&\scriptstyle {\supset .p.\sim q.}\\scriptstyle {[5\cdot 1]}&&\scriptstyle {\supset .p\equiv \sim q:}\\scriptstyle {[2\cdot 54]}&\scriptstyle {\supset \vdash :p\supset q.\lor .p}&\scriptstyle {\equiv \sim q}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\scriptstyle {\vdash .4\cdot 61.}&\scriptstyle {\supset \vdash :\sim (q\supset p).}&\scriptstyle {\supset .q.\sim p.}\\scriptstyle {[5\cdot 1]}&&\scriptstyle {\supset .q\equiv \sim p.}\\scriptstyle {[4\cdot 12]}&&\scriptstyle {\supset .p\equiv \sim q:}\\scriptstyle {[2\cdot 54]}&\scriptstyle {\supset \vdash :q\supset p.\lor .p}&\scriptstyle {\equiv \sim q}&\scriptstyle {\text{(2)}}\\scriptstyle {\vdash .(1).(2)}&\scriptstyle {.4\cdot 41.}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}}
*5Β·16. β’ . βΌ ( π β‘ π . π β‘βΌ π ) {\displaystyle \scriptstyle {\vdash .\sim (p\equiv q.p\equiv \sim q)}}
Dem. β’ . β 3 β 26. ββ’: π β‘ π . π ββΌ π . β . π β π . π ββΌ π . [ β 4 β 82 ] β . βΌ π (1) β’ . β 3 β 27. ββ’: π β‘ π . π ββΌ π . β . π β π . π ββΌ π . [ Syll ] β . π ββΌ π . [ Abs ] β . βΌ π (2) β’ . ( 1 ) . ( 2 ) . Comp . ββ’: π β‘ π . π ββΌ π . β . βΌ π . βΌ π . [ β 4 β 65 π , π π , π ] β . βΌ ( βΌ π β π ) (3) β’ . ( 3 ) . Exp . ββ’: . π β‘ π . β: π ββΌ π . β . βΌ ( βΌ π β π ) : [ Id . ( β 1 β 01 ) ] β:βΌ ( π ββΌ π ) . β¨ . βΌ ( βΌ π β π ) : [ β 4 β 51. ( β 4 β 01 ) ] β:βΌ ( π β‘βΌ π ) : . ββ’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .3\cdot 26.\supset \vdash :p\equiv q.p\supset \sim q.}&\scriptstyle {\supset .p\supset q.p\supset \sim q.}\\scriptstyle {[4\cdot 82]}&\scriptstyle {\supset .\sim p}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\scriptstyle {\vdash .3\cdot 27.\supset \vdash :p\equiv q.p\supset \sim q.}&\scriptstyle {\supset .q\supset p.p\supset \sim q.}\\scriptstyle {[{\text{Syll}}]}&\scriptstyle {\supset .q\supset \sim q.}\\scriptstyle {[{\text{Abs}}]}&\scriptstyle {\supset .\sim q}&\scriptstyle {\text{(2)}}\\scriptstyle {\vdash .(1).(2).{\text{Comp}}.\supset \vdash :p\equiv q.p}&\scriptstyle {\supset \sim q.\supset .\sim p.\sim q.}\\scriptstyle {\left[4\cdot 65{\frac {q,p}{p,q}}\right]}&\scriptstyle {\supset .\sim (\sim q\supset p)}&\scriptstyle {\text{(3)}}\\scriptstyle {\vdash .(3).{\text{Exp}}.\supset \vdash :.p\equiv q.\supset :p}&\scriptstyle {\supset \sim q.\supset .\sim (\sim q\supset p):}\\scriptstyle {[{\text{Id}}.(1\cdot 01)]}&\scriptstyle {\supset :\sim (p\supset \sim q).\lor .\sim (\sim q\supset p):}\\scriptstyle {[4\cdot 51.(*4\cdot 01)]}&\scriptstyle {\supset :\sim (p\equiv \sim q):.\supset \vdash .{\text{Prop}}}\end{array}}}
*5Β·17. β’: π β¨ π . βΌ ( π . π ) . β‘ . π β‘βΌ π {\displaystyle \scriptstyle {\vdash :p\lor q.\sim (p.q).\equiv .p\equiv \sim q}}
Dem. β’ . β 4 β 64 β 21. ββ’: π β¨ π . β‘ . βΌ π β π (1) β’ . β 4 β 63. Transp . ββ’:βΌ ( π . π ) . β‘ . π ββΌ π (2) β’ . ( 1 ) . ( 2 ) . β 4 β 38 β 21. ββ’ . Prop {\displaystyle {\begin{array}{llr}\scriptstyle {\vdash .4\cdot 64\cdot 21.}&\scriptstyle {\supset \vdash :p\lor q.\equiv .\sim q\supset p}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\scriptstyle {\vdash .4\cdot 63.{\text{Transp}}.}&\scriptstyle {\supset \vdash :\sim (p.q).\equiv .p\supset \sim q}&\scriptstyle {\text{(2)}}\\scriptstyle {\vdash .(1).(2).*4\cdot 38\cdot 21.}&\scriptstyle {\supset \vdash .{\text{Prop}}}\end{array}}}
5Β·18. β’: π β‘ π . β‘ . βΌ ( π β‘βΌ π ) {\displaystyle \scriptstyle {\vdash :p\equiv q.\equiv .\sim (p\equiv \sim q)}} [ β 5 β 15 β 16. β 5 β 17 π β‘ π , π β‘βΌ π π , π ] {\displaystyle \scriptstyle {\left[5\cdot 15\cdot 16.*5\cdot 17{\frac {p\equiv q,p\equiv \sim q}{p,\quad q}}\right]}}
5Β·19. β’ . βΌ ( π β‘βΌ π ) {\displaystyle \scriptstyle {\vdash .\sim (p\equiv \sim p)}} [ β 5 β 18 π π . β 4 β 2 ] {\displaystyle \scriptstyle {\left[5\cdot 18{\frac {p}{q}}.*4\cdot 2\right]}}
5Β·21. β’:βΌ π . βΌ π . β . π β‘ π {\displaystyle \scriptstyle {\vdash :\sim p.\sim q.\supset .p\equiv q}} [ β 5 β 1. β 4 β 11 ] {\displaystyle \scriptstyle {[5\cdot 1.*4\cdot 11]}}
5Β·22. β’: . βΌ ( π β‘ π ) . β‘: π . βΌ π . β¨ . π . βΌ π {\displaystyle \scriptstyle {\vdash :.\sim (p\equiv q).\equiv :p.\sim q.\lor .q.\sim p}} [ β 4 β 61 β 51 β 39 ] {\displaystyle \scriptstyle {[4\cdot 61\cdot 51\cdot 39]}}
5Β·23. β’: . π β‘ π . β‘: π . π . β¨ . βΌ π . βΌ π {\displaystyle \scriptstyle {\vdash :.p\equiv q.\equiv :p.q.\lor .\sim p.\sim q}} [ β 5 β 18. β 5 β 22 βΌ π π .4 β 13 β 36 ] {\displaystyle \scriptstyle {\left[5\cdot 18.*5\cdot 22{\frac {\sim q}{q}}.4\cdot 13\cdot 36\right]}}
5Β·24. β’: . βΌ ( π . π . β¨ . βΌ π . βΌ π ) . β‘: π . βΌ π . β¨ . π . βΌ π {\displaystyle \scriptstyle {\vdash :.\sim (p.q.\lor .\sim p.\sim q).\equiv :p.\sim q.\lor .q.\sim p}} [ β 5 β 22 β 23 ] {\displaystyle \scriptstyle {[5\cdot 22\cdot 23]}}
5Β·25. β’: . π β¨ π . β‘: π β π . β . π {\displaystyle \scriptstyle {\vdash :.p\lor q.\equiv :p\supset q.\supset .q}} [ β 2 β 62 β 68 ] {\displaystyle \scriptstyle {[2\cdot 62\cdot 68]}}
From *5Β·25 it appears that we might have taken implication, instead of disjunction, as a primitive idea, and have defined " π β¨ π {\displaystyle \scriptstyle {p\lor q}}" as meaning " π β π . β . π {\displaystyle \scriptstyle {p\supset q.\supset .q}}." This course, however, requires more primitive propositions than are required by the method we have adopted.
*5Β·3.β β’: . π . π . β . π :β‘: π . π . β . π . π {\displaystyle \scriptstyle {\vdash :.p.q.\supset .r:\equiv :p.q.\supset .p.r}} [ Simp . Comp . Syll ] {\displaystyle \scriptstyle {[{\text{Simp}}.{\text{Comp}}.{\text{Syll}}]}}
*5Β·31. β’: . π . π β π :β: π . β . π . π {\displaystyle \scriptstyle {\vdash :.r.p\supset q:\supset :p.\supset .q.r}} [ Simp . Comp ] {\displaystyle \scriptstyle {[{\text{Simp}}.{\text{Comp}}]}}
5Β·32. β’: . π . β . π β‘ π :β‘: π . π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :.p.\supset .q\equiv r:\equiv :p.q.\equiv .p.r}} [ β 4 β 76. β 3 β 3 β 31. β 5 β 3 ] {\displaystyle \scriptstyle {[4\cdot 76.3\cdot 3\cdot 31.5\cdot 3]}}
This proposition is constantly required in subsequent proofs.
5Β·33. β’: . π . π β π . β‘: π : π . π . β . π {\displaystyle \scriptstyle {\vdash :.p.q\supset r.\equiv :p:p.q.\supset .r}} [ β 4 β 73 β 84. β 5 β 32 ] {\displaystyle \scriptstyle {[4\cdot 73\cdot 84.*5\cdot 32]}}
5Β·35. β’: . π β π . π β π . β: π . β . π β‘ π {\displaystyle \scriptstyle {\vdash :.p\supset q.p\supset r.\supset :p.\supset .q\equiv r}} [ Comp . β 5 β 1 ] {\displaystyle \scriptstyle {[{\text{Comp}}.5\cdot 1]}}
5Β·36. β’: π . π β‘ π . β‘ . π . π β‘ π {\displaystyle \scriptstyle {\vdash :p.p\equiv q.\equiv .q.p\equiv q}} [ Ass . β 4 β 38 ] {\displaystyle \scriptstyle {[{\text{Ass}}.4\cdot 38]}}
5Β·4.β β’: . π . β . π β π :β‘ . π β π {\displaystyle \scriptstyle {\vdash :.p.\supset .p\supset q:\equiv .p\supset q}} [ Simp . β 2 β 43 ] {\displaystyle \scriptstyle {[{\text{Simp}}.2\cdot 43]}}
5Β·41. β’: . π β π . β . π β π :β‘: π . β . π β π {\displaystyle \scriptstyle {\vdash :.p\supset q.\supset .p\supset r:\equiv :p.\supset .q\supset r}} [ β 2 β 77 β 86 ] {\displaystyle \scriptstyle {[2\cdot 77\cdot 86]}}
5Β·42. β’:: π . β . π β π :β‘: . π . β: π . β . π . π {\displaystyle \scriptstyle {\vdash ::p.\supset .q\supset r:\equiv :.p.\supset :q.\supset .p.r}} [ β 5 β 3. β 4 β 87 ] {\displaystyle \scriptstyle {[5\cdot 3.*4\cdot 87]}}
5Β·44. β’:: π β π . β: . π β π . β‘: π . β . π . π {\displaystyle \scriptstyle {\vdash ::p\supset q.\supset :.p\supset r.\equiv :p.\supset .q.r}} [ β 4 β 76. β 5 β 3 β 32 ] {\displaystyle \scriptstyle {[4\cdot 76.*5\cdot 3\cdot 32]}}
*5Β·5.β β’: . π . β: π β π . β‘ . π {\displaystyle \scriptstyle {\vdash :.p.\supset :p\supset q.\equiv .q}} [ Ass . Exp . Simp ] {\displaystyle \scriptstyle {[{\text{Ass}}.{\text{Exp}}.{\text{Simp}}]}}
5Β·501. β’: . π . β: π . β‘ . π β‘ π {\displaystyle \scriptstyle {\vdash :.p.\supset :q.\equiv .p\equiv q}} [ β 5 β 1. Exp . Ass ] {\displaystyle \scriptstyle {[5\cdot 1.{\text{Exp}}.{\text{Ass}}]}}
5Β·53. β’: . π β¨ π β¨ π . β . π :β‘: π β π . π β π . π β π {\displaystyle \scriptstyle {\vdash :.p\lor q\lor r.\supset .s:\equiv :p\supset s.q\supset s.r\supset s}} [ β 4 β 77 ] {\displaystyle \scriptstyle {[4\cdot 77]}}
5Β·54. β’: . π . π . β‘ . π : β¨ : π . π . β‘ . π {\displaystyle \scriptstyle {\vdash :.p.q.\equiv .p:\lor :p.q.\equiv .q}} [ β 4 β 73. β 4 β 44. Transp . β 5 β 1 ] {\displaystyle \scriptstyle {[4\cdot 73.4\cdot 44.{\text{Transp}}.5\cdot 1]}}
5Β·55. β’: . π β¨ π . β‘ . π : β¨ : π β¨ π . β‘ . π {\displaystyle \scriptstyle {\vdash :.p\lor q.\equiv .p:\lor :p\lor q.\equiv .q}} [ β 1 β 3. β 5 β 1. β 4 β 74 ] {\displaystyle \scriptstyle {[1\cdot 3.5\cdot 1.4\cdot 74]}}
5Β·6.β β’: . π . βΌ π . β . π :β‘: π . β . π β¨ π {\displaystyle \scriptstyle {\vdash :.p.\sim q.\supset .r:\equiv :p.\supset .q\lor r}} [ β 4 β 87 βΌ π π . β 4 β 64 β 85 ] {\displaystyle \scriptstyle {\left[4\cdot 87{\frac {\sim q}{q}}.*4\cdot 64\cdot 85\right]}}
5Β·61. β’: π β¨ π . βΌ π . β‘ . π . βΌ π {\displaystyle \scriptstyle {\vdash :p\lor q.\sim q.\equiv .p.\sim q}} [ β 4 β 74. β 5 β 32 ] {\displaystyle \scriptstyle {[4\cdot 74.*5\cdot 32]}}
5Β·62. β’: . π . π . β¨ . βΌ π :β‘ . π β¨ βΌ π {\displaystyle \scriptstyle {\vdash :.p.q.\lor .\sim q:\equiv .p\lor \sim q}} [ β 4 β 7 π , π π , π ] {\displaystyle \scriptstyle {\left[4\cdot 7{\frac {q,p}{p,q}}\right]}}
*5Β·63. β’: . π β¨ π . β‘: π . β¨ . βΌ π . π {\displaystyle \scriptstyle {\vdash :.p\lor q.\equiv :p.\lor .\sim p.q}} [ β 5 β 62 βΌ π , π π ,
π ] {\displaystyle \scriptstyle {\left[*5\cdot 62{\frac {\sim p,q}{q,~~p}}\right]}}
5Β·7.β β’: . π β¨ π . β‘ . π β¨ π :β‘: π . β¨ . π β‘ π {\displaystyle \scriptstyle {\vdash :.p\lor r.\equiv .q\lor r:\equiv :r.\lor .p\equiv q}} [ β 4 β 74. β 1 β 3. β 5 β 1. β 4 β 37 ] {\displaystyle \scriptstyle {[4\cdot 74.1\cdot 3.5\cdot 1.*4\cdot 37]}}
*5Β·71. β’: . π ββΌ π . β: π β¨ π . π . β‘ . π . π {\displaystyle \scriptstyle {\vdash :.q\supset \sim r.\supset :p\lor q.r.\equiv .p.r}}
In the following proof, as always henceforth, " Hp {\displaystyle \scriptstyle {\text{Hp}}}" means the hypothesis of the proposition to be proved.
Dem.
β’
.
β
4
β
4.
ββ’:
.
π
β¨
π
.
π
.
β‘:
π
.
π
.
β¨
.
π
.
π
(1)
β’
.
β
4
β
62
β
51.
ββ’::
Hp
.
β:
.
βΌ
(
π
.
π
)
:
.
[
β
4
β
74
]
β:
.
π
.
π
.
β¨
.
π
.
π
:β‘:
π
.
π
(2)
β’
.
(
1
)
.
(
2
)
.
β
4
β
22.
ββ’
.
Prop
{\displaystyle {\begin{array}{lllr}\scriptstyle {\vdash .4\cdot 4.}&\scriptstyle {\supset \vdash :.p\lor q}&\scriptstyle {.r.\equiv :p.r.\lor .q.r}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\scriptstyle {\vdash .4\cdot 62\cdot 51.}&\scriptstyle {\supset \vdash ::{\text{Hp}}.}&\scriptstyle {\supset :.\sim (q.r):.}\\scriptstyle {[4\cdot 74]}&&\scriptstyle {\supset :.p.r.\lor .q.r:\equiv :p.r}&\scriptstyle {\text{(2)}}\\scriptstyle {\vdash .(1).(2).}&\scriptstyle {4\cdot 22.\supset \vdash }&\scriptstyle {.{\text{Prop}}}\end{array}}}
*5Β·74. β’: . π . β . π β‘ π :β‘: π β π . β‘ . π β π {\displaystyle \scriptstyle {\vdash :.p.\supset .q\equiv r:\equiv :p\supset q.\equiv .p\supset r}}
Dem. β’ . β 5 β 41. ββ’:: π β π . β . π β π :β‘: π . β . π β π : . π β π . β . π β π :β‘: π . β . π β π (1) β’ . ( 1 ) . β 4 β 38. ββ’:: π β π . β‘ . π β π . β‘: . π . β . π β π : π . β . π β π : . [ β 4 β 76 ] β‘: . π . β . π β‘ π ::ββ’ . Prop {\displaystyle {\begin{array}{lllr}\scriptstyle {\vdash .5\cdot 41.\supset \vdash ::p\supset q.\supset .}&\scriptstyle {p\supset r:\equiv :p}&\scriptstyle {.\supset .q\supset r:.}\&\scriptstyle {p\supset r.\supset .p}&\scriptstyle {\supset q:\equiv :p.\supset .r\supset q}&\scriptstyle {\qquad {\text{(1)}}}\\scriptstyle {\vdash .(1).4\cdot 38.\supset \vdash ::p\supset q.}&\scriptstyle {\equiv .p\supset r.}&\scriptstyle {\equiv :.p.\supset .q\supset r:p.\supset .r\supset q:.}\\scriptstyle {[*4\cdot 76]}&&\scriptstyle {\equiv :.p.\supset .q\equiv r::\supset \vdash .{\text{Prop}}}\end{array}}}
*5Β·75. β’: . π ββΌ π : π . β‘ . π β¨ π :β: π . βΌ π . β‘ . π {\displaystyle \scriptstyle {\vdash :.r\supset \sim q:p.\equiv .q\lor r:\supset :p.\sim q.\equiv .r}}
Dem. β’ . β 5 β 6. ββ’: . Hp . β: π . βΌ π . β . π (1) β’ . β 3 β 27. ββ’: . Hp . β: π β¨ π . β . π : [ β 4 β 77 ] β: π β π (2) β’ . β 3 β 26. ββ’: . Hp . β: π ββΌ π (3) β’ . ( 2 ) . ( 3 ) . Comp . ββ’: . Hp . β: π β π . π ββΌ π : [ Comp ] β: π . β . π . βΌ π (4) β’ . ( 1 ) . ( 4 ) . Comp . ββ’: . Hp . β: π . βΌ π . β‘ . π : . ββ’ . Prop {\displaystyle {\begin{array}{llllr}\scriptstyle {\vdash .5\cdot 6.}&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :p.\sim q}&\scriptstyle {.\supset .r}&\scriptstyle {\qquad \qquad {\text{(1)}}}\\scriptstyle {\vdash .3\cdot 27.}&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :q\lor r.}&\scriptstyle {\supset .p:}\\scriptstyle {[4\cdot 77]}&&\scriptstyle {\supset :r\supset p}&&\scriptstyle {\text{(2)}}\\scriptstyle {\vdash .3\cdot 26.}&&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :r\supset \sim q}&\scriptstyle {\text{(3)}}\\scriptstyle {\vdash .(2).(3)}&\scriptstyle {.{\text{Comp}}.}&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :r\supset p.r\supset \sim q:}\\scriptstyle {[{\text{Comp}}]}&&\scriptstyle {\supset :r.\supset .p.\sim q}&&\scriptstyle {\text{(4)}}\\scriptstyle {\vdash .(1).(4)}&\scriptstyle {.{\text{Comp}}.}&\scriptstyle {\supset \vdash :.{\text{Hp}}.}&\scriptstyle {\supset :p.\sim q.\equiv .r:.\supset \vdash .{\text{Prop}}}\end{array}}}
The recognized methods of proving independence are not applicable, without reserve, to fundamentals. Cf. Principles of Mathematics, Β§ 17. What is there said concerning primitive propositions applies with even greater force to primitive ideas. We have adopted both the idea and the symbol of assertion from Frege. Cf. Principles of Mathematics, Β§38. When we say that a proposition "belongs to logic," we mean that it can be expressed in terms of the primitive ideas of logic. We do not mean that logic applies to it, for that would of course be true of any proposition. The sign of equality not followed by the letters " Df {\displaystyle \scriptstyle {\text{Df}}}" will have a different meaning, to be defined later. The letters " Pp {\displaystyle \scriptstyle {\text{Pp}}}" stand for "primitive proposition," as with Peano. For further remarks on this principle, cf. Principles of Mathematics, Β§ 38. Later on we shall cease to mark the distinction between a premiss and a rule according to which an inference is conducted. It is only in early proofs that this distinction is important. There is an interesting historical article on this principle by Vailati, "A proposito d'un passo del Teeteto e di una dimostrazione di Euclide," Rivista di Filosofia e scienze affine, 1904. This abbreviation applies to the same type of cases as those concerned in the note to *2Β·15, but is often more convenient than the abbreviation explained in that note. Philosophical works, Gerhardt's edition, Vol. vii. p. 223. Cf. SchrΓΆder, Vorlesungen ΓΌber Algebra der Logik, Zweiter Band (Leipzig, 1891), pp. 270β271, where the apparent oddity of the above proposition is explained.