2

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!

Community
  • 1
Henry Jooste
  • 123
  • 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

1 Answers1

3

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

Graham Kemp
  • 129,094