Section 8.7 introduces three rules for drawing inferences with identities. The text calls all three ID but LogicCoach adds a distinguishing numeral to the ID.
| ID.1 | p | // | a=a | |||
| ID.2 | a=b :: b=a | |||||
| ID.3 | ƒa | / | a=b | // | ƒb |
ID.1 and ID.3 are implication rules while ID.2 is a replacement rule
WARNING: The ID rules are only defined for individual constants. They cannot be applied to variables. To prove an identity about universally quantified variables, consider indirect proof
ID.1 The p in the form's premise indicates that any premise can be used to justify writing that an individual constant is identical to itself. The identity is a logical truth.
ID.2 This replacement rule functions for identity as COM functions for • and for ∨
ID.3 Any line that contains an individual constant can be thought of as a compound property of that individual. Thus (x)(Fx ⊃ Fd) is the property of d and not just the F-predicate. This allows ID.3 to be used to replace the d in (x)(Fx ⊃ Fd) with any other individual constant to which it is identical.
|
1. 2. 3. |
(x)(Fx ⊃ Fd) d=e (x)(Fx ⊃ Fe) |
1,2 ID.3 |