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

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$

  • $\begingroup$ Your $\to$Elim rule lacks a $\Delta$ somewhere in the conclusion. $\endgroup$ – hmakholm left over Monica Jun 16 '17 at 13:41
  • $\begingroup$ Thanks, I have edited it. $\endgroup$ – user65526 Jun 16 '17 at 13:42
  • $\begingroup$ Is $\neg A$ an abbreviation for $A\to \bot$ in your system? If so, I suggest you start by unfolding that in your goal. It should then be obvious that what you need to prove is a matter of two invocations of Modus Ponens. $\endgroup$ – hmakholm left over Monica Jun 16 '17 at 13:43
  • $\begingroup$ Now the question has changed... :-) 1) assume $p \to \lnot q$; 2) assume $p \land q$; 3) derive $p$ from 2); 4) derive $q$ from 2); 5) derive $\lnot q$ from 1) and 3); 6) derive $\bot$ from 4) and 5) and now we need $\to$-intro to conclude with $\lnot (p \land q)$ from 2) and 6). $\endgroup$ – Mauro ALLEGRANZA Jun 16 '17 at 14:07
  • $\begingroup$ I have a follow-up here: math.stackexchange.com/questions/2325111/… $\endgroup$ – user65526 Jun 16 '17 at 15:09

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}$.


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.

| cite | improve this answer | |

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.