Did I solve this correctly? (Natural deduction)

Question

Using the natural deduction method, how would you solve this:

Premises: $\{s, s → t\}.\quad$ Conclusion: $\{s ∧ t\}$

My proposed solution (mind you, I'm brand new at this):

$$\begin{align} s\rightarrow t &\qquad (\to \textrm{elim}) \\ t \\ s \\ s\wedge t &\qquad(\wedge\textrm{-intro}) \end{align}$$

Answer 1

$$ \begin{align} s\rightarrow t & &(1) \\ s & & (2) \\ t & \qquad Modus Ponens(1),(2) & (3)\\ \hline \therefore s \wedge t & \qquad Conjunction (2),(3) & (4) \end{align} $$

This is the format that my computer science course used.

Answer 2

While the subformulas you use in your proof are correct, the way you combined and wrote them down is not.

First of all, natural deduction proofs usually come with numbered lines, and the rule annotations on the right with a reference to the line numbers of the premises from which the conclusion was obtained. Assumptions which are not derived by rule applications are often annotated as such (e.g. $(\text{assumption})$. The order in which you write down your lines is important: Conclusions always have to appear after the premises from which they were derived.

($\to$ elim) requires two premises to derive the conclusion: When a formula $Q$ is derived using ($\to$ elim), there must be a premise of the form $P \to Q$ and a second premise of the form $P$, both of which have to appear on lines before the conclusion, which will be referenced next to the rule name:

$m_1. \quad P \to Q\\ \vdots\\ m_2. \quad P\\ \vdots\\ n. \quad Q \qquad (\to \text{elim}, m_1, m_2)$

So with $P = s$ and $Q = t$, the beginning of your proof goes like this:

$1. \quad s \to t \qquad (\text{assumption})\\ 2. \quad s \qquad (\text{assumption})\\ 3. \quad t \qquad (\to \text{elim}, 1, 2)$

The way in which you apply concjuntion introduction is correct, though you should again specify which premises you got the conclusion from - here, these are the formulas $s$ and $t$ on lines $2$ and $3$. With this, your final proof will look as follows:

$1. \quad s \to t \qquad (\text{assumption})\\ 2. \quad s \qquad (\text{assumption})\\ 3. \quad t \qquad (\to \text{elim}, 1, 2)\\ 4. \quad s \land t \qquad (\land \text{intro}, 2, 3)$

By the way: The Natural deduction proof editor and generator will help you check your natural proofs for correctness.