Use formal proof to determine if two translations are equivalent or not

Question

My logic professor just assigned our class this question that's got us all stumped. We'd appreciate your help.

We have found 2 translations for 'all logicians other than Aristotle are evil' namely $\forall x((Lx\land \lnot a=x)\to Ex)$ and $\lnot\exists x(Lx\land\lnot E x\land\lnot x=a)$. Use formal proof to determine whether these two translations are equivalent or not. That is, show the inference from one to the other is valid/invalid and vice versa. Give counterexample if invalid.

How would we go about doing this proof? Thanks, we appreciate your help!

Answer 1

the two translations are equivalent: $$1)~ (∀x)((Lx∧¬a=x)→Ex)~~~~~$$ $$2)~ ¬¬(∀x)((Lx∧¬a=x)→Ex)$$ $$3)~ ¬(∃x)¬((Lx∧¬a=x)→Ex)$$ $$4)~ ¬(∃x)¬(¬(Lx∧¬a=x)∨Ex)$$ $$5)~ ¬(∃x)((Lx∧¬a=x)∧¬Ex)~~$$

Answer 2

Hint [ref.to : Harry Gensler, Introduction to Logic (3rd ed., 2017)].

For the direction : $\lnot \exists x (\ldots) \to \forall x (\ldots)$.

1) $¬∃x(Lx∧¬Ex∧¬x=a)$ --- premise

2) $∀x ¬(Lx∧¬Ex∧¬x=a)$ --- from 1) by (RS) [page 246 : rules for exchanging quantifiers]

3) $¬∀x((Lx∧¬a=x)→Ex)$ --- [a] assumed the negation of the conclusion

4) $∃x ¬((Lx∧¬a=x)→Ex)$ --- from 3) by (RS)

5) $¬((Lb∧¬a=b)→Eb)$ --- from 4) by (DE) : Drop existential, with $b$ new

6) $(Lb∧¬a=b)$ and $¬Eb$ --- from 5) by (NIF) [page 196]

7) $¬((Lb ∧ ¬a=b) \land ¬Eb)$ --- assumed [b]

8) $(Lb ∧ ¬a=b)$ and $¬¬Eb$ --- from 7) by (NOT-BOTH)

Now we have a contradiction in 6) and 8); thus, by RAA, we can derive :

9) $((Lb ∧ ¬a=b) \land ¬Eb)$ --- closing the innere sub-proof from assumption [b]

10) $¬(Lb ∧ ¬Eb ∧ ¬b=a)$--- from 2) by DU :Drop universal [page 248], re-using $b$

Now we have a new contradiction in 9) and 10); thus, using RAA again, we can derive :

11) $∀x((Lx ∧ ¬a=x) → Ex)$--- closing the outer sub-proof from assumption [a].

---

Similar for the direction : $\forall x (\ldots) \to \lnot \exists x (\ldots)$.

Answer 3

The following is a proof presented in a Fitch-style proof checker. Since the "E" symbol is used to code the existential quantifier in the proof checker, I replaced "E" with "F". Also to make a well-formed formula from the second translation, I added parentheses.

There are three parts to showing that the two translations are equivalent:

1. Show $\forall x((Lx \land \lnot a=x) \to Fx) \to \lnot \exists x((Lx \land \lnot Fx) \land \lnot x=a) $.
2. Show $\lnot \exists x((Lx \land \lnot Fx) \land \lnot x=a) \to \forall x((Lx \land \lnot a=x) \to Fx)$.
3. Use biconditional introduction to derive the result from the first two parts.

Here is the first part:

One source of confusion may be how to commute the terms in the equality. Because the equality statement is negated I used an indirect proof to use equality introduction and elimination rules with non-negated statements.

At this point I could derive the result in part 1 above, but I will do that on the last line when I derive the biconditional.

The second and third parts come next:

Rather than attempting an indirect proof using the negation of the universal statement, I replaced $x$ with $b$ in the universal statement, used the equivalence $P \to Q \equiv \lnot P \lor Q$ to further transform the statement and then simplified it with De Morgan's laws. That resulted in line 21 in the proof checker. When I reached the contradiction on line 34 I still had additional work to do to derive the desired statement. That was done on line 44.

The third part took only one line. I used biconditional introduction on line 45 to complete the proof.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/