1
$\begingroup$

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

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ 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? $\endgroup$ – Patrick Stevens Nov 7 '15 at 18:54
  • $\begingroup$ 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 $\endgroup$ – Levitan Nov 7 '15 at 18:54
  • $\begingroup$ For what statements $\varphi$ is $((\neg \varphi \rightarrow \varphi) \rightarrow \varphi) $ true? $\endgroup$ – Simon S Nov 7 '15 at 19:02
  • $\begingroup$ @PatrickStevens There is no way to massage such in this case. $\endgroup$ – Doug Spoonwood Nov 7 '15 at 22:00
  • $\begingroup$ @DougSpoonwood - oh, my bad. I assumed it would be possible to obtain $\neg \neg p$ iff $p$, without really thinking further. $\endgroup$ – Patrick Stevens Nov 7 '15 at 22:29
3
$\begingroup$

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

|cite|improve this answer
$\endgroup$
  • $\begingroup$ 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 $\endgroup$ – Levitan Nov 9 '15 at 15:14

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.