2
$\begingroup$

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$

$\endgroup$
6
  • $\begingroup$ Your $\to$Elim rule lacks a $\Delta$ somewhere in the conclusion. $\endgroup$
    – hmakholm left over Monica
    Jun 16, 2017 at 13:41
  • $\begingroup$ Thanks, I have edited it. $\endgroup$
    – user65526
    Jun 16, 2017 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, 2017 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, 2017 at 14:07
  • $\begingroup$ I have a follow-up here: math.stackexchange.com/questions/2325111/… $\endgroup$
    – user65526
    Jun 16, 2017 at 15:09

1 Answer 1

Reset to default
3
$\begingroup$

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.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .