I have a question that has been bothering me for quite some time. In second order logic sometimes there is an indication that a variable can be both bound and free. The simplest example I can give is using the variable $v_0$ and the constants $c_0, c_1$ who are not equal to one another. How does one interpret the following formula. $$(v_0=c_0)\wedge \left[ \exists v_0 (v_0 = c_1)\right]$$
I see a few possible interpretations:
- The statement is not actually valid because variables cannot be both bound and free.
- The formula will always be false because $(v_0=c_0)$ restricts $v_0$ such that there cannot exist a $v_0=c_1$
- The formula is true when $v_0=c_0$ because one essentially treats the free version of a variable differently from the bound version such that even though $v_0=c_0$ in this particular instance, it still theoretically could be that a variable $v_0$ equals the constant $c_1$ and thus the existence clause is satisfied as well.
I also recognize that it could be something completely different from any of these that I have not thought of yet, I was just curious if there was an accepted way to handle variables which are both free and bound because I have not found any satisfying answers as of yet.
The best way to think of it is that the name of a bound variable is not visible outside its binder (in this case, outside its quantifier). So the intuitive content of $$ (v_0=c_0) \land \exists v_0(v_0=c_1) $$ is exactly the same as $$ (v_0=c_0) \land \exists v_{99}(v_{99}=c_1) $$
Thus, your option 3 is right.
The exact mechanism that is used to achieve this equivalence differs a bit from context to context. If you look at it semantically (as the model-theory tag suggests), the case for $\exists x\,\phi$ in the definition of $\vDash$ will usually make it clear that the value of $x$ in the surrounding variable assignment is ignored and replaced by a new arbitrary value for the purpose of interpreting $\phi$.
When we view the formulas syntactically, the equivalence between $\exists x\,\phi(x)$ and $\exists y\,\phi(y)$ is sometimes built into the notion of substitution ("capture-avoiding substitution" will automagically rename bound variables as necessary to prevent problems); at other times the two formulas are merely provably equivalent, and you're supposed to explicitly use that equivalence before you apply a proof step that requires the substitution $\bigl(\exists x\,\phi(x,y)\bigr)[y\mapsto \cdots x\cdots]$.
(As a general trend, computer scientists seem to tend to prefer working with capture-avoiding substitution, whereas logicians tend to require explicit renaming of bound variables before one can do a substitution that would otherwise capture a variable. But plenty of exceptions to this can be found).