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?

  • 1
    $\begingroup$ Shouldn't you start from $\forall z(\forall x(\exists y Lxy \to Lzx))$ ? $\endgroup$
    – Henry
    Dec 20, 2019 at 1:27
  • $\begingroup$ @Henry They are equivalent, we can also translate this as $\forall x,y,z(Lxy\to Lzx)$. $\endgroup$
    – Manx
    Dec 20, 2019 at 1:33
  • 2
    $\begingroup$ In a movie, I'm not sure but I think Julia Roberts was in it, a guy is wearing a T-shirt that says "I Love Everyone. You're Next." I can't find it. There is a recent horror movie called You're Next, that is all the search is giving $\endgroup$
    – Will Jagy
    Dec 20, 2019 at 1:39
  • $\begingroup$ I have the same confusion as @Henry. I don't see the equivalence between the proposition of Henry and your proposition 1. $\endgroup$
    – WhatsUp
    Dec 20, 2019 at 2:06
  • 2
    $\begingroup$ @WhatsUp Apply this $(R → ∀xQ(x))≡∀x(R → Q(x))$ on $(1)$, basicly we want to move $\forall y$ out, to avoid two scope of $y$ stack on each other, so we change $y$ to $z$. $\endgroup$
    – Manx
    Dec 20, 2019 at 2:21

2 Answers 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

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:

enter image description here

(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':

enter image description here

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':

enter image description here

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

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

With that:

enter image description here

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.