# Is this rule correct in sequent calculus?

In Ebbinghaus's book, the following rules occur in sequent calculus:

$$\dfrac{\Gamma \phi \dfrac{y}{x}}{\Gamma \forall x \phi}$$, if y is not free in $$\Gamma \forall x \phi$$

$$\dfrac{\Gamma \phi}{\Gamma \forall x \phi}$$, if x is not free in $$\Gamma$$

I want to know if the following rule is also correct and how to prove its correctness/incorrectness:

$$\dfrac{\Gamma \phi \dfrac{c}{x}}{\Gamma \forall x \phi}$$, if c does not occr in $$\Gamma \forall x \phi$$

See page 33: "In the sequel we restrict ourselves to formulas in which only the connectives $$\lnot$$ and $$\lor$$ and the quantifier $$∃$$ occur.

This is the reason why in Ch.IV A Sequent Calculus the rules for $$\forall$$ are not stated explicitly but are derived.

Having said that, the general form of the introduction rule for $$\forall$$ will be:

$$\dfrac{\Gamma \ \phi\dfrac{y}{x}}{\Gamma \ \forall x \phi}$$, if $$x$$ is not free in $$\Gamma$$.

There is a rule, called "Generalization on constant", that allows us to use also a constant $$c$$ in place of $$y$$, provided that $$c$$ is new (not occurring into $$\Gamma$$). See Enderton, page 123 (or van Dalen, page 95).

Comment: a variable is just an "unspecified" name. Thus, if we do not assume some special property involving it ($$x$$ is not free in $$\Gamma$$) we can replace it with a constant $$c$$ whatever, provided that $$c$$ is also "unspecified".

Otherwise we commit a fallacy, like deriving $$\forall x (x < 1)$$ from $$(0 <1)$$ in formal arithmetic. The reason is simple: in the proof of $$(0 < 1)$$ we need the arithmetical axioms. They are the $$\Gamma$$ of the derivation and the constant $$0$$ occurs in it.

• I wonder how we introduce $\phi \dfrac{y}{x}$ or $\phi \dfrac{c}{x}$ in our daily math. When using the Generalization rule, we say "let xx be a randomly selected (or any) yy, ...., we prove xx has the property of P, so for all zz of yy, zz has the property of P". Here, the only thing I'm clear is that zz is a constrained variable. What about xx? Is xx a free variable or a constant? I think "a randomly selected (or any)" is the same thing as "if xx is new or does not occur in $\Gamma$", right? Apr 17 at 13:31
• @William - not very clear... But yes, what is the role of a constant in a mathematical theory if we do not use it? Thus, in practice, if we have a constant (like $0$ and $\emptyset$) in a theory we have to use it into some axioms. Thus, in practice, the rules for universal quantifier introduction needs only variables. Then (as often with mathematician) we like to generalize in some way... Apr 17 at 13:37
• Compare the pair of rules of $\forall$ (the same for $\exists$): with the elimination rule (form $\forall x \phi$ derive $\phi [t/x]$) we may use a term whatever. Intution: if every number is greater-or-equal to $0$, also $0$ will be; vs the introduction rule. See above: from the fact that $0 < 1$ we cannot derive that every number is less than $1$. Apr 17 at 13:42
• Regarding the "randomly selected", the issue is: we choose a number whatever and we prove that a certain property $P$ holds of it; if in the proof we use somewhere the fact that $n$ is even, we cannot say that what we have proved is that $P$ holds for every natural number: maybe it holds olny for even ones. Apr 17 at 13:46