Propositional Logic: Natural Deduction using Elimination and Introduction rules

Question

So, we have to prove ⇁Y as conclusion from premises: A. (X ∨ Y) ⇒ (X ∧ Y) B. ⇁X

What I’ve tried so far is basically:

1. ⇁X [Premise]
2. ⇁X ∨ (X ∧ Y) [∨In, 1]
3. (X ∨ Y) ⇒ (X ∧ Y) [Premise]

.

.

.

n. X ∧ Y [⇒ Out]

(n+1). X [ ∧ Out, n]

(n+2). ⇁X [Reiteration from 1]

(n+3). Y [ ∧ Out, n]

(n + 4): Y ⇒ (X ∧ ⇁X)

(n + 5): ⇁ Y [⇁In from (n+4)]

To prove (n+4): We assume Y then reiterate X and ⇁X we obtained from (n+1) and 1. respectively. So, thus we deduced X and ⇁X from assumption Y thus using [⇒In] to prove (n+4):

Stuck at obtaining line n. For using ⇒Out we have lines 3.(of form A ⇒C), 2 (of form A ∨ B) We need just (of form B ⇒ C) i.e. ⇁X ⇒ (X ∧ Y) to complete the proof. So, using Introduction and Elimination rules for ∧, ∨, ⇒, ⇁, etc. and similar formal proof rules how do we derive ⇁X ⇒ (X ∧ Y) in context of above question and proof?

Answer 1

Derivation

$\begin{array}{} \{1\}&1.&\lnot X&\text{P}\\ \{2\}&2.&(X\lor Y)\to(X\land Y)&\text{P}\\ \{3\}&3.&Y&\text{A for RAA}\\ \{3\}&4.&X\lor Y&\text{3, $\lor$I}\\ \{2,3\}&5.&X\land Y&\text{2, 4, MP}\\ \{2,3\}&6.&X&\text{5, $\land$E}\\ \{1,2,3\}&7.&\bot&\text{1, 6, $\bot$I}\\ \{1,2\}&8.&\lnot Y&\text{3, 7, RAA}\\ \end{array}$