Can a sequence whose final term is an axiom, be considered a formal proof?

Question

Wikipedia gives the following definition of a formal proof:

A formal proof or derivation is a finite sequence of sentences (called well-formed formulas in the case of a formal language) each of which is an axiom, as assumption, or follows from the preceding sentences in the sequence by a rule of inference.

Given this definition, a sequence whose final term is an axiom could qualify as being a formal proof.

What would it be a proof of?

The idea that an axiom can have a formal proof, seems anti-intuitive.

I haven't been able to find a definition of 'formal proof' sufficiently detailed as to unequivocally answer the question posed within the title of this post.

Answer 1

Yes.

Axioms can have proofs. And they can be as short as a sequence of length $1$.

This is only counterintuitive since in high school you learn that "axioms are things which do not have a proof" or something silly like that. No. Axioms are just statements which we assume to be correct in the first place. It does not mean they have no proof.

Not to mention, that an axiom is just a term. The axiom of choice is provable from Zorn's Lemma, as well from the Teichmuller-Tukey principle, and from Zermelo's theorem.

Answer 2

It would be a proof that the axiom is true, given that the axiom is true. So it's a tautology. It would not be an interesting proof, although it is a correct one; most correct proofs do not prove anything interesting.

Answer 3

In a proof (sequence of statements), the axioms can be moved around the sequence arbitrarily since they don't depend on any previous statements. The "conclusion" that is to be proved can be taken to be the last statement that depends on the statements preceding it.