I was introduced to EG as follows (for some name 'a'): One can infer from Fa to (∃x)Fx. But today within a proof my professor posted he used EG to infer from (∃x)Fx to (∃x)(∃x)Fx. I'm not sure how that is supposed to work. It seems he's taking the 'Fx' within (∃x)Fx and using EG to change that to (∃x)Fx in which case we get (∃x)(∃x)Fx. But isn't the EG rule supposed to be going from Fa to (∃x)Fx? How does one go from Fx to (∃x)Fx?


This is a lot simpler than it might seem. The details depend on how exactly the system that you're studying is set up but as an example let's look at the one defined in the Stanford Encyclopedia entry on classical logic.

In that entry, existential generalization (labeled ∃I) is defined as follows:

(∃I) For any closed term t, if Γ⊢θ(v|t) then Γ⊢∃vθ.

where θ(v|t) is defined as the result of substituting t for each free occurrence of v in θ. So suppose θ is Fx, then θ(x|a) would be Fa, and (∃I) tells us that if we've derived θ(x|a) (that is, Fa) we can also derive ∃xθ (that is, ∃xFx).

Here is the crucial part for your question: what happens when x does not occur free in θ? Then x cannot be replaced. That is, if θ is ∃xFx (in which x is bound) then θ(x|a) is also ∃xFx, since x does not occur free in θ. Remember that according to (∃I) we can derive ∃xθ if we have θ(x|a). So if θ is ∃xFx we can derive ∃xθ which is ∃x∃xFx.

In short, (∃I) lets you insert ∃x at the start of any derived formula in which x does not occur free.

| improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.