Modus ponens inference I am looking to prove or disprove that the following formula; 
$(\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A)$
can be inferenced in the following formal system $L(\neg, \rightarrow)$
with the following axioms: 
А1: $\varphi \rightarrow (\psi \rightarrow \varphi)$
A2: $(\varphi \rightarrow (\psi \rightarrow \xi)) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\varphi \rightarrow \xi))$
A3: $((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) \rightarrow ((\varphi \rightarrow \psi) \rightarrow (\neg \psi  \rightarrow \neg \varphi))$
 A: With the axioms you gave, the formula is not provable. I've used Mace to find a counter-model, which consists in interpreting "$\neg$" as an operator that always outputs $F$, irrespective of the input truth value. The arrow "$\rightarrow$" is to be interpreted standardly (since A1 and A2 indeed are axioms that capture the material conditional). Along these lines, you can now build a truth table; it will validate all the axioms but disvalidate $(\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A)$.
For your information, I've used Mace on the following input. As assumptions, I chose
Thm(x) & Thm(f(x,y)) -> Thm(y).
Thm(f(x,f(y,x))).
Thm(f(f(x,f(y,z)),f(f(x,y),f(x,z)))).
Thm(f(f(f(g(x),x),x),f(f(x,y),f(g(y),g(x))))).

As the goal, I chose
Thm(f(f(g(x),g(y)),f(y,x))).

Naturally, "Thm" is the predicate for theoremhood. "f" is the functor for "$\rightarrow$", and "g" is the functor for "$\neg$". The first line says theoremhood is closed under Modus Ponens. The next three lines are translations of the axioms. The goal line is a translation of your formula.
Reply to Levitan's comment: You can choose different output formats which may vary in readability. I find the format "cooked" quite readable; it gives you:
% number = 1
% seconds = 0

% Interpretation of size 2

c1 = 0.
c2 = 1.

g(0) = 0.
g(1) = 0.

f(0,0) = 1.
f(0,1) = 1.
f(1,0) = 0.
f(1,1) = 1.

- Thm(0).
  Thm(1).

There you see:


*

*The model has two object in its domain, $0$ and $1$, which we can naturally interpret as false and true, respectively.

*An interpretation for $g$, which I put in place of $\neg$. In an interpretation of $0$ and $1$ as truth values, it accepts truth values as input, and outputs a truth value. In this case, it always outputs $false$.

*Similarly for the two placed functor $f$.

*Finally, theoremhood is interpreted such that the Truth (every true sentence, or more precisely every term that denotes $1$) is a theorem, and falsity isn't a theorem - quite what we'd expect.


This will yield the following truth table:
$$\begin{array}{cc|c}
A & B & \neg A & \neg B & (\neg A \rightarrow \neg B) & (B \rightarrow A) & (\neg A \rightarrow \neg B) \rightarrow (B \rightarrow A) \\
\hline
T & T & F & F & T & T & T \\
T & F & F & F & T & T & T \\
F & T & F & F & T & F & F \\
F & F & F & F & T & T & T \\
\end{array}$$
