4

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.

Cort Ammon
  • 3,343
  • it’s a bit obtuse, and sounds more like Philosophy than Mathematics. – Thomas Andrews Sep 10 '18 at 16:15
  • @ThomasAndrews It definitely did feel obtuse, but from my own forays into formal logic, some of the things which one feels need to define or assume boggle my mind, so I couldn't immediately discount the possibility. And, from experience, things that are definitions in mathematics do indeed behave differently from other statements that are assumed true. – Cort Ammon Sep 10 '18 at 16:17
  • "but then there you can dispute what counts as proof" -- did they just imply that there cannot be disputes over what counts as proof in mathematics? – Theoretical Economist Sep 10 '18 at 23:58

3 Answers3

13

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.

Hagen von Eitzen
  • 374,180
  • 1
    Well, a proof is a sequence of statements, and an axiom is a statement. So technically, it is not true that an axiom os a proof. :) It does mean that an axiom has a proof. – Thomas Andrews Sep 10 '18 at 16:17
  • IMO, the question is not about the statement "an axiom is a proof", but about the meta-statement ' "an axiom is a proof" is a definition'. –  Sep 10 '18 at 16:25
  • 6
    @ThomasAndrews A single statement is a sequence of length one. – David Richerby Sep 10 '18 at 21:10
  • 1
    Nope, it really is not. There is a relationship, but they are not the same thing. Any more than $x$ and ${x}$ are the same thing. (We are, by nature, being pedantic here.) – Thomas Andrews Sep 10 '18 at 21:22
  • 1
    @DavidRicherby Is that really true? The definition of sequence I know is that it is a function from a subset of N to whatever you're enumerating (axioms), which would make it distinct from an axiom itself. – Norrius Sep 10 '18 at 21:24
  • 3
    There is rarely any loss of clarity or understanding if one identifies one-element sequences with their single element. – David Richerby Sep 10 '18 at 21:29
  • It's worth noting that not all proof systems require a proof to be a "sequence" of statements - for example, in many formulations of natural deduction a proof is a tree (similar to an abstract syntax tree). Though similarly, if you identify a tree with a single leaf node at its root with the contents of that leaf node... – Daniel Schepler Sep 11 '18 at 00:38
2

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.)

2

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

Hans Hüttel
  • 4,271
  • “Is provable” is different from “is a proof.” A proof is a sequence of statements, as usually defined. But a statement is not a sequence of statements (though it can trivially be made to be one.) If this is what the philosophy people mean - that an axiom can be proved from an axiom - then that really is obtuse. – Thomas Andrews Sep 10 '18 at 16:22
  • Please reread my comment, I’m not sure what you are responding to. An axiom is provable. A statement is not a sequence of statements, and a proof is a sequence uence of (one) statement. – Thomas Andrews Sep 10 '18 at 16:31
  • @ThomasAndrews: but the proof of the axiom (within that logic that assumes the relevant axiom) is just the statement of the axiom. – nomen Sep 10 '18 at 20:29
  • No, a proof is a sequence of axioms. A sequence with one element is not the same thing as the element. “What is the length of the proof of (axiom)?” “One line.” What is the length of (axiom)? Depends on what you mean by the length of an axiom, but nobody would say “one line.” That’s because an axiom isn’t a proof. It is a statement. A proof is a sequence of statements. – Thomas Andrews Sep 10 '18 at 20:45