Volume 1 / Part 1 — *13. IDENTITY.
Reading edition
*13. IDENTITY.
Summary of *13.
The propositional function " is identical with " will be written "." We shall find that this use of the sign of equality covers all the common uses of equality that occur in mathematics. The definition is as follows:
*13·01.
This definition states that and are to be called identical when every predicative function satisfied by is also satisfied by . We cannot state that every function satisfied by is to be satisfied by , because satisfies functions of various orders, and these cannot all be covered by one apparent variable. But in virtue of the axiom of reducibility it follows that, if and satisfies , where is any function, predicative or non-predicative, then also satisfies (cf. *13·101, below). Hence in effect the definition is as powerful as it would be if it could be extended to cover all functions of .
Note that the second sign of equality in the above definition is combined with "," and thus is not really the same symbol as the sign of equality which is defined. Thus the definition is not circular, although at first sight it appears so.
The propositions of the present number are constantly referred to. Most of them are self-evident, and the proofs offer no difficulty. The most important of the propositions of this number are the following:
*13·101.
I.e. if and are identical, any property of is a property of .
*13·12.
This includes *13·101 together with the fact that if and are identical any property of is a property of .
*13·15·16·17, which state that identity is reflexive, symmetrical and transitive.
*13·191.
I.e. to state that everything that is identical with has a certain property is equivalent to stating that has that property.
*13·195.
I.e. to state that something identical with has a certain property is equivalent to saying that has that property.
*13·22.
This is the analogue of *13·195 for two variables.
*13·01.
The following definitions embody abbreviations which are often convenient.
*13·02.
*13·03.
*13·1.
*13·101.
Dem.
In virtue of this proposition, if , satisfies any function, whether predicative or non-predicative, which is satisfied by . It will be observed that the proof uses the axiom of reducibility (*12·1). But for this axiom, two terms and might agree in respect of all predicative functions, but not in respect of all non-predicative functions. We should thus be led to identities of different degrees, according to the degree of the functions in respect of which and agreed. Strict identity would, in this case, have to be taken as a primitive idea, and *13·101 would have to be a primitive proposition, as would also *13·15·16·17.
*13·11.
Dem.
*13·12.
Dem.
*13·13.
*13·14.
*13·15.
*13·16.
*13·17.
Dem.
In the above use of *10·3, , , are regarded as three different functions of , and replaces the of *10·3.
The above three propositions show that identity is reflexive (*13·15), symmetrical (*13·16), and transitive (*13·17). These are the three marks of relations having the formal properties which we associate commonly with the sign of equality.
*13·171.
*13·172.
*13·18.
*13·181.
*13·182.
*13·183.
Dem.
*13·19.
*13·191.
Dem.
This proposition is constantly used in subsequent proofs.
*13·192.
Dem.
This proposition is useful in the theory of descriptions (*14).
*13·193.
Dem.
This proposition is very often used.
*13·194.
This proposition is used in *37·65 and *101·14.
*13·195.
Dem.
The use of this proposition in subsequent proofs is very frequent.
*13·196.
*13·21.
Dem.
This proposition is the analogue, for two variables, of *13·191.
*13·22.
Dem.
This proposition is the analogue, for two variables, of *13·195. It is frequently used, especially in the theory of couples (*54, *55, *56).
The following proposition is useful in the theory of types. Its purpose is to show that, if is any argument for which "" is significant, i.e. for which we have , then "" is significant when, and only when, is either identical with a or not identical with . It follows (as will be proved in *20·81) that, if "" and "" are both significant, the class of values of for which "" is significant is the same as the class of those for which "" is significant, i.e. two types which have a common member are identical.
In the following proof, the chief point to observe is the use of *10·221. There are two variables, and , to be identified. In the first use, we depend upon the fact that and both occur in both (4) and (5): the occurrence of in both justifies the identification of the two 's, and when these have been identified, the occurrence of in both justifies the identification of the two 's. (Unless the 's had been already identified, this would not be legitimate, because "" is typically ambiguous if neither nor is of given type.) The second use of *10·221 is justified by the fact that both and occur in both (2) and (6).
*13·3.
Dem.