$\vdash (\lnot \chi \to \lnot \theta) \to (\theta \to \chi) $

Question

For $\theta, \chi$ $\mathcal{L}$-formulas in predicate logic, I'm trying to prove: $\vdash (\lnot \chi \to \lnot \theta) \to (\theta \to \chi) $.

I've managed to prove $\vdash \lnot\lnot \theta \to \theta$, which was the hint for this problem. I have already proved $\vdash (\theta \to \chi) \to (\lnot \chi \to \lnot \theta) $. My attempt was to substitute $\lnot \chi$, $\lnot \theta$ into $\theta, \chi$ in $\vdash (\theta \to \chi) \to (\lnot \chi \to \lnot \theta) $. This gives $\vdash (\lnot \chi \to \lnot \theta) \to (\lnot \lnot \theta \to \lnot \lnot \chi) $. Finally, I was trying to show $\vdash (\lnot \lnot \theta \to \lnot \lnot \chi) \to (\theta \to \chi)$, but was not having much luck. Is there a nice way of doing this?

Furthermore, how does one go about doing things like this? I have seen natural deduction proofs that are very complicated, or are written in a way such that I suspect that there is some motivation that I am surely missing. But I can't figure out how to get the intuition/motivation for natural deduction proofs in general. My attempts purely seem to be brute-forcing, which is not so good.

Answer 1

I have seen natural deduction proofs that are very complicated, or are written in a way such that I suspect that there is some motivation that I am surely missing. But I can't figure out how to get the intuition/motivation for natural deduction proofs in general.

The following proof is based on a form of natural deduction. Simpler than most, it may help. It uses direct proof (lines 8 and 9) and proof by contradiction (line 6).

Note: '=>' is left associative here, so I am proving the equivalent of [~A => ~B] => [B => A].

Screen shot from my proof checker:

Answer 2

I’d do this the following way similarly to what @Mauro has been hinting at in comments but I’m not sure if this is correct in the system for natural deduction you are using.

I’ll use numbers to indicated the levels of „nested proofs”, this is the method of natural deduction I am used (so there are rules for introducing and eliminating different connectives which one can apply)

---

We want $\vdash (\lnot p \to \lnot q) \to (q \to p)$.

1. Let’s assume $(\lnot p \to \lnot q)$. Goal: $q\to p$. So we want $\lnot p \to \lnot q \vdash q \to p$

1.1. Lets assuume $q$. Goal: $p$, ie. $\lnot p \to \lnot q, q \vdash p$

edit: it seems I have messed up the final part. Perhaps this would be better:

1.1.1. proof by contradiction since $\vdash \lnot\lnot p \to p$. So as we recall our goal now was $p$. Lets assume $\lnot p$. Then we have $\lnot p \to \lnot q$ hence we can eliminate the implication and get $\lnot q$.

1.1.2. So now we have both $q$ and $\lnot q$. That's a contradiction -- we achieved the goal ie $\lnot p \to \lnot q, q, \lnot p \vdash \bot$

1.2. So assuming $\lnot p$ we got $\bot$, so we can intro an implication $\lnot p \to \bot$ so $\lnot p \to \lnot q, q\vdash \lnot p \to \bot$ which is equivalent to $\lnot p \to \lnot q, q\vdash \lnot\lnot p$ (intro of negation). Thus we have proven $\lnot\lnot p\leftrightarrow p$ and got our goal

2. we managed to prove $p$ assuming $q$ so we intro $q \to p$ -- we have achieved our current goal. $\lnot p \to \lnot q \vdash q \to p$

So from assuming $\lnot p \to \lnot q$ we have proven $q\to p$. Intro: $\vdash (\lnot p \to \lnot q) \to (q\to p)$

Hope that is correct. My intuition to natural deduction is to realise it s natural so I can just think: when is an implication true? When the antecedent is false (the triv case) or when both parts are true. Let's assume it is true and try proving the rest with those assumptions using those rules for introducing or eliminating different things. Then I simply do it recursively with goals and subgoals etc. Jaśkowski's boxes are good for that as they resemble a computer program with their nested structure.