Proving a sequent in natural deduction sequent style with elimination rules only

Question

Can we derive

$${p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} \neg \thinspace q \hspace{0.2cm} \vdash \hspace{0.2cm}\bot}$$

using $\textit{only}$ elimination rules, structural rules and cut, in an intuitionistic natural deduction in sequent-style calculus (in which the rules are expressed with sequents but there are intro- and elim-rules that act only on consequents)? The relevant elimination rules are:

$$\frac{\Gamma \Rightarrow A \rightarrow B \qquad \Delta \Rightarrow A}{\Gamma, \Delta \Rightarrow B}\hspace{0.1cm} \rightarrow Elim \hspace{0.1cm}$$ $$\frac{\Gamma \Rightarrow A \land B}{\Gamma \Rightarrow A}\hspace{0.1cm} \& Elim_1 \hspace{0.1cm}$$ $$\frac{\Gamma \Rightarrow A \land B}{\Gamma \Rightarrow B}\hspace{0.1cm} \& Elim_2 \hspace{0.1cm}$$ $$\frac{\Gamma \Rightarrow \bot}{\Gamma \Rightarrow A}\hspace{0.1cm} \bot Elim \hspace{0.1cm}$$

This is claimed possible (but not proven) in

• Grigori Mints and Shane Steinert-Threlkeld ADC method of proof search for intuitionistic propositional natural deduction (2016): page 396.

where a version of the natural deduction in sequent-style calculus is presented.

Edit: I have managed to get to $$\frac{\hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} (q \rightarrow \bot) \Rightarrow (p \land q) \rightarrow \bot \qquad p \land q \hspace{0.3cm} \Rightarrow \hspace{0.3cm} p \land q}{p \hspace{0.1cm} \& \hspace{0.1cm} q, \hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} (q \rightarrow \bot) \hspace{0.2cm} \Rightarrow \hspace{0.2cm}\bot}_{\rightarrow \hspace{0.2cm} Elim}$$ But can't prove $\hspace{0.2cm} p \hspace{0.01cm} \rightarrow \hspace{0.01cm} (q \rightarrow \bot) \Rightarrow (p \land q) \rightarrow \bot$

Answer 1

1) $p \land q \Rightarrow p \land q$ --- axiom

2) $p \land q \Rightarrow p $ - from 1) by $\land \text {Elim}_1$

3) $p \to \lnot q \Rightarrow p \to \lnot q$ --- axiom

4) $p \land q, p \to \lnot q \Rightarrow \lnot q$ --- from 2) and 3) by $\to \text {Elim}$

5) $p \land q, p \to \lnot q \Rightarrow q \to \bot$ --- from 4) rewriting $\lnot q$

6) $p \land q \Rightarrow q $ --- from 1) by $\land \text {Elim}_1$

7) $p \land q, p \to \lnot q \Rightarrow \bot$ --- from 5) and 6) by $\to \text {Elim}$.

---

Edit after OP's edit:

8) $p \to \lnot q \Rightarrow (p \land q) \to \bot$ --- from 7) by $\to \text {Intro}$.

---

---

Comment

In conclusion, we have proved the well-known:

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

in a normal form: first applying only elimination rules and then the introduction rules.