I'm reading the book "Gödel's incompleteness theorems" by Smullyan. (I found it online here: https://isidore.co/calibre/get/pdf/5823). In Chapter III he explains the Axiom System for Peano Arithmetic, and on page 29 he defines the axiom scheme for mathematical induction. I don't understand this definition.
He says:
In displaying this scheme, $F(v_1)$ is to be any formula at all (it may contain free variables other than $v_1$). By $F[v_1']$ we shall mean any one of the formulas
(I) $\forall v_i(v_i=v_1’ \supset \forall v_1(v_1=v_i \supset F))$
where $v_i$ is any variable that does not occur in F. ... Here is the scheme:
(II) $(F[\bar{0}] \supset (\forall v_1(F(v_1) \supset F[v_1’]) \supset \forall v_1 F(v_1)))$
I do not understand the first line (I), for two reasons: Firstly, $v_1$ appears as bounded variable (this is the $\forall v_1$ part), and as free variable (this is the $v_1'$ part). How can this be? (The accent symbol ($'$) is the successor symbol.) Secondly, $F$ appears without argument. Must it replaced by $F(v_1)$? The second line (II) seems clear, but the first line (I) seems wrong. Can anyone explain this?
It's not a problem for a variable to have both free and bound occurrences in a formula (although it can certainly be confusing).
What Smullyan is doing with (I) is getting a formula that is equivalent to $F(v_1/v_1')$ (i.e. the formula $F$ with the term $v_1'$ substituted for each free occurrence of $v_1$) without actually doing any substitution. This is a trick done for technical reasons, because substitution is a headache to "Godelize", whereas this transformation is pretty simple.
In fact, using both free and bound occurrences is essential to how this trick works. The free occurrence let's us say that $v_i$ takes the value of $v_1'$ and then binding $v_1$ allows us to pass this value we put into $v_i$ into the free occurences of $v_1$ in $F.$ Smullyan uses a simpler version of this trick (that he attributes to Tarski) earlier, on page 25.
As for your second question, $F$ is just a formula. Writing it as $F(v_1)$ instead of $F$ doesn't change what it is... it is just a cue that $v_1$ is a variable we are singling out informally, perhaps so we can talk about substituting for it, as is the case here. However, some authors will also use this notation as a guarantee that $v_1$ occurs freely in $F,$ or is the only variable that occurs freely in $F,$ but even in this case it's just informal notation, not a distinct thing from the formula $F.$ More confusingly, sometimes authors will subsequently write $F(t)$ to denote $F$ with the term $t$ substituted for each free instance of $v_1$ (rather than something clearer like $F(v_1/t)$).