2
$\begingroup$

I'm looking for a way to prove : $(A \rightarrow B) \rightarrow (\neg B \rightarrow \neg A)$

From the axioms :

A1) $(A) \rightarrow ( B \rightarrow A )$

A2) $(A \rightarrow ( B \rightarrow C )) \rightarrow((A\rightarrow B)\rightarrow(A\rightarrow C ))$

A3) $A \rightarrow (B \rightarrow (A \wedge B ))$

A4) $(A \wedge B )\rightarrow A$

A5) $(A \wedge B )\rightarrow B$

A6) $(A \rightarrow B )\rightarrow ((C \rightarrow B )\rightarrow ((A\vee C)\rightarrow B))$

A7) $A \rightarrow (A \vee B)$

A8) $A \rightarrow (B \vee A)$

A9) $ \neg \neg A \rightarrow A $

and MP

I'm studying in computer science and I don't know any think about logic course. Sorry for easy question and bad english.

  • 1
    a) This is not an answer; it should be part of the question instead. b) You might want to explain a bit about what you're trying to do here. c) As my answer shows that there is no proof, it's an inefficient use of your time to continue searching for one. d) The noun is "proof", the verb is "prove".2011-12-23

3 Answers 3

11

You can't prove this because there's a model for this theory in which it's not true. Let $\to$,$\lor$ and $\land$ have their usual meanings, and let $\neg$ be the identity operation. Then all the axioms hold, but the theorem you want to prove doesn't.

  • 0
    @mobin: As far as "A1)" is meant to indicate that what follows is an instance of the axiom scheme A1 in the question: It isn't, since different variables $A$ and $C$ appear where the axiom scheme has the same variable $A$. The part after "A3)" seems to have little to do with the axiom scheme listed as A3 in the question; I don't understand what you're trying to do. If you insist on trying to prove the unprovable, please add some explanations to your formulas that make them intelligible to other mortals. Again, I believe your time would be better invested in trying to understand my answer.2011-12-24
1

You mention two different axiom systems.

The one is your last comment [(A1), (A2) and (A3) : correcting a typo in (A3); it must be : $(((¬A)→(¬B))→(((¬A)→B)→A))$] is the one used in the "classic" Elliott Mendelson, Introduction to Mathematical Logic (4th ed - 1997): see page 35.

It is sound and complete respect to tautologies; thus, $(A→B)→(¬B→¬A)$ is provable [see Lemma 1.11.e, page 38].

The axiom system in your original question is derived from the 10-axiom system $\mathsf L_4$ of Mendelson [see Example page 42], that is from the axiom system of S.C.Kleene, Introduction to Metamathematics (1952).

But it is lacking of axiom (9) :

$(A→B)→((A→\lnot B)→\lnot A)$.

Thus, the axiom system is incomplete and you cannot prove $(A→B)→(¬B→¬A)$, as stated by Joriki.

0

Dem:

$A1: A\rightarrow B$ Hipothesis

$A2: x\rightarrow ( x'')$

$A3: B\rightarrow B''$ Substitute x with B in A2

$A4: A \rightarrow B'' $ S-Rule(A1,A3)

$A5: A' \lor B'' $ Abbreviation $A\rightarrow B''$

$A6: B'' \lor A' $ Deduction rule on A5: $A\lor B \vdash B\lor A $

$A7: B' \rightarrow A' $ Abbreviation A6