821.sagews

First Verify Statement is truly a Tautology. In this case (TRUE -> TRUE).

Before we attempt to prove.

Check to make sure the TruthTable for your Statement displays all values as TRUE.

import sage.logic.propcalc as propcalc 
f = propcalc.formula("(A->B)->(~B ->~A)"); 
f.truthtable();

A B value False False True False True True True False True True True True

For Giggles we can run is_tautology to verify. This is no neccisary but gives me warm and fuzzies.

import sage.logic.propcalc as propcalc 
f = propcalc.formula("(A->B)->(~B ->~A)"); 
f.is_tautology();

True

If Statement is a tautology then it will not be a Contradiction of course.

f.is_contradiction()

False

Let verify what are all the ways this Statement can be made a tautology. Due to it being a, "if then" Statement we must find all the ways to make P->Q TRUE->TRUE.

import sage.logic.propcalc as propcalc 
P = propcalc.formula("(A->B)"); 
P.truthtable();

A B value False False True False True True True False False True True True

So there are three ways according to this truth table to make P True:

A      B      value
False  False  True   
False  True   True
True   True   True 

import sage.logic.propcalc as propcalc 
Q = propcalc.formula("(~B->~A)"); 
Q.truthtable();

B A value False False True False True False True False True True True True

There appears to be three ways to make Q True:

B      A      value
False  False  True    
True   False  True   
True   True   True

P->Q must both be TRUE to be a Tautology due to the main connective being a Implication. However the values must be opposite if A = FALSE in P then A = TRUE in Q. 

import sage.logic.propcalc as propcalc 
One = propcalc.formula("(~A-> ~B)->(B -> A)"); 
One.truthtable();

A B value False False True False True True True False True True True True

So P: F->F = true
And Q: T->T = true
resulting in a Tautology

One.is_tautology();

True

import sage.logic.propcalc as propcalc 
Two = propcalc.formula("(A-> B)->(~B -> ~A)"); 
Two.truthtable();

A B value False False True False True True True False True True True True

So P: T->T = true
And Q: F->F = true
resulting in a Tautology

Two.is_tautology();

True

import sage.logic.propcalc as propcalc 
Three = propcalc.formula("(~A-> B)->(~B -> A)"); 
Three.truthtable();

A B value False False True False True True True False True True True True

And the third and final opposite pairs

So P: F->T = true
And Q: T->F = true
resulting in a Tautology

Now what would happen if we tried to use the FALSE values for P->Q for their original Truth Tables? P->Q shown respectivly:

A      B      value 
True   False  False  

B      A      value
False  True   False  

import sage.logic.propcalc as propcalc 
False = propcalc.formula("(A->~B)->(~B ->A)"); 
False.truthtable();

A B value False False False False True True True False True True True True

Opps, guess we were right using the FALSE values gives us no Tautology.

False.is_tautology();

False