How to find out whether the formal system is complete and sound?

Question

I have a simple formal system S(!,->), where there are two possible axioms:

AX1 = ((A->B)->A)
AX2 = (A->(B->A))

The only rule is modus ponens.

I'm trying to decide, whether the formal system is sound and complete - we can consider 3 formal systems: System with only one axiom - AX1 or AX2 and system with both axioms.

My thoughts:

1. I think that the system with axiom AX1 can't be sound because, as far as I know, axiom should be tautology, therefore it can't be complete either.

EDIT: The thought 1 is incorrect. Axioms don't have to be tautologies as far as I know.

EDIT2: On of my problems is that I can't derive even one formula from the system (either AX1,AX2 or AX1-AX2). I'm lost.

Answer 1

To show that a formal system is not sound, you only need to show that one of the axioms could take on the value of falsity. That handles two of the possible choices here.

For the third choice, consider the axiom (A->(B->A)). You can instantiate that axiom with any well-formed formula in place of all As, and any well-formed formula in place of all Bs. The only condition on doing that is that each A needs to get instantiated as the same well-formed formula.

For another way of looking at that, we can substitute any instance of 'A' in that axiom with any well-formed formula provided that such substitution qualifies as consistent, and we can substitute any instance of 'B' with any well-formed formula.

Now you have only axiom. To derive something, you need one well-formed formula of the form ($\alpha$->$\beta$) and another of the form $\alpha$. So, with the above paragraphs about instantiating an axiom, or substituting, does it now seem possible to find such forms?

Here lies a deliberately poor example of a valid proof:

Axiom                  (A          ->(B->A          ))
Instance of the axiom  ((A->(A->A))->(A->(A->(A->A))))
Another instance       (A->(A->A))
Use of modus ponens    (A->(A->(A->A)))

To find a richer example of a proof, try to keep in mind that every axiom is an instance of itself, and that every axiom is a well-formed formula.

To show that the system is not complete you just need to show that there exists some tautology which can't get derived. All we know here is that we have a connective ->. So,

(A->A)

is a tautology.

So, go back and look at all possible proofs from AX2. What happens when you detach something? Are instances of the axiom or any of the other provable well-formed formulas shorter, the same length, or longer than the axiom ever? Is what you detach shorter, the same length, or longer than the axiom ever?

Edit:

Assume that you adopt the following "prohibitions" for substitutions in the axiom.

1. You can only substitute a well-formed formula for A in the axiom if it consists of the axiom or if it consists of a previously proved theorem.
2. You can only substitute a well-formed formula for B in the axiom if it consists of a formula which looks like it has both exactly one letter and a unique name for a natural number sub-scripting that letter which does not appear in any previously proved theorem.

I suggest next proving the following as a lemma:

Every theorem in this system is either the axiom, a substitution instance of the axiom, a theorem derivable using the above two rules and modus ponens, or a substitution instance of a theorem derivable using the above two rules and modus ponens.

Maybe you also need another lemma:

Every substitution instance of a well-formed formula has the same or greater length than the well-formed formula.

Then from the lemmas it should follow that (A->A) is not provable.

Answer 2

$$ \dfrac{ \dfrac{\text{Ax2}}{a \Rightarrow (b \Rightarrow a)} \quad \dfrac{\text{Ax1}}{(a \Rightarrow (b \Rightarrow a)) \Rightarrow a} }{a}$$

This is a proof of $a$, an arbitrary formula. This shows the system to be unsound but also complete by common meaning.