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.
Articles by others on the same topic
There are currently no matching articles.