Proving if statement is true by proving the converse is false Can we prove an if-statement by proving the converse is false. I.e.
$\lnot (B \implies A) \implies (A \implies B)$
I've spoken to several colleagues about this and I'm still not convinced this proof is both valid and sound. The
The logical statement
$\lnot (B \rightarrow A) \implies (A \rightarrow B)$
is valid. This can be checked by means of a truth table. However,the antecedent implies $\lnot A$ which feels like it should violate soundness.
 A: *

*Logically, the non-quantified statement $$\text{Amy being a vegan implies that she eats beef}$$ and its converse $$\text{Amy eating beef implies that she is a vegan}$$ cannot both be false: if one is false, then the other must be vacuously true.


*However, the quantified statement $$\text{Every vegan eats beef}$$ and its converse $$\text{Every beef-eater is a vegan}$$ are both false.
Explanation
The open formula $$A(x)\rightarrow B(x)$$ might not have a definite truth value, but is often implicitly universally-quantified to actually mean the sentence $$\forall x\,\Big(A(x)\rightarrow B(x)\Big).$$ The crux of your dilemma, as suggested by DanielV, stems from conflating the above with the sentence $$A \rightarrow B.$$

*

*The sentence $$\lnot (B \rightarrow A) \rightarrow (A \rightarrow
   B)$$ is a tautology. Thus, $$\text{not }\Big(B{\implies}A\Big)$$
logically entails $$A{\implies}B.$$

*On the other hand, the sentence $$\lnot\forall x\,\Big(B(x)\rightarrow
   A(x)\Big)\,\rightarrow\,\forall x\,\Big(A(x)\rightarrow B(x)\Big)$$ is
(satisfiable but) invalid. Thus, $$\text{not }\forall x\,
   \Big(B(x){\implies}A(x)\Big)$$ does not logically
entail $$\forall x\,\Big(A(x){\implies}B(x)\Big).$$
A: It depends on if there is an implicit quantifier or not.  For example:
$x \text { is even } \to x \text{ is odd}$
Both that and the converse is false.  So using the falseness of one to prove the truth of the other would be a fallacy. However, because there is an implicit $\forall x$ in front of it, it is language sensitive whether you want to say it even has a converse.
On the other hand, if you look at the truth table of implication:
$$\begin{array} {cc|c}
A & B & A \to B \\
\text{T} & \text{T} & \text{T} \\
\text{T} & \text{F} & \text{F} \\
\text{F} & \text{T} & \text{T} \\
\text{F} & \text{F} & \text{T} \\
\end{array}$$
You can see that the only way for a statement $A\to B$ to be false is for $A=\text{T}$ and $B=\text{F}$, which determines that $B\to A$ is in fact true.  But this only works if there are no free variables, which is to say: no implicit quantifiers.
So you could correctly use the falseness of
$$1=1 \to 2=3$$
to prove
$$2=3 \to 1=1$$
But you'll find there are very few statements like that in mathematics without free variables, which is implicit quantification.  And that type of statement is vacuous anyway which also makes it less likely to come up.
A: "However,the antecedent implies ¬A which feels like it should violate soundness."
The antecedent (the implication $\lnot$(B$\rightarrow$A)) implying $\lnot$A, on the contrary, further enforces soundness.  Soundness means that if the premises are all true, than the conclusion will hold true.  Validity means that it's impossible for the premises to hold true and the conclusion to be false.  Basically any implication which is always true will also imply validity for associated rules of inference and enforces soundness when the axioms are tautologies.  This works this way, because of the meta-theorem: From ($\alpha$$\rightarrow$$\beta$) we can infer $\alpha$$\vdash$$\beta$, which allows us to get rules of inference from tautologies quickly.  So, it suffices to demonstrate that the implication is a tautology for associated rules of inference to work out as valid and will help to enforce soundness.
Since truth tables haven't sufficed, I'll appeal to two logical laws below directly, after analyzing what follows from the denial of an implication.
If we have $\lnot$(B$\rightarrow$A), then two propositions immediately follow: the antecedent is true and the consequent is false.  So, we have B here.  We also have $\lnot$A here.
There accordingly exist two relevant logical laws for showing that (A$\rightarrow$B) follows from this.  ($\alpha$$\rightarrow$($\beta$$\rightarrow$$\alpha$)) and ($\lnot$$\alpha$$\rightarrow$($\alpha$$\rightarrow$$\beta$)).
Proof 1:  Given $\lnot$(B$\rightarrow$A), we have $\lnot$A.  So, since ($\lnot$$\alpha$$\rightarrow$($\alpha$$\rightarrow$$\beta$)) is a logical law, (A$\rightarrow$B) follows by one application of modus ponens. Therefore, invoking conditional introduction also, ($\lnot$(B$\rightarrow$A)$\rightarrow$(A$\rightarrow$B)).
Proof 2: Given $\lnot$(B$\rightarrow$A), we have B.  So, since ($\alpha$$\rightarrow$($\beta$$\rightarrow$$\alpha$)) is a logical law, (A$\rightarrow$B) follows.  Therefore, invoking conditional introduction also, ($\lnot$(B$\rightarrow$A)$\rightarrow$(A$\rightarrow$B)).
