In a finite domain, an existential quantifier says that at least one candidate satisfies . Reason with a fresh name for such an unspecified witness. If the same conclusion follows using only and the original premises, without depending on which candidate names, then follows from the existential premise itself.
This is exactly existential elimination in boxed form: the sequent is the branch inside the box. The eigenvariable must not occur free in the original undischarged context or in the exported conclusion . Otherwise the proof could smuggle in information about a specially chosen individual or export a fact about a witness whose name has just left scope. Freshness does not mean that the domain contains an additional object; it means that its temporary name carries no other assumptions.
A uniform witness can serve every particular input. Two natural deduction proofs differ in whether universal introduction happens outside or inside the existential witness box.In both proofs is absent from the original premise. In the second it is also absent from the witness assumption, whose is bound; universal generalization is therefore legal inside that box. The exported conclusions contain no free .
Proof 1:
1 ∃y ∀x R(x,y) premise
2 | ∀x R(x,b) assumption, b fresh
3 | R(a,b) ∀-elim 2, with a arbitrary
4 | ∃y R(a,y) ∃-intro 3
5 ∃y R(a,y) ∃-elim 1,2–4
6 ∀x ∃y R(x,y) ∀-intro 5
Proof 2:
1 ∃y ∀x R(x,y) premise
2 | ∀x R(x,b) assumption, b fresh
3 | R(a,b) ∀-elim 2, with a arbitrary
4 | ∃y R(a,y) ∃-intro 3
5 | ∀x ∃y R(x,y) ∀-intro 4
6 ∀x ∃y R(x,y) ∃-elim 1,2–5The converse is not valid. On the domain , interpret as . For each , choose , so holds. Neither single choice of equals both 0 and 1, so fails. This is the distinction between a pointwise witness and a uniform witness.
The proposed proof is invalid: its existential-elimination step exports while the witness name still occurs free in that conclusion. Introducing an existential quantifier later does not retrospectively repair that scope error.
Introduce the existential quantifier before discharging the witness box:The conclusion of existential elimination now has no free occurrence of , and the name occurs in neither original premise, satisfying the eigenvariable condition.
1 ∀x (P(x) → Q(x)) premise
2 ∃x P(x) premise
3 | P(a) assumption, a fresh
4 | P(a) → Q(a) ∀-elim 1
5 | Q(a) →-elim 4,3
6 | ∃x Q(x) ∃-intro 5
7 ∃x Q(x) ∃-elim 2,3–6 Articles by others on the same topic
There are currently no matching articles.