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.

  • 2
    $\begingroup$ Sound means : it proves only valid formulae. But the axiom is not valid, becuase it is not a tautology. Thus, the single line derivation with Ax.1 is a proof on an invalid formula. $\endgroup$ – Mauro ALLEGRANZA Nov 6 '16 at 18:07
  • $\begingroup$ @MauroALLEGRANZA Thank you Mauro. So I suppose that system with AX1 and system with AX1 and AX2 aren't sound because otherwise, they would proof only valid formulas, therefore they can't be complete too. So the only system which can be sound and complete is the one with only AX2. $\endgroup$ – Milano Nov 6 '16 at 18:10
  • 1
    $\begingroup$ Quite right ... Ax.2 is a tautology and thus the system $\{ \text {Ax.2} \}$ is sound, but not complete (assuming that you use the "standard" def : prove all tautologies) : how you prove e.g. $(\lnot A \to \lnot B) \to (B \to A)$ ? $\endgroup$ – Mauro ALLEGRANZA Nov 6 '16 at 18:12
  • $\begingroup$ I can't figure out how to derive any formulae from these axioms which is not one of them. Do you have any? According to your formulae, yes it can't be derived but how to proove that? Thanks $\endgroup$ – Milano Nov 6 '16 at 18:21
  • $\begingroup$ If I want to derive any formulae using AX1 or/and AX2 and modus ponens, I would need to find some "X" and "X->Y" so I could derive "Y". But it's not possible from this. $\endgroup$ – Milano Nov 6 '16 at 18:25

$$ \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.


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,


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?


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.

  • $\begingroup$ Dough, thank you for your explanation. I have just one question. Is it really true that A->A is not derivable? There are situations when we can derive smaller formulae than axioms. $\endgroup$ – Milano Nov 7 '16 at 9:10
  • $\begingroup$ @Piotr See my edit. $\endgroup$ – Doug Spoonwood Nov 7 '16 at 18:06
  • $\begingroup$ @Piotr I've edited the second "prohibition". If you ever learn condensed detachment, you'll probably find it easy to see that (A->A) is not provable ever if (A->(B->A)) is the only axiom without even working through a proof. When using condensed detachment you look for one of the most general derivable theorems from two well-formed formulas (usually axioms or theorems). Which one you find doesn't much matter, because each of them can get obtained for any of the others just by substitution of one or many of the variable(s) by variable(s). $\endgroup$ – Doug Spoonwood Nov 7 '16 at 21:38

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.