# How to construct formal proofs using the natural deduction

So I'm currently studying First Order Logic, and I'm really struggling with constructing formal proofs. Can you guys maybe explain to me how to solve this problem:

Using the natural deduction rules, give a formal proof of:
P → S from the premises:

1. P → (Q ∨ R)
2. Q → S
3. R → S

Thank you so much for the help. I really appreciate your time!

## migrated from mathematica.stackexchange.comMar 24 '16 at 0:08

This question came from our site for users of Wolfram Mathematica.

• This is a forum for the discussion of the software Mathematica. But, you should try proof by contradiction. Assume not(S). Then, both not(Q) and not(R). Therefore, not(P). – evanb Mar 23 '16 at 21:02

It really depends of the style system you are expected to use, but this proof is basically:

• 1) make an assumption to eliminate an implication,
• 2) use a proof by cases, and
• 3) discharge the assumption to arrive at the required conclusion.

One format for a natural deduction proof is like so:

$$\begin{array}{l:ll} 1 & P\to (Q\vee R) & \textsf{Premise 1} \\ 2 & Q\to S & \textsf{Premise 2} \\ 3 & R\to S & \textsf{Premise 3} \\ \hdashline 4 & \quad P & \textsf{Assumption} \\ 5 & \quad Q\vee R & 1,4,\textsf{Implication Elimination (Modus Ponens)} \\ \hdashline 5a.1 & \qquad Q & 5, \textsf{Disjunction Case 1} \\ 5a.2 & \qquad S & 2,5a.1,\textsf{Implication Elimination (Modus Ponens)} \\ \hdashline 5b.1 & \qquad R & 5, \textsf{Disjunction Case 2} \\ 5b.2 & \qquad S & 3,5b.1, \textsf{Implication Elimination (Modus Ponens)} \\ \hline 6 & \quad S & 5a.2,5b.2, \textsf{Disjunction Case Elimination} \\ \hline 7 & P\to S & 4,6, \textsf{Implication Introduction} &{\Large\Box} \end{array}$$

Note how I've indented whenever an assumption is made, and outdented when it is discharged.   This ensures that your proof contains no undischarged assumptions, and is a visual aide to prevent you from calling on statements out side of their scope.   Other formats have similar prompts.

( In second order logic, the same procedure will be used for quantifier elimination and introduction; also called instantiation and generalisation.   Don't worry about that for now; but the tools you master now will be of use later. )

It is also often permissible to summarise the Disjunction Elimination (proof by cases) sub-proof when it is that basic.

$$\begin{array}{l:ll} 1 & P\to (Q\vee R) & \textsf{Premise 1} \\ 2 & Q\to S & \textsf{Premise 2} \\ 3 & R\to S & \textsf{Premise 3} \\ \hdashline 4 & \quad P & \textsf{Assumption} \\ 5 & \quad Q\vee R & 1,4,\textsf{Implication Elimination (Modus Ponens)} \\ 6 & \quad S & 2,3,5, \textsf{Disjunction Elimination} \\ \hline 11 & P\to S & 4,10, \textsf{Implication Introduction} &{\Large\Box} \end{array}$$

And, of course, you are usually also given abbreviations for the allowed justification steps (your rules of inference).   Usually something such as $\to-$ or $\to\textsf{E}$ for "Implication Elimination", and the like.   (Also MP, MT for modus ponens, modus tollens etc. )

• Thank you so much for the help! – Henry Jooste Mar 24 '16 at 5:43