mjhjmtu

From this comments discussion on Philosophy.SE:

"Check out formal logic resources - I'm not going to dig them out for you. Alternatively ask on Math.SE. An 'axiom is a proof' is a definition in formal logic - and not an axiom. In philosophical logic, you can dispute this - but then there you can dispute what counts as proof."

This comment did not align with the definitions I have always used in my head. I have always treated an axiom as a statement that is assumed true without a proof, and a proof is a structure with which one proves the truth of a conclusion given the assumption that its premises are true.

As one descends deeper into formal logic, is there a school of thought where "an axiom is a proof" is actually a definition? I haven't been able to find anything to support this in my searches on the internet, but the original poster of the comment is quite confident that searching will reveal said defintion.

One can say that a proof of a statement $X$ is a finite sequence of statements where a) each statement in the sequence is either an axiom or follows from some previous staements via one of a handful of rules of inference and b) the last statement in the sequence is $X$.
- So if the statement $X$ is already an axiom, the one-term sequence with only term $X$ constitutes a proof of statement $X$. Hence if you do not distinguish between $X$ and the one-term sequence with only term $X$, tha claim is correct and an axiom fulfills the definition of a proof.

In the usual formulation of a proof system, a formula $phi$ is provable if either

• $phi$ is an axiom of the proof system, or


• $phi$ can be concluded from formulae $phi_1,...,phi_n$ that are provable in the proof system, using one of the proof rules of the system

Therefore we cannot say that "an axiom is a proof", since we have to say that a proof is a proof of something. But we can say that if $phi$ is an axiom in our proof system, then the axiom $phi$ constitutes a proof of $phi$.

I guess both can hold, though this discussion has little to do with formal logics.

"An axiom is a proof" could be seen as a definition in a (meta)theory where you previously defined a proof. But without more restrictions, this merely creates an alias and is usually not done.

But in a theory where you defined both an axiom and a proof, with different meanings, you could adopt an axiom saying "an axiom is a proof".

In common mathematics, an axiom is a proposition accepted without a proof, whereas a proof is the logical deduction of a proposition from the available axioms. (The axioms are independent, you can't derive one from the others.)