Originally Posted by

**roberts** Alex,

Repeat isn't an axiom, it's a rule of inference, much like modus ponens. We cannot state modus ponens as an axiom (assuming we have no other rules of inference), because we wouldn't be able to draw any inferences from it. Of course, MP has an associated axiom, i.e. [p -> (p -> q)] -> q, but then so does repeat, i.e. p -> p (which is clearly tautologous).

The rule of repeat usually isn't even stated as a rule, it is given as part of the definition of a proof, i.e. a proof from \Gamma to \phi is a finite sequence of formulas such that each member of the sequence is either an axiom, a member of \Gamma (REPEAT), or derived from other previous members of the sequence by means of some rule (which, in hilbert style presentations is simply MP).

Hope this helps.

Sam

Correction: MP is an axiom of the proof-theory, but it's not a logical axiom. But in the proof-theory it's also an axiom that \Gamma implies phi for all phi in \Gamma.