axiom-1 and modus ponens together form sound system , because they are subset of hilbert system (which is sound) . But how to prove it is not complete ? One of the approach is to prove that axiom-2 and axiom-3 cannot be derived . How to show that axiom 2 and 3 cannot be derived from axiom-1 and modus ponens?
axiom 1 : $A→(B→A)$
axiom 2: $(A→(B→C))→((A→B)→(A→C))$
axiom 3: $(¬B→¬A)→(A→B)$
modus ponens : if $A , A→B$ then $B$.
Typoically, to show that some argument is invalid, we show a way of making the premises true and the conclusion false. That won;t work here, since axioms 2 and 2 are truth-functional tautologies.
So, to show that we cannot derive axioms 2 and 3 from axiom 1 plus Modus Ponens, we need to come up with some non-standard interpretation of the symbols and operators involved.
Here is one: Suppose that the propositional variables can take on the values of $0$ and $1$, and that the operators work on those values as specified by the following tables:
\begin{array}{c|c} A&\neg A\\ \hline 0&0\\ 1&0\\ \end{array}
\begin{array}{cc|c} A&B&A \to B\\ \hline 0&0&0\\ 0&1&1\\ 1&0&0\\ 1&1&0\\ \end{array}
OK, now let's put axioms 1 and 3 on a table:
\begin{array}{cc|ccc|ccc} A&B&A & \to & (B \to A)&(\neg B \to \neg A) & \to & (A \to B)\\ \hline 0&0&&0&0&0&0&0\\ 0&1&&0&0&0&1&1\\ 1&0&&0&1&0&0&0\\ 1&1&&0&0&0&0&0\\ \end{array}
Let's call a statement that always evaluates to $0$ a $0$-tautology. Note that axiom-1 is a $0$-tautology, but axiom 3 is not. But now notice that, using Modus Ponens, if $A \to B$ has value $0$, and $A$ has value $0$, then $B$ has to have value $0$ as well. In other words, from $0$-tautologies we can only infer further $0$-tautologies; we can't infer something that is not a $0$-tautology.
So, axiom 3 cannot be derived from axiom 1 and Modus Ponens.
Can you do something similar for axiom 2? You may have to move to a $3$-value system ....
Use condensened detachment to find the pattern of all theorems derivable from axiom-1 which are not substitution instances of other theorems. The pattern is as follows:
$(A_1\rightarrow (B_1\rightarrow A_1))$
$(A_2\rightarrow (A_1\rightarrow (B_1\rightarrow A_1))$
$(A_3\rightarrow (A_2\rightarrow (A_1\rightarrow (B_1\rightarrow A_1))$
And so on.
Since the pattern continues ad infinitum with each successive theorem increasing in length, we can check to see if some formula can be a substitution instance of previous theorems in that sequence.
Note that $((¬B\rightarrow ¬A)\rightarrow(A\rightarrow B))$ is shorter than $(A_3\rightarrow (A_2\rightarrow (A_1\rightarrow (B_1\rightarrow A_1))$. So, we only need to check substitution instances of $(A_2\rightarrow (A_1\rightarrow (B_1\rightarrow A_1))$ and $(A_1\rightarrow (B_1\rightarrow A_1))$. $((¬B\rightarrow ¬A)\rightarrow(A\rightarrow B))$ is not a substitution instance of any of those theorems, and thus not derivable from axiom-1.
And that finishes our meta-proof.
Edit: The same method can get used to show that axiom-2 isn't derivable from axiom-1. Check all theorems that follow from axiom-1 as a result of condensed detachment. Then show that no substitution instance of those theorems can be axiom-2. This method would be much more difficult to use for other formulas, but since the progression of theorems following from axiom-1 under condensed detachment only get longer and longer in terms of the number of symbols, this method works fairly easily here.
