Formal Deduction (logic) Question: $\lnot C, (B \to \lnot C) \to A \vdash (A \to C) \to F$

Question

I've been stuck on this question for around two hours now.

I'm trying to prove that:

$\lnot C, \ (B \to \lnot C)\to A \vdash (A \to C)\to F $

I'm trying to get my second last step to be:

$\lnot C, \ (B \to \lnot C)\to A, \ A \to C \vdash F $,

but I have no idea how to get started. I'm not sure what I can start off with, especially due to the $(B \to \lnot C)\to A)$ part.

I'm allowed to use 11 rules of formal deducibility/deduction.

If anyone can help me get started, or give me some hints, I would be extremely thankful!

Answer 1

The intuition to prove $\lnot C, \ (B \to \lnot C) \to A \vdash (A \to C) \to F$ is that from the assumption $\lnot C$ it follows that $B \to \lnot C$ (if $\lnot C$ holds, then in particular it holds under the additional hypothesis $B$). From that, you can apply modus ponens with $(B \to \lnot C) \to A$ to get $A$, and then you can easily find a contradiction with the assumption $A \to C$ (to be discarded) and $\lnot C$. From a contradiction you can derive everything (principle of explosion or ex falso quodlibet), in particular $F$. Finally, you just have to discharge the hypothesis $A \to C$.

Formally, the derivation in natural deduction that you are looking for is the following:

\begin{align} \dfrac{\dfrac{\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\dfrac{\lnot C \qquad \dfrac{[A \to C]^* \qquad \dfrac{(B \to \lnot C) \to A \qquad \dfrac{\lnot C}{B \to \lnot C}\to_i}{A}\to_e\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!}{C} \lnot_e\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!}{\bot}\lnot_e\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!}{F}\bot_e\!\!\!\!\!\!\!\!\!}{(A \to C) \to F}\to_i^* \end{align}

where the falsehood or absurdity (a formula that is always false) is denoted by $\bot$, and $[A]^*$ stands for an assumption $A$ that has been discharged by the rule $*$.

Answer 2

You can show that $((B\to \neg C)\to A) \iff ((B\land C)\lor A)$.

Now adding $A \to C$ to the hypotheses and using disjunction of cases:
\begin{array}{l} A \\ A \to C \\ \hline C \end{array}
Which considering $\neg C$ is absurd. Also:
\begin{array}{l} B\land C \\ \hline C \end{array}
which is again absurd.
So we've shown that $A\to C$ is false, so $(A\to C)\to F$ is true regardless of $F$.

Answer 3

Not knowing exactly how your formal; rules are defined, it's hard to give an answer, but I am guessing this is probably close to what you're looking for:

\begin{array}{lll} 1.& \neg F \vdash \neg F & Assumption\\ 2.&\ \neg C \vdash \neg C & Assumption\\ 3.&B\vdash B& Assumption\\ 4.&\neg C, B \vdash \neg C \land B & \land I \ 2,3\\ 5.&\neg C, B \vdash \neg C & \land E \ 4\\ 6.&\neg F, \neg C, B \vdash \neg C \land \neg F& \land I \ 1,5\\ 7.&\neg F, \neg C \vdash B \to \neg C & \to I \ 6\\ 8.& (B \to \neg C) \to A \vdash (B \to \neg C) \to A & Assumption\\ 9.& \neg F, \neg C, (B \to \neg C) \to A \vdash A & \to E \ 7,8\\ 10.& A \to C \vdash A \to C & Assumption\\ 11.& \neg F, \neg C, (B \to \neg C) \to A, A \to C \vdash C & \to E \ 9,10\\ 12.& \neg F, \neg C, (B \to \neg C) \to A, A \to C \vdash C \land \neg C & \land I \ 7,11\\ 13.& \neg C, (B \to \neg C) \to A, A \to C \vdash \neg \neg F & \neg I \ 12\\ 14.& \neg C, (B \to \neg C) \to A, A \to C \vdash F & \neg E \ 13\\ \end{array} ... and you know to do the last line :)

Answer 4

Here is one way to show that

¬C, (B→¬C)→A⊢(A→C)→F

hoping that it will provide some hints how one might proceed.

However, it uses the Law of Excluded Middle (LEM), Reiteration (R) and Modus Tolens (MT) besides introduction and elimination rules. Discussions of these can be found in forallx linked to below if one needs alternatives to them.

I assume "F" refers to False or "⊥". If not, since it is not referenced in the premises, one can derive "F" from "⊥" using Explosion.

---

Kevin Klement's JavaScript/PHP Fitch-style natural deduction proof editor and checker http://proofs.openlogicproject.org/

P. D. Magnus, Tim Button with additions by J. Robert Loftis remixed and revised by Aaron Thomas-Bolduc, Richard Zach, forallx Calgary Remix: An Introduction to Formal Logic, Winter 2018. http://forallx.openlogicproject.org/