# Using formal proof to determine if two translations are equivalent or not

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!

• What proof system are you using? (Rules of inference, axioms, display format, etc.) – Graham Kemp Jun 27 '18 at 15:23
• Are you given a set of equivalence principles, like De Morgan? – Bram28 Jun 27 '18 at 15:28
• 1st step) use the equivalence of $\forall$ with $\lnot \exists \lnot$. – Mauro ALLEGRANZA Jun 27 '18 at 15:33
• 2nd step) use the propositional equivalence of $\lnot (p \to q)$ with $(p \land \lnot q)$. – Mauro ALLEGRANZA Jun 27 '18 at 15:34
• @jzaza: You need to show what the rules in your inference system are (not just recite the names your book is using for them). – Henning Makholm Jun 28 '18 at 1:05

## 2 Answers

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)~~$$

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)$.