1
$\begingroup$

I am working on assignment for school where the task asks to give a deductive proof. However, I have never used this technique (nor that I am very good in proofs in general) thus it is quite complicated. Can anyone here give me a short "guide" on how to proof by deduction? (Couldn't find any good guide online). It would be really useful to see how to generate this kind of proofs if anyone could show how to solve this proof:

If $\forall x. (P(x) \to (Q(x) \wedge S(x)))$ and $\forall x. (P(x) \wedge R(x))$, then $\forall x. (R(x) \wedge S(x))$.

Thanks in advance!

$\endgroup$

migrated from cs.stackexchange.com May 12 '16 at 22:52

This question came from our site for students, researchers and practitioners of computer science.

  • 1
    $\begingroup$ Generally you need to show what you've tried, to get good reception on your homework question. $\endgroup$ – Insane May 12 '16 at 14:52
  • 1
    $\begingroup$ It's better to ask this question on math.se. Somebody will write a textbook for you. $\endgroup$ – Yuval Filmus May 12 '16 at 19:04
  • 2
    $\begingroup$ Thus, you will never get an answer unless you will not "specify" what rules/axioms to be used in a "proof by deduction" you are allowed to use. $\endgroup$ – Mauro ALLEGRANZA May 13 '16 at 9:47
  • 1
    $\begingroup$ Intuitively, the argument is quite simple: if all "objects" that are $P$s are also ($Q$ and $S$)s, by first premise, and all "objects" are ($P$ and $R$)s, by second premise, then necessarily all "objects" are ($P$ and $Q$ and $R$ and $S$)s and thus a fortiori they are ($R$ and $S$)s. $\endgroup$ – Mauro ALLEGRANZA May 13 '16 at 9:51
  • 1
    $\begingroup$ No it does not make sense to say we allow the use of all valid inference rules, because then any tautology can be proven in one step since it is a valid inference rule! In natural deduction, there are very few rules, but it can prove every tautology. Do you understand my answer? $\endgroup$ – user21820 Jun 3 '16 at 0:22
2
$\begingroup$

There are many styles of natural deduction, and the one most suited for practical use is Fitch-style, which uses indentation just like programming languages to denote scoping. Basically, you ensure that every sentence you write is true in its context, where the context is captured by headers exactly as in a multi-level list. We can even throw away the lines at the side. See here and here and here for some examples.

Here is what such a proof of your example will look like: $\def\imp{\rightarrow}$

If $\forall x \ ( P(x) \imp Q(x) \land S(x) ) \land \forall x \ ( P(x) \land R(x) )$:

  $\forall x \ ( P(x) \imp Q(x) \land S(x) )$.

  $\forall x \ ( P(x) \land R(x) )$.

  Given any $x$:

    $P(x) \imp Q(x) \land S(x)$.

    $P(x) \land R(x)$.

    $P(x)$.

    $R(x)$.

    $Q(x) \land S(x)$.

    $S(x)$.

    $R(x) \land S(x)$.

  $\forall x \ ( R(x) \land S(x) )$.

$\forall x \ ( P(x) \imp Q(x) \land S(x) ) \land \forall x \ ( P(x) \land R(x) ) \imp \forall x \ ( R(x) \land S(x) )$.

I'm confident you can figure out how each line follows from the preceding ones. That ultimately is the goal of natural deduction, to make the logical reasoning clear.

$\endgroup$
  • $\begingroup$ Of course, this may not be what your assignment is looking for but it's usually more instructive to understand proofs in natural deduction than in any other system. The worst is Hilbert systems, which are good for theoretical study of first-order logic systems but quite useless for practical usage. $\endgroup$ – user21820 May 17 '16 at 4:42
0
$\begingroup$

A proof in natural deduction style is done with things called proof-trees. I don't know how to draw them on SE, so I'll use the other alternative known as Hilbert-style proof.

1. ∀ x . P x ⇒ Q x ∧ S x     premise
2. ∀ x . P x ∧ R x            premise
3. ∀ x . R x ∧ S x            goal
   3.1 P x ⇒ Q x ∧ S x       using (1) on x
   3.2 P x ∧ R x              using (2) on x
   3.3 P x                    ∧-elimination1 on 3.2
   3.4 R x                    ∧-elimination2 on 3.2
   3.5 Q x ∧ S x              modus-ponens using 3.1 and 3.3
   3.6 S x                    ∧-elimination2 on 3.5
   3.6 R x ∧ S x              ∧-introduction using 3.4 and 3.6

Natural deduction is treated in the early chapters of this nifty book called: Using Z. Best of luck!

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy