Beginner's statement translation to first order logic

Question

I'm beginning to learn predicate logic and I'm having a rough time figuring this one out.

I need to translate: Every planet except Earth is lifeless. Therefore, given any distinct two planets, at least one of them is lifeless. UD: planets, Lx= x is lifeless, e= earth

This is how I translated it so far: $$ ∀x (x ≠ e → Lx) \land ¬Le ∴ ∀x∀y ((Lx∨Ly) → (∃z(Lz \land (z = y ∨z = x) )\land (x≠y)))) $$

I understand that if the statement was just "at least one planet is lifeless" then it would be $ ∃zLz$. But then I also have to translate "given any distinct two planets".

What would the translation of the conclusion be? Thank you.

Answer 1

Every planet except Earth is lifeless.
Therefore, given any distinct two planets, at least one of them is lifeless.

$$ ∀x (x ≠ e → Lx) \land ¬Le\\ ∴ ∀x∀y ((Lx∨Ly) → (∃z(Lz \land (z = y ∨z = x) )\land (x≠y)))) $$

The first line is correct.

For the second line, will this do? $$\therefore∀x∀y\;\Big(x≠y→(Lx∨Ly)\Big).$$

Your suggestion, on the other hand, reads as "For every pair of planets such that at least one is lifeless, exactly one is lifeless."

Answer 2

I would interpret your translated conclusion as: "Given any two lifeless planets, at least one of them must be lifeless and they must not be the same planet." This is false for the case where $x = y = \textsf{Venus}$, since $\textsf{Venus}$ and $\textsf{Venus}$ are two lifeless planets but are the same planets.

I would translate the conclusion as: $$ \forall x \forall y ~ \Big( x \neq y ~~\to~~ Lx \lor Ly\Big) $$