Can axioms be premises in formal proofs?

Question

If I use an axiom to prove a theorem, i.e. use the axioms of equality in FOL to prove the converse of the axiom of extensionality, do I list those axioms as premises in a formal proof?

The answer seems obvious already but doing that means that the theorem I'm actually proving is $$\text{axioms of equality in FOL}\vdash\text{converse of axiom of extensionality}$$ and not the latter independently. Is there a rule that allows me to independently write down the statement that follows after $\vdash$ when I know that the statement preceding it is true?

Answer 1

The symbol $\vdash$ is not really what you want. You are doing metalogic, so to speak, and the first rule is not to mess up with notation and conflate lower order logic with higher order logic. Something like $\Rightarrow$ is more suitable.

Furthermore, you cannot do metalogic over FOL as you were actually doing FOL. You are quantifying over sets, sets of sets, etc. You are outside FOL.

Those axioms define the symbol $=$ in a higher order metalogic, and the symbol is employed as a primitive term (what means it cannot be "proved"). You should think of axioms as definitions of its terms and the related concepts appearing in the axiom. I highly recommend you read Tarski to have a superb and clear overview of all of these issues.

Thus, proving one axiom from the other might be useful, although it is perhaps not what you think you are doing. If you strip the axiom of extensionality out of the equality symbol/concept, you still do set theory. If you want to do FOL with equality, then you introduce the equality symbol in the axiom of equality.

Anyway, Equality in mathematics comes with plenty of different flavors. Philosophically speaking, there seems to be nothing better than Leibniz's definition.