Is the wf $B \to \forall x B$ logically valid?

Question

So I wanted to know If $B \to \forall x B$ is logically valid. I found this Tree proof generator website where I can check If a wf is logically valid or if there is an counter-example. I putted in the wf , and it said that it is logically valid.

But , then I checked Introduction to Mathematical Logic by Elliot Mendelson , page 78 , exercise 2.32(a). Here is the exercise.

Assume that $B$ and $C$ are wfs and that $x$ is not free in $B$. Prove the following.
(a) $\vdash B \to \forall x B$

So I am suspecting that $ B \to \forall x B$ in general (without the condition that $x$ is not free in $B$) cannot be proven in a predicate calculus. So because "Gödel's completeness theorem" (page 91) , $ B \to \forall x B$ is not logically valid. At this point I am confused.

So , Is the wf $$ B \to \forall x B$$ logically valid ?(In the context of mendelson)

Answer 1

Further to the assurances in the comments that $B\rightarrow\forall x B$ is not generally valid, here's a formal derivation of the validity of $B\rightarrow\forall x B$ in the case where $x$ does not occur free in $B.$

---

EDIT (following the comments)

Since $x$ does not occur free in $Ba,$ we could've simply inferred Line 8 directly from Line 1 using the rule $\forall I.$

Here's my full statement of the $\forall I$ inference rule:

• Let $B(\alpha/x)$ denote the result of replacing all free occurrences of variable $x$ in formula $B$ with arbitrary term $\alpha$; let $\alpha$ be freely substitutable for $x$ in $B$, and neither occur in $B$ nor occur free in any undischarged assumption.

  Then $B(\alpha/x)$ syntactically entails $\forall xB,$ i.e., $B\vdash\forall xB.$

  (Notice that during the inference, all occurrences of $\alpha$ are replaced by $x$).

Answer 2

Your suspicion is correct: If $x$ occurs free in $B$, the formula is invalid.

A formula is valid iff it is true for all interpretations and sequences. $B$ may hold of one object and not hold of another. Then the sequence which assigns $x$ to that object satisfies $B(x)$ but not $\forall x B(x)$, and thereby $B(x) \to \forall x B(x)$ is false under that sequence (and hence invalid):