by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[Logic & Semantics, Entry Directory]
[Nolt, Logics, entry directory]
[The following is summary. All boldface in quotations are in the original unless otherwise noted. Bracketed commentary is my own.]
Summary of
John Nolt
Logics
Part 3: Classical Predicate Logic
Chapter 8: Classical Predicate Logic: Inference
8.5 Identity
Brief summary:
There are two identity inference rules for making proofs in predicate logic.
Identity Introduction (=I) Where α is any name, assert α = α.
Identity Elimination (= E) From a premise of the form α = β and a formula Φ containing either α or β, infer any formula which results from replacing one or more occurrences of either of these names by the other in Φ.
(241-242)
Summary
Nolt will explain how to make proofs in predicate logic when identity is involved. He will give two rules, namely, identity introduction ‘=I’ and identity elimination ‘=E’.
Identity Introduction (=I) Where α is any name, assert α = α.
(241)
As we can see, there are not any premises involved, and so it is not really a rule of inference. Rather, “It simply licenses us to assert a logical truth of the form α = α at any line of a proof” (Nolt 241). Nolt says that this rule is valid, because a logical truth is true no matter what the premises, even if there are no premises. [I am not certain, but perhaps the idea is like how you can insert a tautology into any proof, but I am not sure.] But since this rule does not need to be based on any particular line, we do not need to give a line number in the justification part of the proof. Nolt gives the example of a proof for the sequent
∀x∀y(x = y → Rxy) ⊢ Raa
[So let us set it up, by first placing the assumption.
| 1. | ∀x∀y(x = y → Rxy) | A |
In the proofs we made with Agler, we would put a ‘P’ for the premises, but here we place an ‘A’, perhaps to mean ‘assumption’ but I am not sure. With Agler, ‘assumption’ had a different meaning (it was used for starting subproofs). For Nolt, it seems we would use ‘H’ instead of ‘A’ when making a subproof, and perhaps the ‘H’ means ‘hypothesis’. But again I am not sure yet. At any rate, we are going to want to derive Raa. Since we are working with a universal quantifier, that means we will want to use universal elimination. Recall from Agler section 8.1 the rule:
| Universal Elimination (∀E) From any universally quantified proposition ‘(∀x)P,’ we can derive a substitution instance ‘P(a/x)’ in which all bound variables are consistently replaced with any individual constant (name). | (∀x)P P(a/x) | ∀E |
(Agler 325)
So using this rule and also the new identity introduction rule, we will want to go from ∀x∀y(x = y → Rxy) to obtain Raa. We could go one step at a time to get the constant a into the formulation, using universal elimination. So let us do that.
| 1. | ∀x∀y(x = y → Rxy) | A |
| 2. | ∀x(a = y → Ray) | 1∀E |
| 3. | a = a → Raa | 2∀E |
Now, recall that that the identity introduction rule says that “where α is any name, assert α = α”. So we have the name ‘a’. And were we to also have a = a, then we could use conditional elimination to derive our goal proposition. So let us do that.]
| 1. | ∀x∀y(x = y → Rxy) | A |
| 2. | ∀x(a = y → Ray) | 1∀E |
| 3. | a = a → Raa | 2∀E |
| 4. | a = a | =I |
| 5. | Raa | 3,4→E |
(Nolt 241)
Nolt then shows another “typical use of =I” with the proof for
⊢~∃x~x=x
(Nolt 241)
[Recall from section 6.3 that structures of the form ‘~a=b’ should be understood as meaning, ‘a is not identical to b’. So this formulation above is perhaps read, there is no x such that x is not identical to itself, or perhaps also, nothing is not identical to itself (or all things are identical to themselves). Recall from Agler Symbolic Logic section 5.4.2 strategic rule SA#1(P,¬Q):
SA#1(P,¬Q)
If the conclusion is an atomic proposition (or a negated proposition), assume the negation of the proposition (or the non-negated form of the negated proposition), derive a contradiction, and then use ‘¬I’ or ‘¬E.’
(Agler 199)
Since we want to prove ~∃x~x=x, we will assume the non-negated form. Then ultimately we will use negation introduction to derive the goal proposition.
| 1. | | ∃x~x=x | H (for ~I) |
Now recall from Agler Symbolic Logic section 8.1.4 the rule Existential Elimination.
| Existential Elimination (∃E) From an existentially quantified expression ‘(∃x)P,’ an expression ‘Q’ can be derived from the derivation of an assumed substitution instance ‘P(a/x)’ of ‘(∃x)P’ provided (1) the individuating constant ‘a’ does not occur in any premise or in an active proof (or subproof) prior to its arbitrary introduction in the assumption ‘P(a/x),’ and (2) the individuating constant ‘a’ does not occur in proposition ‘Q’ discharged from the subproof. | (∃x)P | P(a/x) | . | . | . | Q Q | ∃E |
(Agler 181)
What Nolt will do is use a rule that we did not get in Agler, namely, Ex Falso Quodlibet (EFQ): From Φ and ~Φ, infer any formula Ψ (Nolt 106). But let us first start the sub-subproof for the purpose of existential elimination.
| 1. | | ∃x~x=x | H (for ~I) |
| 2. | | | ~a = a | H (for ∃E) |
So we can see already that we are set up to find a contradiction. We will just expose it by using identity introduction.
| 1. | | ∃x~x=x | H (for ~I) |
| 2. | | | ~a = a | H (for ∃E) |
| 3. | | | a = a | =I |
We said that we need a contradiction in the main subproof. Nolt will then just directly derive a contradiction in the sub-subproof so that we accomplish this in one step in the subproof.
| 1. | | ∃x~x=x | H (for ~I) |
| 2. | | | ~a = a | H (for ∃E) |
| 3. | | | a = a | =I |
| 4. | | | P & ~P | 3,3EFQ |
Now we derive that self-contradictory proposition in the subproof, as planned, using existential elimination.
| 1. | | ∃x~x=x | H (for ~I) |
| 2. | | | ~a = a | H (for ∃E) |
| 3. | | | a = a | =I |
| 4. | | | P & ~P | 3,3EFQ |
| 5. | | P & ~P | 1,2-4∃E |
Now with a contradiction in our subproof, we can derive the negation of the original hypothesis, which was our goal proposition.]
| 1. | | ∃x~x=x | H (for ~I) |
| 2. | | | ~a = a | H (for ∃E) |
| 3. | | | a = a | =I |
| 4. | | | P & ~P | 3,3EFQ |
| 5. | | P & ~P | 1,2-4∃E |
| 6. | ~∃x~x=x | 1-5~I |
(Nolt 241)
Nolt gives this explanation for the process:
Since the desired conclusion ‘~∃x~x=x’ is negative, we hypothesize ‘∃x~x=x’ for indirect proof at line 1. But this is an existential formula, and so we hypothesize ‘~a = a’, a representative instance of it, for ∃E at line 2. We can now contradict line 2 by applying =I at line 3, but to obtain a contradiction that does not contain the name ‘a’ of the representative individual, we must use EFQ. Steps of ∃E and ~I then complete the proof.
(Nolt 241)
Identity Elimination is a matter of substituting identical things for one another:
The elimination rule for identity is familiar from algebra as the rule that allows us to substitute equals for equals – but in logic, since we are not dealing | only with quantities, it is more accurate to say ‘identicals for identicals.’ It is sometimes called the rule of identity substitution.
Identity Elimination (= E) From a premise of the form α = β and a formula Φ containing either α or β, infer any formula which results from replacing one or more occurrences of either of these names by the other in Φ.
Uses of =E are annotated by citing two line numbers: the number of the line on which α = β occurs and the number of the line on which Φ occurs.
(241-242)
Given that proving the validity of =E requires a lot of work, we will postpone such a proof until section 9.1. Until then, we will merely see how it is used. He gives as illustration the proof for:
⊢ (Fa & a = b) → Fb
(242)
[What we need to prove takes the form of a conditional. Recall strategic rule SA#2(→) from Agler Symbolic Logic section 5.4.2.
SA#2(→)
If the conclusion is a conditional, assume the antecedent, derive the consequent, and use ‘→I.’
(Agler 199)
So we will want to begin by hypothesizing the antecedent.
| 1. | | Fa & a = b | H (for →I) |
And we will want to derive the consequent so that we can use conditional introduction in order to derive the goal proposition. We also said that we would use identity elimination. Look again at the goal proposition: (Fa & a = b) → Fb. As we can see, we have an identity statement that will allow for a substitution that can give us our consequent. So first we will use conjunction elimination to extract the two parts of our hypothesis, which will allow us to make that substitution.
| 1. | | Fa & a = b | H (for →I) |
| 2. | | Fa | 1&E |
| 3. | | a = b | 1&E |
Now we will make the substitution using identity elimination to derive the goal proposition’s consequent.
| 1. | | Fa & a = b | H (for →I) |
| 2. | | Fa | 1&E |
| 3. | | a = b | 1&E |
| 4. | | Fb | 2,3=E |
And finally we can use conjunction introduction to derive the goal proposition.]
| 1. | | Fa & a = b | H (for →I) |
| 2. | | Fa | 1&E |
| 3. | | a = b | 1&E |
| 4. | | Fb | 2,3=E |
| 5. | (Fa & a = b) → Fb | 1-4→I |
(Nolt 242)
Nolt describes the reasoning this way:
The theorem is a conditional, so the overall strategy is conditional proof. With respect to the formal statement of the =E rule, α = β is ‘a = b’ and Φ is ‘Fa’.
(Nolt 242)
When the equated terms occur more than once in a formula, then we can substitute them in all the variety of ways that maintain the equality. So if we have ‘Laa’ and ‘a = b’, then we can use identity elimination to derive ‘Lab’ or ‘Lba’ or ‘Lbb’. We also can make our substitutions to ‘a = b’, since it also is a formula. Thus we can also derive ‘a = a’, ‘b = b’, and ‘b = a’. However, obtaining ‘b = a’ is not a derivation we can make in one step [because we are applying the rule separately for the first term and for the second]. So:
| 1. | a = b | A |
| 2. | b = b | 1,1=E |
| 3. | b = a | 1,2=E |
(Nolt 242)
From:
Nolt, John. Logics. Belmont, CA: Wadsworth, 1997.
Or if otherwise noted:
Agler, David. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman &; Littlefield, 2013.
.
No comments:
Post a Comment