Natural Deduction - How to define literals?

Question

I'm currently working on the following question:

"At least one of Plato and Democritus believed in the theory of forms. Plato believed in the theory of forms only if he was not an atomist, and Democritus was an atomist only if he did not believe in the theory of forms. Democritus was an atomist. Prove, using Natural Deduction, that Plato was not an atomist"

I have been working for quite some time to take the information and turn it into a set of literals and statements I can work with.

So far, I have got $P \lor D$, $P \Rightarrow \lnot a$, $D \Rightarrow A$, $D = A$

However, I cannot seem to make these prove the statement using natural deduction, any hints?

Answer 1

Suppose we put

P: Plato believed in the theory of forms.

D: Democritus believed in the theory of forms.

A: Plato was an atomist.

B: Democritus was an atomist.

We don't need to expose any more structure (that Plato and Democritus feature in two premisses, that believing in the theory of forms features in two premisses, evidently doesn't matter for the validity of this argument, so needn't by captured in our symbolic representation). Then the argument can be regimented as

$(P \lor D), ((P \to \neg A)\ \land\ (B \to \neg D)), B \therefore \neg A$

(Note there are three premisses, the second one is conjunctive.)

---

The way a natural deduction argument goes will depend on your particular ND system -- for example, is disjunctive syllogism a basic rule? are you allowed to invoke it as a derived rule? how does your or-elimination rule work?

One line of argument goes: Consider cases. We either have P or D. The first case gives us $\neg A$. The second case is quickly leads to contradiction. Hence $\neg A$.

Or we could go from $B$ and the second conditional to $\neg D$, use disjunctive syllogism to get $P$, and then use the first conditional to get the desired conclusion.

Which is easier to formalise in your preferred ND system?