# 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.

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.

• 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"? Sep 26, 2020 at 3:53
• 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. Sep 26, 2020 at 4:26
• 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. Sep 26, 2020 at 4:44
• @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)))$. Sep 26, 2020 at 4:53
• @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?)? 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}$$

• 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? Sep 26, 2020 at 8:42
• @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)? Sep 26, 2020 at 18:41
• @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}$. Sep 26, 2020 at 19:13
• @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. Sep 26, 2020 at 19:22