If $\Sigma \vdash \varphi$ then $\Sigma \vdash \forall x \varphi$. Why when $(\varphi \implies \forall x \varphi)$ is not true?

Question

In the book of first order logic I'm reading they say that if $(\varphi_1,...,\varphi_n)$ is a proof from a set of formulae $\Sigma$, then so is $(\varphi_1,...,\varphi_n,\forall x \varphi_j)$ for all $1\leq j \leq n$. They assume that as an axiom but it doesn't make sense to me. Why if $\varphi$ is true then so is $\forall x \varphi$? For example if $\varphi$ is $x=1$ that wouldn't mean that $\forall x : x=1$ , or would it?

Maybe what I don't understand is: why $(\Sigma \vdash \varphi \implies \Sigma \vdash \forall x \varphi)$ is true but $(\varphi \implies \forall x \varphi)$ is not true?

The book is this: https://www.springer.com/cda/content/document/cda_downloaddocument/9781447121756-c2.pdf?SGWID=0-0-45-1192238-p174141200

Answer 1

Edit: It turns out that the system you're dealing with is very different from the systems I'm familiar with. Hence more or less everything below is wrong, with regard to that system. I'd simply delete the whole thing but I can't since it's "accepted"...

The reason your version makes no sense is it's false. You're leaving out a crucial hypothesis; what's true, and what it had better say in the book, is this:

If $\Sigma\vdash\phi$, where $x$ does not occur free in $\Sigma$, then $\Sigma\vdash\forall x\phi$.

That makes much more sense. Informally, saying $x$ does not occur free in $\Sigma$ means that the formulas in $\Sigma$ do not say anything about $x$. So saying $\Sigma\vdash \phi$ where $x$ does not occur free in $\Sigma$ means "you can prove $\phi$ without assuming anything about $x$".

Now it makes sense. If you can prove $\phi$ from a set of assumptions that don't mention $x$, then $\phi$ follows from your assumptions regardless of what $x$ is, so $\forall x\phi$ "should" also follow from the same assumptions.

Taking $\phi$ to be $x=1$ is a bad example, because it's hard to imagine a system where you can prove $x=1$ without assuming anything about $x$. Instead imagine you have some axioms describing how the real numbers work, and you want to prove $\forall x(x>1\to x^2>1)$. If you can prove $x>1\to x^2>1$ without assuming anything special about $x$ then $\forall x(x>1\to x^2>1)$ follows. (That is how people prove $\forall x\phi$ in actual math: prove $\phi$ without assuming anything about $x$.)

Hmm. An example of a $\Sigma$ where $\Sigma\vdash x=1$ but $x$ is not free in $\Sigma$ would be $\Sigma=\{\forall y (y=1)\}$. Yes, $\forall y (y=1)$ implies $x=1$, and it also implies $\forall x (x=1)$.

Another example, illustrating how if $x$ does occur free in $\Sigma$ then all bets are off: It's true that $x=1\vdash x=1$. But $x=1\not\vdash \forall x(x=1)$. If you leave out that "where $x$ does not occur free in $\Sigma$" then you're going to conclude that in fact $x=1\vdash\forall x(x=1)$, which is nonsense; luckily $x=1\vdash\forall x(x=1)$ does not follow from the correct version of the result we're talking about.

Answer 2

A proof of $\varphi$, with $x$ as a free variable, treats $x$ as an arbitrary element of its domain of discourse. This is exactly how we obtain a proof of $\forall x ~ \varphi$—introduce a variable $x$ and, knowing only those properties of $x$ that hold of all elements in its domain of discourse, prove $\varphi$. This is essentially the content of the $\forall$-introduction rule (a.k.a. universal generalisation).

If you could prove $x=1$ knowing nothing about $x$ than that it is an element of its domain of discourse, then it would indeed be true that $\forall x (x = 1)$ is true. But of course this is only going to be true if the domain of discourse of $x$ is $\{ 1 \}$. (Or $\varnothing$, I suppose.)

Now if you're doing first-order logic, it's likely that your domain of discourse is some ambient set theoretic universe, in which case $x=1$ will almost certainly not be provable, but formulae like $\varnothing \subseteq x$ and $x \in \{ x \}$ are provable.