# If F→G is a consequence of F, then so is ¬G→¬F. A direct proof?

Homework question (introduction to logic):

"If $F \to G$ is a consequence of $\mathcal F$, then so is $\lnot G \to \lnot F$. We refer to this rule as $\to$-contrapositive. Verify this rule by giving formal proof."

My attempt at proving it (by contradiction):

$H: \lnot G \to \lnot F$
$(1)\quad\mathcal F\vdash F \to G \quad$ {assumption}
$(2)\quad\mathcal F \cup \{ \lnot H \} \vdash \lnot ( \lnot G \to \lnot F) \quad$ {assumption for contradiction}
$(3)\quad\mathcal F \cup \{ \lnot H \} \vdash \lnot(\lnot F \lor G)\quad$ {from $\vdash \lnot (\phi \to \psi) \equiv \psi \lor \lnot \phi$, and line: 2}
$(4)\quad\mathcal F \cup \{ \lnot H \} \vdash F \land \lnot G\quad \quad${from deMorgan's Law and line: 3}
$(5)\quad\mathcal F \cup \{ \lnot H \} \vdash F \quad \quad$ {$\land$ - elimination, line: 4}
$(6)\quad\mathcal F \cup \{ \lnot H \} \vdash \lnot G \quad \quad$ {$\land$ - elimination, line: 4}
$(7)\quad\mathcal F \cup \{ \lnot H \} \vdash G \quad \quad$ {$\to$ - elimination, lines: 1, 5}
$(8)\quad\mathcal F \cup \{ \lnot H \} \vdash G \land \lnot G\quad \quad$ {$\land$ - introduction, lines: 6, 7}
$\quad \quad\mathcal F \vdash H .\square$

question 1: Can you verify if it's OK/ give hints what's wrong if it's not?
question 2: Is there a direct proof?

[edited]

• When you ask about formal proof homework, you always need to specify exactly which formal system you want to carry out the proof in. There are many different systems of formal logic that are equivalent in the sense that they prove the same theorems, but with formal proofs that can look radically different. It looks rather strange that you're apparently working in a system that allows both De Morgan's laws and things like "$\land$-elimination" to be primitive proof steps at the same time. – hmakholm left over Monica Mar 26 '13 at 16:13
• ... not to mention that in line 3 you appear to be appealing to a semantic fact ($\vDash$), which is not something one would expect to find in a formal proof. – hmakholm left over Monica Mar 26 '13 at 16:24
• @HenningMakholm in comment to line 3 I meant that I'm 'allowed' to use that 'rule' because I derived it earlier. The system I'm using is propositional logic with minimal set of axioms: conjunction/disjunction introduction/elimination, modus ponens, double negation elimination, law of the excluded middle (I hope I listed them all, but am not sure). – Vlad K. Mar 26 '13 at 16:52
• x @Pawel: In general you need to show your axioms instead of simply naming them; different systems tend to use the same names for axioms that do more-or-less the same high-level job but are phrased differently in ways that matter here. Also note that "propositional logic" is the name of the family of systems that have the same axioms, not a (generally understandable) name for a particular system. – hmakholm left over Monica Mar 26 '13 at 17:56
• x @Pawel: If your rule in line 3 is a derived rule, then you should have notated it with $\vdash$ instead of $\vDash$ -- the two-horizontal-lines turnstile is generally used for semantic reasoning about interpretations and model, whereas $\vdash$ is for "a formal proof exists". – hmakholm left over Monica Mar 26 '13 at 17:57

$H: \lnot G \to \lnot F$
$(1)\quad\mathcal F\vdash F \to G \quad$ {assumption}
$(2)\quad\mathcal F \vdash \lnot G$ {assumption for direct proof}
$(n)\quad\mathcal F \vdash \lnot F$ {reasons...}