How to formalize and prove a reasoning as propositional logic?

Question

If both E and H are at a lecture, then A won't be there. If E is at the lecture, then H will also be there. If A is not at the lecture, then E will be there. Thus, either E but not A is at the lecture, or A but not E is at the lecture.

Formalize the reasoning as a propositional logic sequent and prove the sequent using natural deduction.

My take on it

$1. E ∧ H ∧ ¬A$

$2. E \to H $

$3. ¬A \to E$

$4. (E ∧ ¬A) ∨ (¬E ∧ A)$

Then I did

$$ E ∧ H ∧ ¬A, E \to H, ¬A \to E ⊢ E ∧ ¬A$$

Then

$ 1.....E \to H...........$premise

$ 2.....¬A \to E..........$premise

$ 3.....E ∧ H ∧ ¬A........$premise

$ 4........H.............∧_{e_1} 3$

$ 5.......¬A.............∧_{e_2} 3$

$ 6........E.............\to e_1 2,5$

$ 7........E ∧ ¬A ........V_{i} 5,6$

This feels wrong so did I even formalize it correctly, if yes did I actually prove anything?

Also I'm only allowed to use basic natural deduction rules such as elemination and introduction for disjunction, conjunction, implication and negation.

Answer 1

$ \begin{array}{ll} E: & E \text{ is at the lecture.} \\ H: & H \text{ is at the lecture.} \\ A: & A \text{ is at the lecture.} \\ \end{array} $

I offer a proof below using a few derived rules near the end in order to shorten it up...

$ \begin{array}{lllll} \{ 1 \} & 1. & E \wedge H \to \neg A & \text{premise} & \\ \{ 2 \} & 2. & E \to H & \text{premise} & \\ \{ 3 \} & 3. & \neg A \to E & \text{premise} & \\ \{ 4 \} & 4. & E \vee \neg A & \text{Assumption for Conditional Proof} & \\ \{ 5 \} & 5. & E & \text{Assumption} & \\ \{ 2,5 \} & 6. & H & \text{2,5 Modus Ponens} & \\ \{ 2,5 \} & 7. & E \wedge H & \text{5,6 Conjunction Introduction} & \\ \{ 1,2,5 \} & 8. & \neg A & \text{1,7 Modus Ponens} & \\ \{ 1,2,5 \} & 9. & E \wedge \neg A & \text{5,8 Conjunction Introduction} & \\ \{ 10 \} & 10. & \neg A & \text{Assumption} & \\ \{ 3,10 \} & 11. & E & \text{3,10 Modus Ponens} & \\ \{ 3,10 \} & 12. & E \wedge \neg A & \text{10,11 Conjunction Introduction} & \\ \{ 1,2,3,4 \} & 13. & E \wedge \neg A & \text{4,5,9,10,12 Disjunction Elimination} & \\ \{ 1,2,3 \} & 14. & (E \vee \neg A) \to (E \wedge \neg A) & \text{4,13 Conditional Proof} & \\ \{ 1,2,3 \} & 15. & \neg (E \vee \neg A) \vee (E \wedge \neg A) & \text{14 SI: Implication Rule} & \\ \{ 1,2,3 \} & 16. & (\neg E \wedge \neg\neg A) \vee (E \wedge \neg A) & \text{15 SI: DeMorgan's Law} & \\ \{ 1,2,3 \} & 17. & (\neg E \wedge A) \vee (E \wedge \neg A) & \text{16 Double Negation Elimination} & \square \\ \end{array} $

Answer 2

"If both $E$ and $H$ are at a lecture, then $A$ will not." We can translate this as $L(E) \land L(H) \rightarrow \neg L(A)$.

As for the others:

$L(E) \rightarrow L(H)$;

$\neg L(A) \rightarrow L(E)$.

We seek: $(L(E) \land \neg L(A)) \lor (L(A) \land \neg L(E))$.

We know: $L(A) \lor \neg L(A)$.

If $L(A)$, we know $\neg L(E)$, hence $L(A) \land \neg L(E)$, as $L(E) \rightarrow L(H)$, and $L(E) \land L(H) \rightarrow \neg L(A)$ (i.e., $L(E)$ would imply a contradiction).

If $\neg L(A)$, $L(E)$, hence $L(E) \land \neg L(A)$, as $\neg L(A) \rightarrow L(E)$.

Thus, you obtain your desired result.