I'm trying to prove that Mendelson's Standard Axiom System, i.e.
$A\to (B\to A)$
$(A\to(B\to C))\to((A\to B)\to(A\to C))$
$(\neg A\to \neg B)\to ((\neg A\to B)\to A)$
(plus Modus Ponens obviously) would be incomplete omitting the 3rd axiom. I was hinted so in order to do that I should first prove this:
Given a proposition $A$, let $A^+$ be the same proposition after deleting all occurrences of the negation connective ($\neg$). Show that if proposition $A$ can be inferred in this omitted version of the system, then $A^+$ must be a tautology.
I was able to show incompleteness assuming the above statement is correct, but cannot figure out how to show it.
As possibly another approach, if you look at the sub-system with the first two axioms under condensed detachment the axioms and their consequences can only generate implications without any negation symbols appearing anywhere. Why? Because there are no negations in any place of the first two formulas, and unification thus won't generate any consequents with any negations before detachment. And thus anything after detachment still has no negations. Finally, adding any generated conclusion to the premise set under condensed detachment also doesn't have any negations, so no formula that can get generated eventually has a negation in it. So, anything obtainable in that system works as a special case of some formula with only implication symbols, variables, and parentheses.
Notice that substitution always lengthens formulas. Now, as an example, consider this little tautology:
($\lnot$$\lnot$A $\rightarrow$ A).
By the above, it would have to qualify as a special case of
(B $\rightarrow$ A) or (A $\rightarrow$ A) since those make for the only two possible well-formed formulas up to re-lettering.
The first is not a tautology and thus can't get used to obtain the law of double negation above. The second can't get used to obtain the law of double negation, since the law of double negation doesn't have the same number of negation symbols on the left side (antecedent) as on the right side (consequent) as any instance of (A $\rightarrow$ A) does.