Missing a logic argument

Question

I have to prove $$(w ⇒ s ∨ p) ∧ (t ⇒ ¬ s) ⇒ (s ⇒ ¬ q)$$

Is there a way to make it right?

Answer 1

The original steps shown in the proof are correct, but I think you're proving the wrong thing. The conclusion $t \land \lnot r \to q$ is provable given the premises. It also uses all the premises and is slightly more difficult to prove, so I think it's the intended problem.

---

Here's a proof of $t \land \lnot r \to q$

Your premises are equivalent to the following conditional tautologies

$$ \begin{align} \textbf{(I)} & & q \vdash s, p \;\; \text{is equivalent to $q \to s \lor p$} \\ \textbf{(II)} & & s, t \vdash \;\; \text{is equivalent to $s \to \lnot t$} \\ \textbf{(III)} & & t, p \vdash r \;\; \text{is equivalent to $t \land p \to r$} \end{align} $$

We can conclude via cut elimination from (I) and (II) that

$$ \begin{align} \textbf{(IIII)} & & q, t \vdash p \end{align} $$

We can use cut elimination again and conclude from (III) and (IIII) that

$$ \begin{align} \textbf{(V)} & & q, t \vdash r \end{align} $$

We can use the negation introduction rule twice

$$ t \vdash r, \lnot q $$ $$ t, \lnot r \vdash \lnot q $$

Note that this is equivalent to the desired conclusion, shown below

$$ \vdash t \land \lnot r \to \lnot q $$

---

Proof of $t \land \lnot p \to \lnot q$.

---

I'll use the nonstandard notion of a covariant and contravariant position below. A covariant position is a position like $\square$ in $A \to \square$ or $A \land \square$. Replacing a subexpression $\alpha$ by a subexpression $\beta$ where $\alpha \to \beta$ holds yields a valid conclusion if $\alpha$ is in a covariant position. By contrast, $\square$ is a contravariant position in $\lnot \square$ and $\square \to A$. In a contravariant position, $\beta$ can be replaced with $\alpha$ given that $\alpha \to \beta$ and the conclusion will be a valid inference.

This property is called upward and downward entailment in semantics, I don't know a good name for it in logic but it is a useful concept. Upward entailment is equivalent to what I'm calling a covariant position.

---

Given your hypotheses

$$ q \to s \lor p \;\;\text{and}\;\; s \to \lnot p \;\;\text{and}\;\; t \land p \to r $$

You can conclude the following by contrapositive, as you did

$$ \lnot(s \lor p) \to \lnot q $$

The De Morgan step is also correct

$$ (\lnot s \land \lnot p) \to \lnot q $$

However, given $s \to \lnot t$, the conclusion $ (\lnot\lnot t \land \lnot p) \to q $ does follow. The position $\square$ in $(\lnot \square \land \lnot p) \to \lnot q$ is a covariant position, so you can replace a subexpression appearing in $\square$ with one it implies. The double elimination step is also valid.

$$ (t \land \lnot p) \to \lnot q $$