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

This question is mainly about formality, not intuition.

There are some questions here (and a lot of answers) about Universal Generalization. Each of these states some rules that can be used to avoid fallacies in a First Order Logic argument.

1: This post says:

Assume $$\Gamma$$ is a set of formulas, $$\varphi$$ a formula, and $$\Gamma \vdash \varphi(y)$$ has been derived. The generalization rule states that $$\Gamma \vdash \forall x \varphi(x)$$ can be derived if $$y$$ is not mentioned in $$\Gamma$$ and $$x$$ does not occur in $$\varphi$$.

2: This other one says:

The following restrictions apply:

1. The term $$t$$ cannot occur in any undischarged assumption of the derivation of $$\phi[t/x]$$
2. The term $$t$$ cannot occur in $$\phi$$

3: An answer on the same question says:

1. $$t=0$$ --- assumption : is $$\phi[t/x]$$

2. $$\forall x \ (x =0)$$ --- from 1) by $$\forall$$I : wrong : $$t$$ is free in the one-line derivation of $$\phi[t/x]$$ , i.e. in $$t=0$$

4: One answer on this question says:

So, typically formalizations of the rule will say that $$a$$ needs to be a 'fresh' or 'new' constant: a constant that is not used elsewhere for a different purpose.
[...]
For Existential Elimination something similar happens. [...] In other words, once again you have to introduce a new constant.

From that, we can extract some rules that can be used (some of them are repeated, like "there can't be $$x$$ on the premise" and "there can't be $$x$$ anywhere before", in that case, we'll use the stronger version). For any substitution $$P(a)$$ to $$\forall x[P(x)]$$ (Universal Generalization) or $$\exists y[P(y)]$$ to $$P(b)$$ (Existential Instantiation):

1. $$a$$ can't have appeared in any undischarged assumptions/premises.
2. $$a$$ can't occur in $$P$$ after the substitution.
3. $$x$$ has to be a new variable.
4. $$b$$ has to be a new variable.

From this answer, it is clear that they are not meant to be used together:

Different systems define these rules a bit differently in terms of notation. For example, some systems simply drop quantifiers for the elimination rules, leaving what seems to be free variables in the formula, while others replace those variables with constant symbols. Either way, however, restrictions do indeed need to be in place that prevent you from making invalid inferences, as you already suspected.

A smaller combination of these seems to be usually regarded as enough, but for the sake of argument, let's use them all of them together. Now consider the following: \begin{align}\exists x[P(x)] & \quad \text{Premise} \\ P(a) & \quad \text{Existential Instantiation} \\ \forall y[P(y)] & \quad \text{Universal Generalization} \end{align}

It is clear that the above argument is a fallacy. If it works for one example, it doesn't mean it works for all of them. Still, all the rules were followed:

1. $$a$$ doesn't appear in the premise
2. $$a$$ doesn't occur after the substitution
3. $$y$$ is a new variable
4. $$a$$ is a new variable

Now of course, we can also add a new rule that states "If $$a$$ came from a Existential Instatiation, then it cannot be used in a Universal Generalization", but given that even following those 4 (quite strict) rules still resulted in a fallacy, what guarantees that there isn't some subtle example in which, even following those 5 rules, we'll still end up with a fallacy?

Almost all of these answers cite that "$$a$$ has to be arbitrary and not specific", or "we can't have previously assumed anything about $$a$$", but those are very informal and imprecise ways of stating how Universal Generalization can be safely used.

So, given that, my question is: What set of rules can one use, for which it is guaranteed that, given a statement $$P(x)$$, you can safely conclude that $$\forall x[P(x)]$$?

Edit: Though this question has been marked as a duplicate of Restrictions on the use of universal generalization, that question is asking how to understand these rules, and why they exist (also the case for this linked question), which is not the point of my question. It is clear to me how to use them (or so I hope, if I did not apply one of the rules properly, I'd be more than glad to be corrected). Also, it is clear why they exist, it's to avoid fallacies like the one presented above (namely, $$\exists x[P(x)] \Rightarrow P(a) \Rightarrow \forall y[P(y)]$$). Now, even though that is their purpose, they don't seem to be strong enough to always avoid a fallacy. Even on an argument in which all of them are followed, it still leads to a conclusion that clearly shouldn't follow from the premise. So my question remains: Since these don't seem to be enough, which set of rules can be used to always avoid a fallacious use of UG?

Edit: Changed question from only Universal Generalization to Universal/Existential Generalizations and Specifications, to reflect evolving answers regarding the other quantifier rules.

• Two comments: 1) the formal expressions of the rules and their proviso may slightly differ according to the proof system: Natural Deduction, Hilbert-style, etc. Thus, you have to refer to a consistent set of rules. With regards to UG, the proviso amounts to avoiding the following fallacy: "Plato is a Philosopher; therefore everything is a Philosopher". Oct 2 '20 at 6:22
• Oct 2 '20 at 6:40
• @MauroALLEGRANZA Still my doubt remains. I agree with your third comment that $\exists x[P(x)] \Rightarrow P(a) \Rightarrow \forall y[P(y)]$ should be incorrect, my point is that none of the rules cited on any of the questions linked impede that. Now, of course, one can put their intuitive finger on it and say "that argument seems very nonsensical", and they'd be right. Nonetheless, all of the rules are followed properly in it (or so I hope, more than glad to be corrected otherwise), but still, the argument is a fallacy. Oct 2 '20 at 12:35
• @MauroALLEGRANZA Responding to your comment on the proviso on Existential Elimination, the variable used on that argument is specifically chosen to be one in which $P$ applies, but still, there doesn't seem to be a formal rule impeding it to be used in UG. Now of course, using a value in which it applies, makes so it is "specific", not "arbitrary". But there doesn't seem to be any formality in the language used to indicate that, for all that the person on the laguage knows, a variable is a variable. Oct 2 '20 at 12:44
• @MauroALLEGRANZA Putting my second comment in a different way. If you were a person that didn't have a "logical intuition" and were merely following the rules of the system, for all that you know, that argument is perfectly valid. Another way to put it is: Even you do have a logical intuition, if someone hides the first line of the argument, you have no way to know if UG is applicable on the second line or not. So my doubts about these rules still remain. Oct 2 '20 at 12:48

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:

•  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.

•  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$$).

•  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}{\begin{array}{rlr}#1\end{array}} \nwcm{\fcol}{\begin{array}{r}#1\end{array}} %FirstColumn \nwcm{\scol}{\begin{array}{l}#1\end{array}} %SecondColumn \nwcm{\tcol}{\begin{array}{l}#1\end{array}} %ThirdColumn \nwcm{\subcol}{\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:

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

Here's an important note on rule . 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  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}& 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:

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

•  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 . In the right one $$a$$ is distinct, not arbitrary, so step $$3$$ breaks rule .

Two things to note on rule . 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 . As rule  resolves the problem of different non-arbitrary variables getting equated for $$\exI$$, this part of rule  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 , 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:

•  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}$$).

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

•  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  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:

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

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

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

•  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 ). 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.
•  New rule: All formulas on conclusions should have U-Closure.

 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 : }\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 : }\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 \ \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] } }$$

• Came here to understand how to avoid "There are bald people. Let's say, Bob. Then, everyone is bald", but got lost in your in-depth explanation. Could you, please, ELI5? Nov 9 '20 at 13:35
• @JorgeAmVF To avoid that specific fallacy, you only need to mark all variables that you ES on (in my case, I use a greek letter subscript, so $\exists x[P(x)]$ becomes $P(x_\alpha)$), and remember to not UG those marked variables. In my summarization, this appears as the ES rule "$a$ is a not yet used dependent variable" and the UG rule "$a$ is arbitrary". Nov 9 '20 at 22:30
• Very precise explanation. Thanks! Nov 11 '20 at 3:02

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.

• Thanks a lot for the recomendation man. I'm on the last chapter of the book you recommended, and it had exatcly what I was looking for, thanks a lot! Oct 29 '20 at 23:43
• Also, I've added an answer with an explanation of the rules present on the book, for those looking for the information, and since I imagine you are more knowlegable about that, feel free to criticize that answer as well if I got something wrong. Oct 29 '20 at 23:45
• @LuizMartins - you are welcome :-) Oct 30 '20 at 7:19

If you follow these guidelines, what you can safely do with universal generalizations should not be an issue. Here, I am assuming proofs are ordered lists of statements. No statement may refer to or depend on a subsequent statement.

It should be simple, but I found making universal generalizations perhaps the most difficult thing to master in formal logic. I came up with the following guidelines that I have used for several years now, and that can also be used in ordinary, informal proofs:

How to introduce free variables

Only introduce new free variables by means of a premise or existential specification. Though it is not usually done in mathematical proofs anyway, do not introduce new free variables by universal specification.

How to discharge a premise

When discharging a premise to obtain a conclusion, your conclusion should contain no free variables that were introduced in that premise or on subsequent lines. This may require first doing existential generalizations in the last statement to get rid of the free variables introduced by existential specifications in the interval. Then introduce $$\implies$$ or $$\neg$$ depending on whether a contradiction was obtained. Then do universal generalizations on any free variables that were introduced in that premise. This is the only time you should be doing universal generalizations.

When a premise is discharged, it, along with subsequent statements up to but not including the conclusion, will be deactivated so that other statements may not refer to or depend on them.

EXAMPLES

1. Conditional (direct) proof

Premise: $$~~P(x)~~~~~~~~~~~~~~~~~~~~~~~~~~$$ (introduces free variable $$x$$)

$$~~~~~~\vdots$$

Introduce free variable $$y$$ by existential specification

$$~~~~~~\vdots$$

Derive statement: $$~~Q(x,y)$$

Conclusion: $$~~\forall a: [P(a) \implies \exists b: Q(a,b)]~~~~~~$$ (no free variables $$x$$ or $$y$$)

Premise: $$~~P(x)~~~~~~~~~~~~~~~~~~~~~~~~~~$$ (introduces free variable $$x$$)
$$~~~~~~\vdots$$
Derive statement: $$~~Q \land \neg Q~~~~~~$$ or $$~~~~~~Q\iff \neg Q~~~~~~$$ (contradiction)
Conclusion: $$~~\forall a: \neg P(a)~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~$$ (no free variable $$x$$)
• I don't know that it "goes bad." It just isn't necessary and only makes this process much more complicated. You won't see it done in any proofs in algebra, analysis or number theory. If you make the domains of quantification explicit for each individual quantifier, as is implicitly done in these fields, there is no need to introduce free variables by Universal Specification. You just start with the premise, e.g. $x\in R$, and proceed from there. Oct 2 '20 at 23:20
• If you want to simulate standard FOL, you can explicitly introduce a premise for an non-empty domain of discourse, say the unary predicate $U$ with the premise, $\exists a: U(a)$, and for each universal quantifier you would have $\forall a: [U(a) \implies \cdots ]$, and for each existential quantifier $\exists a: [U(a) \land \cdots ]$. And for every free variable $x$ that you introduce in a premise, you would have to include $U(x)$ in that premise. This way, you can see behind the scenes of FOL and solve some otherwise tricky problems for the beginner. Oct 3 '20 at 1:50