# Axiom 3 of Hilbert System

I have seen that Axiom 3 of the Hilbert System is sometimes written as:

1: $( \neg A \rightarrow B) \rightarrow ( ( \neg A \rightarrow \neg B) \rightarrow A)$

and then sometimes it is:

2: $( \neg A \rightarrow \neg B) \rightarrow (B \rightarrow A)$

and even:

3: $( \neg B \rightarrow \neg A) \rightarrow ( ( \neg B \rightarrow A) \rightarrow B )$

is one more correct than the other, or do they all mean the same thing? How can you convert between (1) and (2)?

-
Between 1 and 3: take 1, switch A and B, replace now the A by not-A. However it's maybe not the way the system is used, namely some of these systems require everything to be developed from the initial axioms, which bars one from doing things like replacing a symbol by its negative and using not-not-A equals A. That last result may not occur until later in the system. –  coffeemath Oct 9 '12 at 3:07
@coffeemath: There is no need to replace $A$ by $\neg A$. Instead, you switch $\neg B \rightarrow \neg A$ and $\neg B \rightarrow A$. –  beroal Oct 9 '12 at 22:32

These three axioms are all equivalent*, meaning that, once you assume the first two traditional axioms of a Hilbert system (i.e., $p\to(q\to p)$ and $(p\to(q\to r))\to((p\to q)\to(p\to r))$), assuming any one of the three axioms you list will allow you to prove both of the others (such proofs are left as an exercise to the reader). The only reasons to prefer one formulation over another are (a) a specific formulation might yield shorter/easier proofs that you care about in the early stages of deriving propositional calculus, and (b) the text you're using might make use of a specific version.

Also note that there really is no single Hilbert system; the term refers to a type of system, of which there are numerous instances, each with its own set of axioms. However, each system is capable of proving the exact same propositions, albeit in different ways (at least, once you segregate the systems into classical logic, intuitionistic logic, etc., the latter class proving only a proper subset of the statements proven by the former).

* For the sake of full disclosure, I'm only certain that (2) and (3) are equivalent; I've never seen (1) before, but its similarity to (3) is enough for now to convince me that it's equivalent to the others.

-
The first part of this answer talks about the equivalence of the axiom sets, NOT the equivalence of the axioms. The equivalence of axioms concerns where we can deduce one axiom from the other with the same rule(s) in place. –  Doug Spoonwood Jul 4 '13 at 1:21
It is simply not the case that (2) and (3) are inter-derivable. –  Doug Spoonwood Jul 4 '13 at 1:36

Axiom 1 is NOT equivalent to axiom 2 in the sense that you can't deduce axiom 2 with just 1 and modus ponendo ponens. At least according to the model that Mace4 (all models here I've obtained with Mace4, I haven't checked them) gives me:

 →  0  1  2  ¬
0  1  1  1  0
1  2  0  2  0
2  0  0  0  0


Axiom 1 is NOT equivalent to axiom 3 according to this model:

 →  0  1  2  ¬
0  0  1  1  1
1  0  2  0  1
2  2  1  1  1


Axioms 2 is NOT equivalent to axiom 3 according to this model:

 →  0  1  ¬
0  1  0  0
1  0  1  1


Axiom 2 is the shortest (if you want to do metalogic or explain the difference between metalogic and logic, and have no idea as to how to start, counting symbol length is probably the simplest way to go). If you use the resolution theorem on axiom 2, the derived rule of inferences obtainable from axiom 2 are both probably more clearly and easily comprehended than using the resolution theorem in a corresponding manner on the other two axioms (and you can always use the resolution theorem anytime you have modus ponens, even if you don't have the deduction theorem). It also comes as the simplest to check that it's a wff (or formula), once you clarify the intended meaning of it.

-