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.


2 Answers 2



"$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.

  • $\begingroup$ Could you suggest on how to find inference in this case? Since expression for "Horses' tails are tails of animals" seems to be difficult compared to "Horses are animals"? $\endgroup$
    – rentbuyer
    Sep 26, 2020 at 3:53
  • $\begingroup$ And also, I do not think "$x$ is a $P$'s tail" is a conjunction of two statements. It seems to be conditional statement, where $\forall(y)$($H(y)$ $\Rightarrow$ IsTailOf$(x,y)$) looks pretty logical in this sense. $\endgroup$
    – rentbuyer
    Sep 26, 2020 at 4:26
  • $\begingroup$ I am also suspicious on how you will construct tail-bearers y, since it does not seem obvious with which premises you will do that. $\endgroup$
    – rentbuyer
    Sep 26, 2020 at 4:44
  • $\begingroup$ @rentbuyer - No, what the answer correctly suggests is that "Horses' tails are tails of animals" can be formalized as $\forall x \forall y ((H(y) \land T(x,y)) \to A(y))$ or more precisely, $\forall x \forall y ((H(y) \land T(x,y)) \to (A(y) \land T(x,y)))$. $\endgroup$ Sep 26, 2020 at 4:53
  • $\begingroup$ @Taroccoesbrocco Yeah, second option seems much clear why it is true. So, basically, is it good idea to mention $\forall(x)\forall(y)((H(y) \wedge T(x,y)) \Rightarrow A(y))$ instead of $\forall(x)\forall(y)((H(y) \wedge T(x,y)) \Rightarrow (A(y) \wedge T(x,y)))$ (which is much obvious to a reader)? By the way, how can you prove that those $2$ expressions are indeed logically equivalent (Truth Table?)? $\endgroup$
    – rentbuyer
    Sep 26, 2020 at 5:04

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} $$

  • $\begingroup$ Thank you very much for your detailed solution. I just would like to ask you about [ ... ]* notation. Since I am beginner in natural deduction and we mostly use vertical proof for inferences during lectures, my question is only about elaborating on the meaning of [ ... ]* notation: where do you regularly use it, and is it same as sigma (set of assumptions) in "logic" literature? $\endgroup$
    – rentbuyer
    Sep 26, 2020 at 8:42
  • $\begingroup$ @rentbuyer - Natural deduction has many equivalent presentation. I guess when you say "vertical presentation", you refer to Fitch-style presentation of natural deduction. But to be sure (and so to answer precisely the question in your comment), I would like to see an example of a proof in natural deduction with the rule $\to_\text{intro}$ in the formalism you're using. Can you edit your question in order to add this example (as an image if it's too difficult to type it)? $\endgroup$ Sep 26, 2020 at 18:41
  • $\begingroup$ @rentbuyer - Anyway, $[B]^*$ means that we are "temporary" assuming $B$ (in Fitch-style, this is usually represented by shifting the formula to the right) and then we discharge this assumption in the inference rules marked by $*$, so that below the rule $*$ the formula occurrence $B$ is not an assumption any more. Inference rules that requires this discharging mechanism are $\to_\text{intro}$, $\lor_\text{elim}$, $\exists_\text{elim}$. In my example, the temporary assumption $H(y) \land T(x,y)$ (used twice) is discharged by the only instance of the rule $\to_\text{intro}$. $\endgroup$ Sep 26, 2020 at 19:13
  • $\begingroup$ @rentbuyer - The intuitive idea for the inference rule $\to_\text{intro}$ is that, in order to prove $A \to B$, we temporary assume $A$ and we show using other inference rules that $B$ follows from $A$. Hence, we discharge the temporary assumption $A$ (which is not an assumption any more) and we conclude by the rule $\to_\text{intro}$ that $A \to B$ holds. $\endgroup$ Sep 26, 2020 at 19:22

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .