Everyone loves all lovers, Romeo loves Juliet $\vdash$ I love you (Natural deduction proof)

Question

Everyone loves all lovers.

Romeo loves Juliet.

$\therefore$ I love you. [Use $Lxy,r,j,i,u$]

Here is what i did:

Is this the best we can do, or are there shorter approaches?

Answer 1

It all depends on what rules you have in your system.

For example, the Fitch system I use allows you to instantiate multiple quantifiers at once, so representing the first premise as $\forall x \forall y \forall z (Lxy \to Lzx)$, it can do:

(the system regards $u$ as a variable, so I had to use $o$ for 'you')

Moreover, suppose we had in addition to that some rule that generalizes Modus Ponens so you can chain through any number of conditionals in $1$ step. Let's call it 'Chain':

Also, I know some books define a rule that combines Universal Elimination and Conditional Elimination. So, for example, with such a rule, you can go straight from $\forall x (P(x) \to Q(x))$ and $P(a)$ to $Q(a)$. Having such a rule makes a lot of sense, since universals so often come with conditionals. Moreover, let's suppose that this rule allows you to drop multiple universals at once. Let's call it 'Universal Conditional Elimination':

Then, there is of course my trusty 'Hokus Ponens', formally defined as:

\begin{array}{c} \cfrac{}{\varphi} \end{array}

With that:

Tada! ... Hey, you never said the rules in the proof system had to be sound!

Finally, since he argument is valid, one an always define an inference rule that matches the very argument. It would be completely ad hoc, but theoretically it's always possible Hence, every valid argument can, in theory, be proven by a single valid inference rule.

Answer 2

Yes, all the shortest proofs in natural deduction consist of 10 steps (included the 2 assumptions), because you have to apply 3 elimination rules for the quantifiers and 1 elimination rule for the implication, for 2 times.

For instance, if you translate the first assumption as $\forall x \forall y \forall z(Lxy \to Lzx)$ (which is logically equivalent to $\forall x (\exists y Lxy \to \forall y Lyx)$), the shortest proof in natural deduction is the following:

1. $\forall x \forall y \forall z(Lxy \to Lzx)$ assumption
2. $Lrj$ assumption
3. $ \forall y \forall z(Lry \to Lzr)$ $ \ \forall_E$ from 1
4. $ \forall z(Lrj \to Lzr)$ $\ \forall_E$ from 3
5. $Lrj \to Lur$ $\ \forall_E$ from 4
6. $Lur$ $\ \to_E$ from 5, 2
7. $ \forall y \forall z(Luy \to Lzu)$ $\ \forall_E$ from 1
8. $ \forall z(Lur \to Lzu)$ $\ \forall_E$ from 7
9. $Lur \to Liu$ $\ \forall_E$ from 8
10. $Liu$ $\ \to_E$ from 9, 6