Bound & Unbound Variables Renaming

Usually students have some problem to remember the technique of renaming bound and unbound variables in PL. Here's a tactic, considering higher or lower groups. But firstly let's draw the firsts:

where Q is a quantor and P₁..._n are predicates. The formula 1 supposes all the variables α to be bound by the quantor. Let's have a look into another one:


In this last formula 2 all the variables are bound, except for the first β, which is not (because there are no quantors with β ahead of it). But some troubles with renaming may occur especially if there are similar quantified variables occurs. In the formula 1 just one quantor is there, and that is why there are no other renaming, except for to rename all the variables at the same time. In the formula 2 we cannot rename bound variables as we'd like to. All we have to do is to more from the nearest to the fartherst quantors. The nearests must be renamed firstly, and to rename them we have not to break the rule:

that is why it's no good to rename a bound variable that after that turns into an unbound. Let's try to rename some in 2:

        S1. Qα(...Qα(...α...β...Qβ(...α...β...)...)...)
        S2. Qα(...Qγ(...γ...β...Qβ(...γ...β...)...)...)
        S3. Qβ(...Qβ(...β...β...Qβ(...β...β...)...)...)

The transition from s1 to s2 is correct - we changed the variable α into γ in the inner formula. The transition from s2 to s3 has two mistakes: we cannot make the first unbound variable β be bound, and we cannot transform the bound variables γ into β. We might change the unbound variable β into some other variable, let's say δ. All we must be careful at - not to make the unbound variable to be bound. That's why any unbound variables are better to rename introducing new variables. The correct renaming of s2 may be look like:

        S4. Qα(...Qγ(...γ...δ...Qβ(...γ...β...)...)...)