4
$\begingroup$

I came back to learn proving with natural deduction and I find it really hard to see the initial concept. If it's consisting out of bunch of implications it's fairly easy to do it with Modus Ponens and other tools but how to do it in the following example?

$$p \Leftrightarrow q, \neg p, \neg(q \Rightarrow r) \vee t, (s \vee t) \Rightarrow r\vdash r \wedge \neg q$$

Now, obviously I know all of the natural deduction rules but it's hard to me to see which ones could be more useful than the others and what is the way of proving these examples? Here's another example that seems even harder than the first one:

$$(\neg p \vee q) \Rightarrow r, r \Rightarrow (s \vee t), \neg s \wedge \neg u, \neg u \Rightarrow \neg t \vdash p$$

Important note: I don't want you to just solve this example, all I am looking for is the explanation of thought process and why some formulas would be more useful in this case etc.

$\endgroup$
2
  • $\begingroup$ Unfortunately, without the rules of your system being listed, it’s hard to say how you should proceed. The general idea is that since you’re proving a conjunction, you need to be able to prove both conjuncts. Your elimination rules will be on your premises, and the introduction rules will be for sub-conclusions or your conclusion. You’ll want to do $\lor$ elimination on $\neg (q \to r) \lor t$. For the second one, you’ll want to use double negation elimination, since you’ll want to show that $\neg p$ leads to a contradiction. $\endgroup$
    – PW_246
    Commented Jun 2 at 20:15
  • $\begingroup$ It takes practice to be able to recognize what to do next. Start by doing simpler problems, gradually increasing the level of difficulty. If the solution is not immediately apparent, I usually start by entering the required theorem into a proof checker as an axiom or premise. Then, by a process resembling trial and error, I apply various rules of inference to parts of that statement. Hopefully, the solution will just come to you. $\endgroup$
    – Dan Christensen
    Commented Jun 3 at 16:49

1 Answer 1

Reset to default
5
$\begingroup$

Intuitionistic propositional logic is mostly nice and syntax-directed, so you can just do the obvious thing at each step:

  • We want to prove $r \land \neg q$; let's start with $\neg q$ since that's easier.
    • We have $\neg p$ and $p \Leftrightarrow q$, hence $\neg q$.
    • We want $r$; the only hypothesis that can help us is $s \lor t \Rightarrow r$, so let's make $s \lor t$ our new goal.
      • There's no way to get an $s$, so let's try proving $t$.
      • We have $\neg (q \Rightarrow r) \lor t$, so let's reason by cases:
        • If $t$, we're done.
        • If $\neg (q \Rightarrow r)$, we might try to show $q \Rightarrow r$ to get a contradiction. So let's assume $q$ and try to prove $r$. We saw earlier that we can show $\neg q$, and we assumed $q$, so we have a contradiction. We're done.

You can package this up as a $\lambda$-term:

$$ \lambda a b c d. \langle d (\iota_2 (\mathsf{case}\ c\ \mathsf{of} [\iota_1\ x. \mathsf{absurd}\ (x (\lambda q. \mathsf{absurd}\ (b (\pi_2\ a\ q)))); \iota_2\ t. t])), b \circ \pi_2\ a \rangle $$

You can even automate this, using something like Dyckhoff's LJT calculus to avoid loops.

$\endgroup$

You must log in to answer this question.

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