Proving this sequent using only natural deduction

185 Views Asked by At

$ p \rightarrow q,s \rightarrow t \quad \vdash \quad (p \land s) \rightarrow (q \land t) $

We are not allowed to use truth tables, De-morgan's laws, or any other method except natural deduction. Laws allowed: Implication, And, Or, MT, PBC, Copy Rule, Negation, Double Negation, Contradictions.

Both introduction and elimination wherever applicable.

Here is a sample style we are supposed to use while writing the proof :

2: $ p \lor \neg p $ $\quad L.E.M. $

3: $ p $ $ \quad assumption $

4: $ q $ $\quad \rightarrow e \quad 1,3 $

5: $ \neg p \lor q $ $\quad \lor i_2 \quad 4 $

6: $ \neg p $ $\quad assumption $

2

There are 2 best solutions below

1
On

If you can use the deduction theorem you can assume $p\land s$ and from that follows $p$ and subsequently $q$. Also follows $s$ and subsequently $t$. And since you've proven both $q$ and $t$, $q\land t$ follows. Then you discharge the assumption resulting in the statement to be proved.

$$\begin{align} \tag{1}p\rightarrow q, s\rightarrow t, p\land s &\vdash p\land s&\text{ assumption} \\\tag{2}p\rightarrow q, s\rightarrow t, p\land s &\vdash p&\text{ CE(1)} \\\tag{3}p\rightarrow q, s\rightarrow t, p\land s &\vdash p\rightarrow q&\text{ assumption} \\\tag{4}p\rightarrow q, s\rightarrow t, p\land s &\vdash q&\text{ MP(2,3)} \\\tag{5}p\rightarrow q, s\rightarrow t, p\land s &\vdash s&\text{ CE(1)} \\\tag{6}p\rightarrow q, s\rightarrow t, p\land s &\vdash s\rightarrow t&\text{ assumption} \\\tag{7} p\rightarrow q, s\rightarrow t, p\land s &\vdash t&\text{ MP(5,6)} \\\tag{8} p\rightarrow q, s\rightarrow t, p\land s &\vdash s\land t&\text{ CI(5,7)} \\\tag{9}p\rightarrow q, s\rightarrow t &\vdash (p\land s) \rightarrow (s\land t)&\text{ DT(8)} \\ \end{align}$$

Where CE is conjuction elimination, MP is modus ponens, CI is conjuction introduction and DT is the deduction theorem. Assumption is of course using one of the assumptions to the left of the $\vdash$.

0
On
01. (p→q)∧(s→t)  premise
  02. p∧s          assumption
  03. (p→q)∧(s→t)  restate 01
  04. p            ∧elim 02
  05. p→q          ∧elim 03
  06. q            MP 04 05
  07. s            ∧elim 02
  08. s→t          ∧elim 03
  09. t            MP 07 08
  10. q∧t          ∧intro 06 09
11. (p∧s)→(q∧t)  →intro 02 10

Therefore, ((p→q)∧(s→t))⊢((p∧s)→(q∧t)).