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

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.

• You are very close! You have $\vdash \neg \neg \theta \to \theta$, but you will also need the other direction, so $\vdash \theta \to \neg \neg \theta$. Then you should be able to string together implications. To give a proper answer we would need to know what kind of formal system you are using. But to your last question (how to go about this): I think the general approach is to first try and prove this in words. Then you can always try to formalise it. – Mark Kamsma Feb 24 at 10:48
• To give an example of what I mean by "prove in words": let's prove $\vdash \neg \neg \theta \to \theta$ in words. We assume $\neg \neg \theta$. Suppose now for a contradiction that we do not have $\theta$, so $\neg \theta$. Then we have both $\neg \neg \theta$ and $\neg \theta$, which is a contradiction. Thus $\theta$ must hold. Since we assumed $\neg \neg \theta$ at the start we conclude $\neg \neg \theta \to \theta$. You might actually count this already as a full proof, depending on how formal you want to get. – Mark Kamsma Feb 24 at 10:50
• You have to assume $\theta$ and $\lnot \chi$ and derive $\bot$, from which, by $\to$-intro, derive $\lnot \lnot \chi$. The conclusion follows by Double Negation elimination. – Mauro ALLEGRANZA Feb 24 at 10:56
• What is "the intuition/motivation for natural deduction proofs in general"? For derivations like that above, it is quite simple. It is a conditional: thus, assume the antecedent as premise and conclude with $\to$-intro. Also the purported conclusion is a conditional: thus, do the same. – Mauro ALLEGRANZA Feb 24 at 10:58

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:

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

1. 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.

• 1.2 is wrong. Up to that point you have: $¬p→¬q,q,¬p ⊢ ⊥$. If now you use EFQ to derive $p$ you will have $¬p→¬q,q,¬p⊢p$ and from it $¬p→¬q,¬p⊢q → p$ but assumption $¬p$ is still there. – Mauro ALLEGRANZA Feb 24 at 13:17
• yes, i think you may be right. Perhaps it would be better to conclude after 1.1.2 that we had proven $\lnot p \to \bot$ which is equivalent to $\lnot \lnot p$, from which we have $p$. So to put it simplier forget the efq and simply say that $\lnot p\to \bot\vdash p$ thus achieving the goal in 1.2. Would that be correct? – ggegoge Feb 24 at 14:18