How to Use Generalization Axiom in Predicate Logic

Question

The Axiom says that if we have B it proves that we have $∀x B$, provided that x is not free in B.

Given that, if we have $B(x)$ we can say that we have $∀x B(x)$.

But if we have something like $B(c)$ with c a constant, can we say that we have $∀x B(c)$ by using Generalization Axiom ?

For me yes because if we have a constant then we have this constant for all x ...

But I want to clear my mind.

Answer 1

The Universal Generalization rule states that $\vdash \ P(x)$ has been derived, then $\vdash \!\forall x\,P(x)$.

More generally, if $\Gamma$ is a set of formulas and we have $\Gamma \vdash \varphi (y)$ has been derived, then $\Gamma \vdash \forall x\,\varphi (x)$ can be derived, provided that $y$ is not free in $\Gamma$.

In this context, a constant $b$ acts as a variable. Thus:

if $\Gamma \vdash \varphi (b)$ has been derived, then $\Gamma \vdash \forall x\,\varphi (x)$ can be derived, provided that $b$ does not occur in $\Gamma$.

Regarding the syntax of predicate logic, usually we can have "void" quantifiers, i.e. a quantifier like e.g. $\forall x$ that acts on a formula $\varphi$ where $x$ does not occur free.

In this case, the quantifier simply does not change the meaning (and truth value) of the formula.

Example: we can prove $0=0$ and thus, by UG, we can prove $\forall x (0=0)$; but this second formula is exactly like the first one.