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?
$\begingroup$
$\endgroup$
7
-
1$\begingroup$ Shouldn't you start from $\forall z(\forall x(\exists y Lxy \to Lzx))$ ? $\endgroup$ – Henry Dec 20 '19 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 '19 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 '19 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 '19 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 '19 at 2:21
|
Show 2 more comments
$\begingroup$
$\endgroup$
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.
$\begingroup$
$\endgroup$
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:
- $\forall x \forall y \forall z(Lxy \to Lzx)$ assumption
- $Lrj$ assumption
- $ \forall y \forall z(Lry \to Lzr)$ $ \ \forall_E$ from 1
- $ \forall z(Lrj \to Lzr)$ $\ \forall_E$ from 3
- $Lrj \to Lur$ $\ \forall_E$ from 4
- $Lur$ $\ \to_E$ from 5, 2
- $ \forall y \forall z(Luy \to Lzu)$ $\ \forall_E$ from 1
- $ \forall z(Lur \to Lzu)$ $\ \forall_E$ from 7
- $Lur \to Liu$ $\ \forall_E$ from 8
- $Liu$ $\ \to_E$ from 9, 6
answered Dec 20 '19 at 2:05
