Show that $∀x∃yRxy ⊢ ∃zRf(a)z$

Question

I'm very logic noob.

I'm having trouble deciphering what this means.

What I've got is "For all $x$, there exists some $y$ such that $x$ Respects (R) $y$ ~something~ there exists some $z$ such that $f(a)$ Respects (R) $z$"

I know that ⊢ means that $B$ is provable from $A$ but I'm not even sure what $A$ and $B$ are in this case.

Help.

Answer 1

Obviously, we have to assume that the constant symbol $a$ and the function symbol $f$ are part of the language.

This means that $f(a)$ is a term.

Thus, it is enough to apply Universal Instantiation rule (aka $(\forall \text E)$ ) : $\forall x \varphi \vdash \varphi [x/t]$, with term $f(a)$ as $t$, to get from $∀x∃y \ R(x,y)$ the conclusion :

$∃y \ R(f(a),y)$.

The change of bound variable is straightforward.

Answer 2

It's worthwhile to point out that the solution has nothing to do with function domain and codomain as you expressed confusions in your last comment, which means you still haven't completely understood the problem. By the way completeness is a very demanded quality in logic before compactness (completeness theorem, incompleteness theorems, etc). As a side inspirational note from philosophy, completeness in ancient Sanskrit and Pali is called Pāramitā, which also means perfection and many ancient philosophical and religious classics' titles end in Pāramitā or Prajñāpāramitā.

You worried about domain/codomain because you were only aware at the usual set-theoretic semantic level regarding the definitions of functions, relations, etc. But for this problem as the previous answer rightly pointed out, f(a) is just a first order logic (FOL) concept called constant term (of course f itself is another FOL concept called function symbol) to intentionally conflate you with set-theoretic function. Since the question asked already presented f(a) meaning it actually exists and you never need to doubt its soundness, and all later derivation are only syntactic entailment (⊢). Finally via semantic meaning from set theory, any function can be changed to an equivalent relation (not vice versa). So your claim in your last comment is incorrect, R is a binary relation symbol in FOL which we can only talk about it's satisfied or not by evaluation of its two arguments, it doesn't make sense to talk about its domain/codomain. A relation can always be mentally treated as a default function at the set theory meta-level (though not a valid concept at the FOL logic level) assuming its codomain is some truth object ranging only 2 distinct values such as the usual bits {0, 1}, but be careful truth value in such codomain is not normal grounded object in the official domain of discourse within FOL (thus cannot be quantified and hardly useful). Only in higher order logics you're allowed to ground predicate relations directly and range over a family of possible relations so that we can express something like if two objects share two such and such properties then they are the same object.

Hope this can completely dissolve your unanswered lingering confusion...