A fresh variable is an arbitrary eigenvariable whose value is not constrained by the undischarged assumptions. For universal introduction, it must not occur free in those assumptions; otherwise a fact about one constrained object could be incorrectly generalized to all objects. For existential elimination, its temporary witness must additionally not occur free in the conclusion or in other undischarged assumptions outside the witness subproof. Choosing a completely unused variable is a sufficient convention. These are the eigenvariable conditions, and concern free occurrences rather than harmless reuse of bound names.
Use a fresh witness in the existential elimination subproof. The universal elimination step gives the opposite of its assumed negated property.The witness is absent from the premise and from the conclusion of the existential-elimination step, so its freshness condition is met.
1. ∀x R(x) premise
2. ∃y ¬R(y) assumption [i]
3. ¬R(a) fresh witness assumption [j]
4. R(a) ∀E, 1
5. ⊥ ¬E, 3, 4
6. ⊥ ∃E, 2, 3–5, discharging [j]
7. ¬∃y ¬R(y) ¬I, 2–6, discharging [i]Take a fresh arbitrary variable . Assuming would provide precisely the witness forbidden by the premise; discharge that assumption before universal introduction.At line 6, is free in no undischarged assumption: line 2 has already been discharged. The change of bound variable name is part of the universal-introduction instance.
1. ¬∃x R(x) premise
2. R(a) assumption [i], a fresh
3. ∃x R(x) ∃I, 2
4. ⊥ ¬E, 1, 3
5. ¬R(a) ¬I, 2–4, discharging [i]
6. ∀y ¬R(y) ∀I, 5The result of part (ii), with replaced by , first yields . To show every use of the derived rule explicitly, one can instead write:The classical step is double-negation elimination at line 6. Freshness at line 7 holds after discharging the temporary assumption.
1. ¬∃x ¬R(x) premise
2. ¬R(a) assumption [i], a fresh
3. ∃x ¬R(x) ∃I, 2
4. ⊥ ¬E, 1, 3
5. ¬¬R(a) ¬I, 2–4, discharging [i]
6. R(a) ¬¬E, 5
7. ∀y R(y) ∀I, 6Choose distinct fresh variables . Instantiate the outer universal quantifier first, then the inner one; generalize them in the opposite order.Neither nor occurs free in the sole undischarged premise. Thus both universal introduction steps satisfy the eigenvariable condition.
1. ∀x ∀y P(x,y) premise
2. ∀y P(a,y) ∀E, 1
3. P(a,b) ∀E, 2
4. ∀x P(x,b) ∀I, 3, generalizing a
5. ∀y ∀x P(x,y) ∀I, 4, generalizing bKeep the two existential elimination scopes nested. Let witness the outer existential and the inner one, both fresh. Inside them, negation introduction proves the required counterexample to without invoking an unproved contraposition lemma.The result at lines 12–14 has no free occurrence of either fresh witness. At the inner discharge, is absent from the remaining assumptions; at the outer discharge, is absent from the premise and final conclusion. Hence the eigenvariable conditions hold at both eliminations.
1. ∀x ∀y (P(x,y) → Q(x,y)) premise
2. ∃y ∃x ¬Q(x,y) assumption [i]
3. ∃x ¬Q(x,b) fresh witness assumption [j]
4. ¬Q(a,b) fresh witness assumption [k]
5. ∀y (P(a,y) → Q(a,y)) ∀E, 1
6. P(a,b) → Q(a,b) ∀E, 5
7. P(a,b) assumption [l]
8. Q(a,b) →E, 6, 7
9. ⊥ ¬E, 4, 8
10. ¬P(a,b) ¬I, 7–9, discharging [l]
11. ∃x ¬P(x,b) ∃I, 10
12. ∃y ∃x ¬P(x,y) ∃I, 11
13. ∃y ∃x ¬P(x,y) ∃E, 3, 4–12, discharging [k]
14. ∃y ∃x ¬P(x,y) ∃E, 2, 3–13, discharging [j]
15. (∃y ∃x ¬Q(x,y)) → (∃y ∃x ¬P(x,y))
→I, 2–14, discharging [i] Articles by others on the same topic
There are currently no matching articles.