# 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))$

• Note that Axiom 3 has a consequent which is very nearly what you want. How can you massage your statement into a form which matches that consequent? – Patrick Stevens Nov 7 '15 at 18:54
• I have few long tries to inference it but it hasn't led me to success. Probably I don't know some useful fact or bad in applying of MP in the right way – Levitan Nov 7 '15 at 18:54
• For what statements $\varphi$ is $((\neg \varphi \rightarrow \varphi) \rightarrow \varphi)$ true? – Simon S Nov 7 '15 at 19:02
• @PatrickStevens There is no way to massage such in this case. – Doug Spoonwood Nov 7 '15 at 22:00
• @DougSpoonwood - oh, my bad. I assumed it would be possible to obtain $\neg \neg p$ iff $p$, without really thinking further. – Patrick Stevens Nov 7 '15 at 22:29

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}$$

• Could you please provide me with even more details regarding the counter model? I have checked the manual and digged the topic, but still I do not understand the output it gives goo.gl/7SNMAu and the way to build a counter model – Levitan Nov 9 '15 at 15:14