I am a beginner in Natural Deduction currently reading the book "Logic in Computer Science" and got stuck at proving: $$ P\land Q\to P\Leftrightarrow R\lor\lnot R$$

The latter formula is clearly a LEM, which I think $R$ should be obtained by getting a contradiction in the former formula. Any help will be much appreciated.

  • 1
    $\begingroup$ You cannot obtain a contradiction from $P ∧ Q → P$, because it is a tautology. $\endgroup$ – Mauro ALLEGRANZA Apr 9 '15 at 19:31

See :

(A) LEM is a $0$-premise rule in the system; thus, we have a $1$-line proof of :

$\vdash r \lor \lnot r$.

(B) $p \land q \to p$ is a tautology, thus it must be provable :

1) $p \land q$ --- assumed [a]

2) $p$ --- from 1) by $\land$-e

3) $\vdash p \land q \to p$ --- from 1) and 3) by $\to$-i, discharging [a].

Now, we can use the (obvious) property of the derivability relation : $\vdash \ $ [not present in the book; we can see it in : Dirk van Dalen, Logic and Structure (5th ed - 2013), page 37] :

if $\Gamma \vdash \varphi$, then $\Gamma \cup \Delta \vdash \varphi$,

to add to the above proofs the "unnecessary" premises, getting from (A) :

$p \land q \to p \vdash r \lor \lnot r$

and from (B) :

$r \lor \lnot r \vdash p \land q \to p$.

Now we can conclude with :

$p \land q \to p \dashv \vdash r \lor \lnot r$.

  • $\begingroup$ I am sorry I still don't quite get r∨¬r ⊢ p∧q→p I thought (B) just shows p∧q→p ⊢ p∧q→p ? $\endgroup$ – elly0t Apr 10 '15 at 19:37
  • $\begingroup$ @Elliot : NO; (B) shows $ ⊢ p∧q→p$ without assumptions, because it is a tautology, i.e. a "law of logic". $\endgroup$ – Mauro ALLEGRANZA Apr 11 '15 at 9:11

Try this: $$ p\wedge q\rightarrow p \leftrightarrow r \vee -r$$ $$ (-(p\wedge q)\vee p )\leftrightarrow V $$ If $ (-(p\wedge q)\vee p )$ is true or false, the result will be true or false respectivally, so $$ (-p \vee -q \vee p)$$ $$(-q \vee -p\vee p)$$ $$(-q \vee V)=V$$


Your Answer

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

Not the answer you're looking for? Browse other questions tagged or ask your own question.