What set of formal rules can we use to safely apply Universal/Existential Generalizations and Specifications?

Note: I've accepted Mauro ALLEGRANZA's answer, as it was the one that solved the problem for me. However, it didn't really get into the rules. So, to keep a record (and for anyone that also has this question but doesn't want to get into the book), I've come back to complement his answer with an explanation of the ruleset discussed in the book, so that you can use to keep your arguments sound when using any Specification and Generalization.

“I apologize for such a long letter - I didn't have time to write a short one.” - Mark Twain

Before I answer, it's important to note that, as pointed by Mauro, there's no single answer for this question. There are different systems capable of solving the fallacies that generalizations and specifications can bring, and they should not be mixed. If you choose to use this ruleset, or any other, keep in mind that they are meant to be used individually, as mixing them might result in a incomplete (too restrictive) system, or an unsound (illogical) system. So, do not mix rulesets.

For those looking for the original source, the ruleset given here is taken from the book Introduction to Logic (1957), by Patrick Suppes.

Note: You may notice that the naming scheme used here differs from the book ($\alpha$ to $x_\alpha$, flagged variables to distinct variables, ambiguous variables to restricted variables). The reason is that I feel this naming scheme makes the ideas presented more intuitive. However, it's just a matter of presentation. The ideas and rules behind them are the same.

Motivation

Here we show the setbacks, and the natural solutions to them. For now, don't worry about memorizing the rules, as the complete list will be given in the end. This part is only meant build some intuition on why these rules are necessary.

When building an argument using quantifiers, there are 3 main things that we have to pay attention to avoid fallacies:

• Mixing different variable classes
• Mixing quantifiers
• Variables getting caught by different quantifiers

Mixing different variable classes

There are 3 types of free variables:

• Those that are free in our premises (as in the premise $P(a)$)
• Those that are freed from an exisitential quantifier (as in the deduction $\exists x [P(x)] \vdash P(a)$)
• Those that are freed from an universal quantifier (as in the deduction $\forall x [P(x)] \vdash P(a)$)

Treating these classes the same way will quickly lead to fallacies, as shown by the example in the question. Intuitively, the first type represents a distinct variable, a single example from the domain of discourse. The second type represents only objects for which some restricted context applies (i.e. the predicates inside the existential quantifier). The third type represents an object which we have no assumptions about, so any object in the domain of discourse. To avoid confusion, let's separate them:

• New concept - Distinct variable: Free variables that represent a specific object from the domain of discourse.

• New concept - Restricted variable: Free variables that represent objects restricted by some context.

• New concept - Arbitrary variable: Free variables which we have no assumptions about, that may represent any object from the domain of discourse.

Then specify where they appear and some notation so we can differentiate between them:

• [1] New $\tt{P}$ rule: Any variable present in an undischarged premise, is a distinct variable. They may be marked on the side of the line in which they are introduced.

• [2] New ${\exists}\tt{E}$ rule: Every variable created by ${\exists}\tt{E}$ must be a new/not yet used restricted variable. They may be marked as such with a subscript lowercase greek letter (e.g. $x_\alpha$, $x_\beta$, $y_\gamma$).

• [3] New ${\forall}\tt{E}$ rule: Any variable created by ${\forall}\tt{E}$ is an arbitrary variable.

So, in this example:

$$ %PREAMBLE \newcommand{\nwcm}{\newcommand} \nwcm{\fitch}[1]{\begin{array}{rlr}#1\end{array}} \nwcm{\fcol}[1]{\begin{array}{r}#1\end{array}} %FirstColumn \nwcm{\scol}[1]{\begin{array}{l}#1\end{array}} %SecondColumn \nwcm{\tcol}[1]{\begin{array}{l}#1\end{array}} %ThirdColumn \nwcm{\subcol}[1]{\begin{array}{|l}#1\end{array}} %SubProofColumn \nwcm{\startsub}{\\[-0.29em]} %adjusts line spacing slightly \nwcm{\endsub}{\startsub} %adjusts line spacing slightly \nwcm{\fl}{\\[0.044em]} %adjusts line spacing slightly \nwcm\liff{\leftrightarrow} \nwcm\lif{\rightarrow} \nwcm\foll{\forall} \nwcm\exi{\exists} \nwcm\tt{\text} \nwcm\exE{{\exi}\tt{E}} \nwcm\exI{{\exi}\tt{I}} \nwcm\follI{{\foll}\tt{I}} \nwcm\follE{{\foll}\tt{E}} \fitch{ \fcol{1:\fl 2:\fl 3:\fl 4:\fl 5:\fl } & \scol { P(a) \\ \exi x[P(a) \lif Q(x)] \\ P(a) \lif Q(x_{\alpha}) \\ Q(x_{\alpha}) \\ \exi x [Q(x)] \\ } & \tcol{ \tt{P}[a] \fl \tt{P}[a] \fl 2\ \exE \fl 1,3\ {\lif}\tt{E} \fl 3\ \exI \fl } }$$

$a$ is a distinct variable, and is marked as such on the right in line $1$ as "$P[a]$", and $x_{\alpha}$ is a restricted variable, and is marked as such with the $_{\alpha}$ subscript.

Now we may develop some rules to make sure that these definitions are being used in a logical manner. It should be intuitively clear that you may apply $\exI$ with any variable class you wish, but the fallacious example in the question shows that this is not the case with $\follI$, so:

• [4]. New $\follI$ rule: You may only generalize from arbitrary variables.

Here's an important note on rule [1]. Arbitrary variables represent an object that we have no assumptions about, so it makes sense that when we introduce a variable in a premise, it's not abitrary, since we've made assumptions about it. However, this also means that if we discharge all assumptions about it, it becomes arbitrary. This is why rule [1] specifies undischarged premises.

Consider this argument: "All pigs are animals. Suppose that a head belongs to a pig. Then the head belongs to an animal. Therefore, all heads of pigs are heads of animals.". Notice that in this argument, the distinct "a head" became the universal "all heads". This happened because the proposition "Suppose that a head [...]" is discharged by the end of the argument. This gets more clear if we formalize the argument:

$$ \fitch{ \fcol{1:\fl 2:\fl 3:\fl 4:\fl 5:\fl 6:\fl 7:\fl 8:\fl 9:\fl} & \scol{ \foll x[P(x) \lif A(x)] \startsub \subcol{ \exi x[P(x) \land H(y,x)] \\ \hline P(x_\alpha) \land H(y, x_\alpha) \\ P(x_\alpha) \lif A(x_\alpha) \\ A(x_\alpha) \\ A(x_\alpha) \land H(y, x_\alpha) \\ \exi x[A(x) \land H(y, x)] \\ } \endsub \exi x[P(x) \land H(y,x)] \lif \exi x[A(x) \land H(y, x)] \\ \foll y [\exi x[P(x) \land H(y,x)] \lif \exi x[A(x) \land H(y, x)]] } & \tcol{ \tt{P} \fl \tt{P}[y] \fl 2\ \exE[x/x_\alpha] \fl 1\ \follE \fl 3,4\ {\lif}\tt{E} \fl 3,5\ {\land}\tt{I} \fl 6\ \exI[x_\alpha/x] \fl 2,7\ {\lif}\tt{I} \fl 8\ \follI[y] } } $$

Line $2$ introduced $y$ in a premise, but that premise is discharged on line $8$, so from that point on, $y$ is arbitrary, and we are free to apply ${\foll}{I}$ on line $9$. So remember, a variable is only distinct if it's in an undischarged premise.

It should also make intuitive sense that we may subsitute an arbitrary variable for a variable of any other class, since it is arbitrary. Here are examples of this happening under $\follE$ and $\exI$, respectively:

$$\begin{array}{rll|rll} 1: & \foll n[n+0=n] & \tt{P}[0]& 1: & \exi x \foll n[n+x=n] & \tt{P} \\ 2: & 0+0=0 & 1\ \follE & 2: & \foll n[n+x_{\alpha}=n] & 1\ \exE \\ 3: & \exi n[n+n=n] & 2\ \exI & 3: & n+x_{\alpha}=n & 2\ \follE\\ &&& 4: & \exi n[n+n=n] & 3\ \exI[x_{\alpha}/n]\\ \end{array} $$

In the first example, the arbitrary $n$ is substituted for the distinct $0$ in line $2$. In the second one, the arbitrary $n$ is equated with the restricted $x_{\alpha}$ in line $4$. Since they are arbitrary, they may represent any individual or class of objects, no foul play here.

However if a non-arbitrary variable gets equated with a different non-arbitrary variable, that may cause a problem:

$$\begin{array}{rll|rll} 1: & \exi a \exi x[a < x] & \tt{P} & 1: & \exi x[a < x] & P[a] \\ 2: & \exi x[a_{\alpha} < x] & 1\ \exE & 2: & a < x_{\alpha} & 1\ \exE \\ 3: & a_{\alpha} < x_{\alpha} & 2\ \exE & 3: & \exi a[a < a] & 2\ \exI[x_{\alpha}/a] \tt{(fallacy)} \\ 4: & \exi x_{\alpha}[x_{\alpha} < x_{\alpha}] & \exI[a_{\alpha}/x_{\alpha}] \tt{(fallacy)}\\ \end{array} $$

The "$\exi x_{\alpha}$" on the left example is especially silly. The point of restricted variables is to use them as free variables, outside of the existential quantifier, so there is no point using $\exI$ to them. $\exE$ should create restricted variables, and $\exI$ should destroy them. As for the example on the right, we need to make sure that the variable being equated to is arbitrary. So we may state those as:

• [5] New $\exI$ rule: Do not generalize to restricted variables.

• [6] New $\exI$ rule: You may only generalize to a different variable already present in the formula if it is arbitrary.

So in our left example, line $4$ generalizes to $x_{\alpha}$, which is restricted, breaking rule [5]. In the right one $a$ is distinct, not arbitrary, so step $3$ breaks rule [6].

Two things to note on rule [6]. First, the word "different". As we said before, the problem happens when "a non-arbitrary variable gets equated with a different non-arbitrary variable". If the variable at the end uses the exact same symbol however, it's not getting equated with anybody else, and no problem emerges. So going from $P(x)$ to $\exi x[P(x)]$ is always valid, as they use the same symbol. The second note is on "already present in the formula". If the end variable is not present in the formula, it'll not be equated with any other free variable, so you're safe to generalize to it. So going from $P(x)$ to $\exi a[P(a)]$ is always valid, because $a$ was not present in the formula, even if $a$ is distinct somewhere else.

Another thing worth pointing out is the "new/not yet used" part of rule [2]. As rule [5] resolves the problem of different non-arbitrary variables getting equated for $\exI$, this part of rule [2] does the same for $\exE$. Take this argument:

$$ \begin{array}{rll} 1: & \exi x \exi y[x < y] & \tt{P} \\ 2: & \exi y[x_\alpha < y] & 1\ \exE[x/x_\alpha] \\ 3: & x_\alpha < x_\alpha & 2\ \exE[y/x_\alpha]\ \tt{(fallacy)} \\ 4: & \exi x[x < x] & 3\ \exI \\ \end{array} $$

Here, two non-arbitrary variables under different quantifiers ($x$ and $y$) got equated in line $3$ because a restricted variable was reused, which resulted in a fallacy. So don't forget that part of rule [2], always use a new/not yet used restricted variable on each $\exE$.

With these in place, we won't mix variable classes.

Mixing quantifiers

In this case the first problem is changing the order of quantifiers, which is easy to exemplify. Take the assertion "there's no greatest number", or $\foll x \exi y [x < y]$, if we invert its quantifiers we produce the complete opposite phrase $\exi y \foll x[x < y]$. We may derive this contradiction like so:

$$ \begin{array}{rll} 1: & \foll x \exi y [x < y] & \tt{P} \\ 2: & \exi y [x < y] & 1\ \follE \\ 3: & x < y_{\alpha} & 2\ \exE \\ 4: & \foll x[x < y_{\alpha}] & 2\ \follI \tt{(fallacy)} \\ 5: & \exi y \foll x[x < y] & 2\ \exI \\ \end{array} $$

The order of the quantifiers within the same formula should be maintained.

The second one is more subtle:

$$ \begin{array}{rll} 1. & \foll x \exi y [x < y] & \tt{P} \\ 2. & \exi y [x < y] & 1\ \follE \\ 3. & x < y_{\alpha} & 2\ \exE \\ 4. & \exi x[x < x] & 3\ \exI \tt{(fallacy)} \\ \end{array} $$

$x$ is arbitrary, so it would seem that equating $y_{\alpha}$ to it under $\exI$ is fine, but it results in a fallacy. So what is going on here?

When restricted variables were presented, it was mentioned that it "represents only objects for which some restricted context applies (i.e. the predicates inside the existential quantifier)", but what wasn't said on that parenthesis is that not only the predicates are part of the context, but also the free variables within it. In both cases we are failing to account for this, so luckily, we can kill two birds with one stone here.

In the examples above, the restricted variable $y$ depends specifically on being greater than $x$, so we cannot subsitute for it. We may say that the restricted variable depends on the other free variables present. So, let's describe that dependence:

• [2] Improved $\exE$ rule: Every variable created by $\exE$ must be a new/not yet used restricted variable. They may be marked as such with a subscript lowercase greek letter (e.g. $x_\alpha$, $x_\beta$, $y_\gamma$). In case there are non-restricted variables free in the formula, they may be added to the subscript (e.g. $x_{\alpha y}$, $x_{\beta zy}$, $y_{\gamma x}$).

• [7] New $\exI$ rule: Do not generalize to a variable that is a subscript in the formula.

• [8] New $\follI$ rule: Do not generalize to a variable that is a subscript in the formula.

Two points to note. The first one is that rule [2] mentions only non-restricted variables. This is because the other rules we have in place are already enough to stop these problems from occurring for restricted ones (even without the new rules). So, we only need to subscript non-restricted variables. The second one is that being in a subscript counts as "present in the formula". So, the formula $\exi x[P(x,y_{\alpha z})]$ will not become $P(x_{\alpha},y_{\alpha z})$, but $P(x_{\alpha z},y_{\alpha z})$, as $z$ was present in a subscript.

With these rules in place, no quantifiers will be mixed.

Variables getting caught by different quantifiers

When applying some specification, such as $\exE$ or $\follE$, the intention is to free the varable. A specification from a statement like $\foll x \foll y[P(x,y)]$ to $\foll y[P(y,y)]$ is problematic, as the variable was not freed, since it was caught by the "$\foll y$" quantifier.

In the same vein, when applying a generalization, such as $\exI$ or $\follI$, the intention is for the variable to be bounded by the quantifier you just created, and not by any other. That makes a generalization from a statement like $\foll y[P(x,y)]$ to $\exi y \foll y[P(y,y)]$ also problematic, as the variable was caught by the "$\foll y$" quantifier.

This type of deducition can lead to fallacies when applied with any generalization or specification. Here are examples for all of them:

$$\begin{array}{rll|rll} 1: & \foll y \exi x[y < x] & \tt{P} & 1: & \exi x \foll y[x+y=y] & \tt{P} \\ 2: & \exi x[x < x] & 1\ \follE \tt{(fallacy)} & 2: & \foll y[y+y=y] & 1\ \exE \tt{(fallacy)} \\ \hline 1: & \foll y \exi x[y < x] & \tt{P} & 1: & \exi x \foll y[x+y=y] & \tt{P} \\ 2: & \exi x[y < x] & 1\ \follE & 2: & \foll y[x_{\alpha}+y=y] & 1\ \exE \\ 3: & \foll x \exi x[x < x] & 2\ \follI \tt{(fallacy)} & 3: & \exi y \foll y[y+y=y] & 2\ \exI \tt{(fallacy)} \\ \end{array}$$

All of these fallacious arguments stem from the same problem, the variable being freed or bounded getting caught by another quantifier. So even more luckily in this case, we can kill four birds with one stone:

• [9] New $\follE$ rule: The variable may not caught by another quantifier.

• [10] New $\exE$ rule: The variable may not caught by another quantifier.

• [11] New $\follI$ rule: The variable may not caught by another quantifier.

• [12] New $\exI$ rule: The variable may not caught by another quantifier.

This might look like a lot, but it's actually just one rule to remember, as it applies to any case. So just remember "your variable may not caught by another quantifier" and you're safe from this one.

Note: In the book, this rule is only given for $\exI$ and $\follE$. The $\exE$ and $\follI$ versions are not strictly necessary for soundness, as other rules already stop these cases (for example, the top right argument already breaks [2]). However, it's way easier to remember it as one single rule for all of them.

Extra rule on restricted variables

It's important to note that there should be no restricted variables present in your conclusion. They are a means to an end, not the end itself. If your conclusion is $P(x_\alpha) \lif Q(x_\alpha)$, what you actually meant was $\exi x[P(x) \lif Q(x)]$. So:

• New concept - U-Closure: Any formula that doesn't contain restricted variables has unrestricted closure, or U-Closure.
• [13] New rule: All formulas on conclusions should have U-Closure.

[13] might seem like an optional rule, but not using it can lead to a fallacy when you start using derived formulas (i.e. shortcut steps) on your arguments, as two restricted variables from different proofs which happened to use the same symbol might be equated, which would lead to the problem of "mixing non-arbitrary variables". So it is indeed a rule, not a rule of thumb.

It is worth pointing out that "inline conclusions", such as ones from a reductio ad absurdum or a conditional proof do not count as conclusions. This rule is meant only for the actual conclusion of the formal proof.

Summarizing

Now that you know how each rule fits into the construction of a sound deduction system, I can present to you the full list of definitions and rules.

Note that, even though the list is long and verbose, a lot of the rules are repeated, and for some, breaking them looks so wrong that you'll naturally follow them (you may already be actually). Probably the hardest are the ones that manage restricted variables and its subscripts (such as when you have $x_\alpha$, $y_{\alpha x}$, or $z_{\beta b}$). Having that said, here's the list:

Definitions

Distinct Variables: Free variables that represent a distinct object from the domain of discourse.
Restricted Variables: Free variables that represent objects restricted by some context.
Arbitrary variables: Free variables which we have no assumptions about, that may represent any object from the domain of discourse.
U-Closure: If a formula has no restricted variables then it has Unrestricted Closure, or U-Closure.

Rules

Premise: Any free variable present in an undischarged premise, is a distinct variable. They may be marked on the side of the line in which they are introduced for clarity.

Universal Elimination: From $\foll x [P(x)]$ you may derive $P(a)$ if:

• $a$ will not be caught by any different quantifier in the result formula.

Existential Elimination: From $\exi x [P(x)]$ you may derive $P(a)$ if:

• $a$ will not be caught by any different quantifier in the result formula.
• $a$ must be a new/not yet used restricted variable. It may be marked as such with a subscript lowercase greek letter (e.g. $x_\alpha$, $x_\beta$, $y_\gamma$). In case there are non-restricted variables free in the formula, they may be added to the subscript (e.g. $x_{\alpha y}$, $x_{\beta zy}$, $y_{\gamma x}$)

Universal Introduction: From $P(a)$ you may derive $\foll x [P(x)]$ if:

• $x$ will not be caught by any different quantifier in the result formula.
• $a$ is not present as a subscript in the formula.
• $a$ is arbitrary.

Existential Introduction: From $P(a)$ you may derive $\exi x [P(x)]$ if:

• $x$ will not be caught by any different quantifier in the result formula.
• $a$ is not present as a subscript in the formula.
• when $x$ is already present in the formula as a different variable, this variable is arbitrary.
• $x$ is not restricted.

General:

• All conclusions must have U-Closure.

Tips

Starting the argument

At the start of the argument, you'll usually try to eliminate all the quantifiers first, make your deductions, then reestablish the necessary ones at the end to get U-Closure. Like on the following syllogism:
"All pigs are animals. There are some pigs. Therefore, there are some animals": $$ \begin{array}{rll} 1: & \foll x [P(x) \lif A(x)] & \tt{P} \\ 2: & \exi x[P(x)] & \tt{P} \\ 3: & P(x_\alpha) & 2\ \exE \\ 4: & P(x_\alpha) \lif A(x_\alpha) & 1\ \follE \\ 5: & A(x_\alpha) & 3,4\ {\lif}\tt{E} \\ 6: & \exi x[A(x)] & 5\ \exI \\ \end{array} $$

Here we eliminate the quantifiers on lines $3$ and $4$, make our deduction on line $5$, and reestablish the necessary quantifiers on line $6$ to get U-Closure.

Now that you know that structure, here's the tip: At the beginning, eliminate the existentials first, then the universals. Here's the reason: Differently from $\exE$, there's no restriction on $\follE$ saying that we need a new variable, or even if it has to be restricted or not, so we can freely $\follE$ $x$ to $x_\alpha$ on line $4$. In fact, you can $\follE$ to almost any variable. However, let's see at what happens when we try to eliminate the universal quantifier first: $$ \begin{array}{rll} 1: & \foll x [P(x) \lif A(x)] & \tt{P} \\ 2: & \exi x[P(x)] & \tt{P} \\ 3: & P(x) \lif A(x) & 1\ \follE \\ ? \\ \end{array} $$

Now, we can't do much. We could try to use $\exE$ with line $2$, but that'd give us $P(x_\alpha)$, with a new variable. As $x_\alpha$ is different than $x$, it can not be used with $P(x) \lif A(x)$ to finish the argument. So as a rule of thumb, at the start, $\exE$, only then $\follE$.

Finishing the argument

The tip I just gave has a very important implication: a statement like $\exi x \foll y[P(x,y)]$ is much more useful than $\foll x \exi y[P(x,y)]$. In the former you can $\exE$ first, and then $\follE$, (possibly) making your deductions much easier, while the latter forces you to $\follE$ first. So if you have a statement like $P(x,a_\alpha)$ in your conclusion, assuming that $x$ is arbitrary, you want to end with $\exi a \foll x P(x,a)$ instead of $\foll x \exi a P(x,a)$. So your instinct should be to, at the end, $\follI$, only then $\exI$.

That is not always possible however, since $\follI$ is more restrictive than $\exI$. As an example, let's take $(P(x, a_{\alpha x}) \land Q(y,b_{\alpha xy}))$. Our dream would be to end with $\exi a \exi b \foll x \foll y [(P(x, a) \land Q(y,b))]$, with the existentials first. We're not so lucky on this one though. Notice that the first generalization ($\foll y$) is invalid, since $y$ appears as a subscript in $b_{\alpha xy}$. So, we first have to apply $\exI$ on $b_{\alpha xy}$ to get $\exi b[P(x, a_{\alpha x}) \land Q(y,b)]$ , then, with no $y$ in any subscript, we can $\follI$ it, resulting in $\foll y \exi b [(P(x, a_{\alpha x}) \land Q(y,b))]$. Again, it'd be great to $\follI$ on $x$, but unfortunately, it appears as a subscript on $a_{\alpha x}$, so, we have to $\exI$ it first, getting $\exi a \foll y \exi b [(P(x, a) \land Q(y,b))]$, only then, without $x$ appearing in any subscript, we can $\follI$, resulting in $\foll x \exi a\foll y \exi b [(P(x, a) \land Q(y,b))]$. Not the statement we dreamed about, but the best version we could hope for.

Now, that whole process might have seem a bit convoluted, but in reality there's a nice pattern to it.

To arrive a better U-Closure, use the following steps:

1. $\follI$ all arbitrary variables that do not appear as a subscript in the formula. Skip this step if there are none.
2. $\exI$ the restricted variable with the largest amount of subscripts.
3. Repeat steps 1 and 2 until you arrive at a formula with U-Closure.

This gives you the optimal U-Closed formula in your conclusion.

As an example, here's the optimal U-Closure for the (long) phrase $(P(x, a_{\alpha xy}) \land Q(x,y,b_{\alpha x}) \lif P(z,c_{\alpha yz})) \lor P(z, d_{\alpha xyz})$:

$$ \fitch{ \fcol{} & \scol{ \exi d [(P(x, a_{\alpha xy}) \land Q(x,y,b_{\alpha x}) \lif P(z,c_{\alpha yz})) \lor P(z, d)] \\ \exi c \exi d [(P(x, a_{\alpha xy}) \land Q(x,y,b_{\alpha x}) \lif P(z,c)) \lor P(z, d)] \\ \foll z \exi c \exi d [(P(x, a_{\alpha xy}) \land Q(x,y,b_{\alpha x}) \lif P(z,c)) \lor P(z, d)] \\ \exi a \foll z \exi c \exi d [(P(x, a) \land Q(x,y,b_{\alpha x}) \lif P(z,c)) \lor P(z, d)] \\ \foll y \exi a \foll z \exi c \exi d [(P(x, a) \land Q(x,y,b_{\alpha x}) \lif P(z,c)) \lor P(z, d)] \\ \exi b \foll y \exi a \foll z \exi c \exi d [(P(x, a) \land Q(x,y,b) \lif P(z,c)) \lor P(z, d)] \\ \foll x \exi b \foll y \exi a \foll z \exi c \exi d [(P(x, a) \land Q(x,y,b) \lif P(z,c)) \lor P(z, d)] } & \tcol{ \exI[d_{\alpha xyz}/d] \fl \exI[c_{\alpha yz}/c] \fl \follI[z] \fl \exI[a_{\alpha xy}/a] \fl \follI[y] \fl \exI[b_{\alpha x}/b] \fl \follI[x] \fl } } $$

Examples

It might be useful to see these in action in some examples, so let's prove some arithmetic facts using the following axioms:

• $\tt{Axiom }[a]$: $\foll x \foll y \foll z [x+(y+z)=(x+y)+z]$
• $\tt{Axiom }[b]$: $\foll x[x+(-x)=0]$
• $\tt{Axiom }[c]$: $\foll x[x+0=x]$

Notice that, since $0$ is free in these axioms, and axioms are never discharged, the variable $0$ is distinct in all of the theorems.

$\tt{Theorem [1]: }\foll x \foll y \foll z [x=y \liff x+z=y+z]$.
$\tt{Proof:}$

$$\fitch{ \fcol{1:\fl 2:\fl 3:\fl 4:\fl 5:\fl 6:\fl 7:\fl 8:\fl 9:\fl 10:\fl 11:\fl 12:\fl 13:\fl 14:\fl 15:\fl 16:\fl 17:\fl 18:\fl 19:\fl} & \scol{ \subcol{ x=y \\ \hline x+z = x+z \\ x+z = y+z } \endsub x=y \lif x+z=y+z \startsub \subcol{ x+z = y+z \\ \hline (x+z)+(-z)=(x+z)+(-z) \\ (x+z)+(-z)=(y+z)+(-z) \\ (x+z)+(-z) = x+(z+(-z)) \\ (y+z)+(-z) = y+(z+(-z)) \\ x+(z+(-z))=(y+z)+(-z) \\ x+(z+(-z))=y+(z+(-z)) \\ z+(-z) = 0 \\ x+0=y+0 \\ x+0=x \\ y+0=y \\ x=y } \endsub x+z=y+z \lif x=y \\ x=y \liff x+z=y+z \\ \foll x \foll y \foll z [x=y \liff x+z=y+z] } & \tcol{ \tt{P}[x,y] \fl {=}\tt{R} \fl 1,2\ {=}\tt{S} \fl 1,3\ {\lif}\tt{I} \fl \tt{P}[x,y,z] \fl {=}\tt{R} \fl 5,6\ {=}\tt{S} \fl [a]\ \follE[x/x,z/(-z),y/z] \fl [a]\ \follE[z/(-z),y/z,x/y] \fl 7,8\ {=}\tt{S} \fl 9,10\ {=}\tt{S} \fl [b]\ \follE[x/z] \fl 11,12\ {=}\tt{S} \fl [c]\ \follE \fl [c]\ \follE[x/y] \fl 13,14,15\ {=}\tt{S} \fl 5,16\ {\lif}\tt{I} \fl 4,17\ {\liff}\tt{I} \fl 18\ \follI \fl } } $$

Pedantic note: Notice the order in which we $\follE$ line $9$. If we tried specifying $x/y$ first, $y$ would get caught by the quantifier inside at the axiom $[a]$. Same for $z$ if we tried specifying $y/z$ first. So, formally speaking, that order matters.

$\tt{Theorem [2]: }\foll x [x+0=0+x]$.
$\tt{Proof:}$

$$ \fitch{ \fcol{1:\fl 2:\fl 3:\fl 4:\fl 5:\fl 6:\fl 7:\fl 8:\fl 9:\fl 10:\fl 11:\fl 12:} & \scol{ \subcol{ x+0 \neq 0+x \\ \hline x+0 = x \\ x \neq 0+x \\ x = 0+x \liff x+(-x) = (0+x)+(-x) \\ x+(-x) \neq (0+x)+(-x) \\ (0+x)+(-x) = 0+(x+(-x)) \\ x+(-x) \neq 0+(x+(-x)) \\ x+(-x) = 0 \\ 0 \neq 0+0 \\ 0 = 0+0 } \endsub x+0 = 0+x \\ \foll x [x+0 = 0+x] \\ } & \tcol{ P[x] \fl [c]\ \follE \fl 1,2\ {=}\tt{S} \fl [1]\ \follE[x/x,y/(0+x),z/(-x)] \fl 3,4\ \tt{m.t.} \fl [a]\ \follE[x/0,y/x,z/(-x)] \fl 5,6\ {=}\tt{S} \fl [b]\ \follE \fl 7,8\ {=}\tt{S} \fl [c]\ \follE[x/0] \fl 1,9,10\ \tt{r.a.} \fl 11\ \follI } } $$

And to wrap it up, an argument using Existential Quantifiers. Pay special attention on how the previous tip of "at the start $\exE$, only then $\follE$" is used in here (it is used twice, actually! In lines 4-6 and in lines 9-10):

None of Ockham's followers like any realist. All of Ockham's followers likes at least one of Hobbes' followers. Moreover, Ockham does have followers. Therefore, some of Hobbes' followers are not realists.

$$ \fitch{ \fcol{1:\fl 2:\fl 3:\fl 4:\fl 5:\fl 6:\fl 7:\fl 8:\fl 9:\fl 10:\fl 11:\fl 12:\fl 13:\fl 14:\fl 15:\fl} & \scol{ \foll x [O(x) \lif \foll y [R(y) \lif \lnot L(x,y)]] \\ \foll x [O(x) \lif \exi y [H(y) \land L(x,y)]] \\ \exi x[O(x)] \\ O(x_\alpha) \\ O(x_\alpha) \lif \exi y [H(y) \land L(x_\alpha,y)] \\ O(x_\alpha) \lif \foll y [R(y) \lif \lnot L(x_\alpha,y)] \\ \exi y [H(y) \land L(x_\alpha,y)] \\ \foll y [R(y) \lif \lnot L(x_\alpha,y)] \\ H(y_\alpha) \land L(x_\alpha,y_\alpha) \\ R(y_\alpha) \lif \lnot L(x_\alpha,y_\alpha) \\ L(x_\alpha,y_\alpha) \\ \lnot R(y_\alpha) \\ H(y_\alpha) \\ H(y_\alpha) \land \lnot R(y_\alpha) \\ \exi y[H(y) \land \lnot R(y)] \\ } & \tcol{ P \fl P \fl P \fl 3\ \exE[x/x_\alpha] \fl 2\ \follE[x/x_\alpha] \fl 1\ \follE[x/x_\alpha] \fl 4,5\ {\lif}\tt{E} \fl 4,6\ {\lif}\tt{E} \fl 7\ \exE[y/y_\alpha] \fl 8\ \follE[y/y_\alpha] \fl 9\ {\land}\tt{E} \fl 10,11\ \tt{m.t.} \fl 10\ {\land}\tt{E} \fl 12,13\ {\land}\tt{I} \fl 14\ \exI[y_\alpha/y] } } $$

Some preliminary comments.

First: the formal expressions of the rules and their provisos may slightly differ according to the proof system: Natural Deduction, Hilbert-style, etc. Thus, it is a good practice to refer to a consistent set of rules.

Second: every proof system must be sound, i.e. it must allow us to derive only true conclusion from true premises.

Thus, for example, every proof system must avoid the following fallacy:

"Plato is a Philosopher; therefore everything is a Philosopher".

The usual proviso regarding Universal Generalization is exactly designed to avoid it.

This proviso is present also in the Natural Deduction version of the rule.

But we have to consider that the "standard" version of Natural Deduction does not have a rule like "Existential Specification": "from $\exists x Px$, derive $Pc$, for a new constant $c$".

Why so ?

Exactly in order to avoid the fallacy you have rediscovered:

"There is an Even number." Let $3$ a new name for it. Thus, from the premise above, using ES: "$3$ is Even". Now "generalize" it with UG to conclude with: "Every number is Even".

As you can see the Natural Deduction for Existential Elimination is more complicated.

Also Hilbert-style proof system, where we have the Generalization rule, cannot have Existential Specification.

Assume it; then we have (by Deduction th): $∃xPx → Pc$, and also: $∃x¬Px → ¬ Pc$.

By contraposition: $¬¬Pc → ¬∃x¬Px$ that (in classical logic) amounts to the invalid: $Pc → ∀xPx$.

You can see e.g. P.Suppes, Introduction to Logic (1957) for a detailed discussion of quantifiers rules and related restrictions.

See page 90 for the fallacy we are discussing, and see page 91 for additional restriction on UG necessary to avoid that fallacy when the system has ES.