Not sure if correct answers for substitution and "free for"

Question

My first question is: What is the result of the following substitution?

$[y/x](Bx \wedge \exists y Rxy)$

I would say that there is no result. Or should I say the result is $Bx \wedge \exists y Rxy$?

My second question is:

The question that's being asked: Is $f(x, y)$ free for $y$ in $Bx \wedge \exists y Rxy$?

The only $y$ in this formula is bound. Can you then also say that $f(x, y)$ free for $y$?

Edit per request: "Free for" (vrij voor in Dutch) basically means that you can replace a variable in a formula with a term. But it has to adhere to certain rules, one of which is that you cannot replace a variable in a formula that is bound by a quantifier.

Answer 1

I think that we have different "flavors" according to the textbooks.

See George Tourlakis, Mathematical Logic (2008), page 132 :

The definition of $A[x := t]$ [i.e.the substitution into formula $A$ of term $t$ in place of variable $x$] says that we are to replace every free occurrence of $x$ in $A$ by $t$, but if for some $y$ that occurs in $t$ — free, of course — there is a subformula $(\forall y)B$ [or $(\exists y)B$] of $A$ where $x$ occurs free, then we abort the operation and declare $A[x := t]$ undefined.

Thus, according to the following "convention", we have no result with $(Bx∧∃yRxy)[x := y]$, because there is the subformula $\exists yRxy$ with the quabtifier $\exists y$ and we do not want that it "captures" the new term $y$.

We may check on other textbooks; see Dirk van Dalen, Logic and Structure (5th ed - 2013), page 61 :

$(∀yϕ)[t/x]$ is $∀yϕ$ if $x = y$ (the "equal" is in the metalanguage).

This amount to say that the substitution is not performed.

In both cases, we have that the "operation" of substitution is not permitted; thus the original formula stay unchanged.

Regarding the second question, in van Dalen [page 62] we have that :

Definition 3.3.12 $t$ is free for $x$ in $ϕ$ if [...]

(iii) $ϕ := ∃yψ$ (or $ϕ := ∀yψ$) and if $x ∈ FV(ϕ)$, then $y \notin FV(t)$ and $t$ is free for $x$ in $ψ$.

In your example, the term $t$ is $f(x,y)$ and we want to know if it is free for $y$ in $ϕ$, where $ϕ$ is (simplifying a little bit) $∃yRxy$.

The answer is NO, because $y \notin FV(ϕ)$.

Note. The same rule is used by Herbert Enderton, A Mathematical Introduction to Logic (2nd - 2001), page 113, where the locution used : "the term $t$ is not substitutable for $x$ in $\varphi$", is intended explicitly to prevent wrong substitutions.