Predicate Logic and Inference Assume that given three predicates are presented below:
$H(x)$: $x$ is a horse
$A(x)$: $x$ is an animal
$T(x,y)$: $x$ is a tail of $y$
Then, translate the following inference into an inference using predicate logic expressions and prove whether inference is valid or not (for instance, using natural deduction):
Horses are animals.

Horses' tails are tails of animals.
My thoughts: I am quite good at translating predicate logic expressions, but here I struggled to come up with formula for Horses' tails. My initial idea was to consider similar sentence such as "w is a tail of a horse" to form required inference, but it was not successful. Would be welcomed to hear your ideas about this task.
 A: Hints:
"$x$ is a $P$'s tail" means that $x$ is a tail of $y$ and $y$ is a $P$.
"Horses' tails are tails of animals" means that for all tails $x$ and tail-bearers $y$, the tail being a horse's tail implies the tail being an animal's tail (where for "being a $P$'s tail" insert the above definition).
With the appropriate formalization of this paraphrase, it is possible to find a formal proof of the inference.
A: As correctly suggested in lemontree's answer, "Horses' tails are tails of animals" can be formalized as $\forall x \forall y \big((H(y) \land T(x,y)) \to A(y) \big)$ or more precisely, $\forall x \forall y \big((H(y) \land T(x,y)) \to (A(y) \land T(x,y))\big)$.
Of course, the argument
$\frac{\text{Horses are animals}}{\text{Horses' tails are tails of animals}} \quad \text{i.e.} \quad \frac{\forall y (H(y) \to A(y))}{\forall x \forall y \big((H(y) \land T(x,y)) \to (A(y) \land T(x,y))\big)}$
is valid. First, I give you an informal proof of that.
We want to prove that $\forall x \forall y \big((H(y) \land T(x,y)) \to (A(y) \land T(x,y))\big)$, under the hypothesis $\forall y (H(y)  \to A(y) )$.
So, let us fix arbitrary individuals $x$ and $y$ and let us suppose that $H(y) \land T(x,y)$, we have to show that $A(y) \land T(x,y)$. Since by hypothesis $\forall y (H(y)  \to A(y) )$, hence $H(y) \to A(y)$ holds for the particular $y$ we have chosen. Moreover, we are supposing that $H(y) \land T(x,y)$ and in particular $H(y)$ holds. By modus ponens, from $H(y) \to A(y)$ and $H(y)$ it follows that $A(y)$. Also, since we are supposing that $H(y) \land T(x,y)$, in particular $T(x,y)$ holds. So, $A(y) \land T(x,y)$. Therefore, we have proved that, for arbitrary $x$ and $y$, if $H(y) \land T(x,y)$ then $A(y) \land T(x,y)$.
Thus, $\forall x \forall y \big((H(y) \land T(x,y)) \to (A(y) \land T(x,y))\big)$ holds, under the hypothesis $\forall y (H(y) \to A(y))$.
You can formalize this proof in natural deduction as follows:
$$
\dfrac
{\dfrac
 {\dfrac
  {\dfrac{\dfrac{\forall y (H(y) \to A(y))}{H(y) \to A(y)}\forall_\text{elim} \qquad \dfrac{[H(y) \land T(x,y)]^*}{H(y)}\land_\text{elim}\!\!\!\!\!\!\!\!\!\!\!}{A(y)}\to_\text{elim} \quad \dfrac{[H(y) \land T(x,y)]^*}{T(x,y)}\land_\text{elim}}
  {A(y) \land T(x,y)}\land_\text{intro}\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!
 }
 {(\!\!\!\!\!\!\!\!H(y) \land T(x,y)) \to (A(y) \land T(x,y))} \to_\text{intro}^*\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!
}
{\dfrac
 {\forall y \big((H(y) \land T(x,y)) \to (A(y) \land T(x,y))\big)} 
 {\forall x \forall y \big((H(y) \land T(x,y)) \to (A(y) \land T(x,y))\big)} \forall_\text{intro}
} \forall_\text{intro}
$$
