How to prove with natural deduction?

223 Views Asked by At

Given this question, I tried solving in the first picture as you can see, but I didn't know how to continue and the second image is the right way to solve it. My question is have I done right so far? If you make an assumption about not q, do you also have to assume q ? Last but not least what is the point of using LEM in the second image at step 7?

enter image description here

enter image description here

2

There are 2 best solutions below

2
On BEST ANSWER

In formal systems such as propositional logic, there are certain statements known as theorems that can be proven from no premises at all; in other words, they can be shown to follow from the inference rules and/or axioms of the system alone. Consequently, you may introduce any of these theorems on any line of proof, as needed, a technique known as theorem introduction. The introduction of a theorem is not an assumption. Rather, it is a true statement that can be added to your set of premises whenever needed.

In the system of propositional logic that you're using, the law of the excluded middle (LEM), which states $\vdash p \vee \neg p$, is one such theorem. In the second proof above, LEM is introduced in order to infer $\neg p \vee q$ from the premise $p \to q$ via an inference rule known as disjunction elimination.

In short, disjunction elimination allows one to infer a statement by showing that it follows from every disjunct of a given disjunction. Here, the given disjunction is LEM. Beginning with the first disjunct $p$ on line $2$, the statement $\neg p \vee q$ is deduced on line $4$. Then, beginning with the second disjunct $\neg p$ on line $5$, the statement $\neg p \vee q$ is once again deduced on line $6$. Since $\neg p \vee q$ is deduced from every disjunct of $p \vee \neg p$, one may infer that $\neg p \vee q$ follows from $p \to q$.

As your own proof stands, it is incomplete. From the assumption $\neg q$ on line $2$, you deduce $\neg p \vee q$ on line $4$. Then, from the assumption $p$ on line $5$, you deduce $\neg p \vee q$ on line $7$. However, this is of litte value because you cannot introduce a disjunction such as $\neg q \vee p$ without proof. But... instead of assuming $p$ on line $5$, you could assume $q$ and deduce $\neg p \vee q$ via disjunction introduction. Then, after introducing $q \vee \neg q$ via LEM, you could finish the proof by inferring $\neg p \vee q$ via disjunction elimination. In other words, you could proceed with your own proof using LEM just as the second proof does, but instead of introducing $p \vee \neg p$, you use $q \vee \neg q$.

4
On

To be frank, that FIRST proof-attempt is pretty hopeless, and suggested that you need to get back to basics and read one or two good introductory presentations of natural deduction proofs.

The SECOND proof works, though in many proof systems LEM is not basic, so you'd need to build in a proof of that too.

There are some excellent introductions available, including the forallx version here: https://www.homepages.ucl.ac.uk/~uctytbu/forallxcam.pdf

Or try my now freely available book (originally CUP) downloadable at https://www.logicmatters.net/ifl/ One way of deriving the result you want from basic ND rules (without helping yourself to LEM) is at p. 207.

But start further back from the beginning of the chapters on natural deduction to get more hints about proof strategies.