FOM: decidability of sets of axioms

[Torkel Franzen]

  Neil says:

  >It's especially important to mathematicians for their set of axioms (in any
  >given area, such as arithmetic or geometry or set theory) to be decidable
  >[= recursive, assuming Church's Thesis]. The reason is obvious: one needs
  >to be able to *tell*, effectively, when a proof establishes a theorem of the
  >area in question; and for this, one needs to be able to determine, of each
  >premise of the proof, whether it is a permissible axiom.

  Although I've said similar things myself often enough, it only now
occurs to me that this isn't really convincing, if one takes the
epistemological motivation seriously.

  The basic premise is that we need to able to decide whether a
proposed proof is a proof. I will accept this basic premise, although
it is not an immediate consequence of the necessity of avoiding an
infinite regress in proving theorems. (Merely being able to verify
that a correct proposed proof is a proof, while coming to no
conclusion in the case when it is not a proof, would be sufficient to
avoid such a regress.)

  But then it's not enough that the set of axioms *is* recursive. To
be able to check a proposed proof we also need to know that the set
of axioms is recursive, and in fact we need to have an algorithm for
deciding whether or not a formula is an axiom. Such an algorithm, then,
is an implicit part or parameter of the proof, from an epistemological
point of view.

  If the set of axioms is not recursive, but recursively enumerable,
the property of being a proof will still be decidable, if we regard
as part of the proof the generation, using an algorithm for enumerating
axioms, of the axioms actually used in the proof. The basic premise,
then, is satisfied even if we only require the axioms to be recursively
enumerable.

  I therefore think that what the epistemological argument supports is
only the need for the set of axioms to be recursively enumerable. A
slightly different formal model of proofs is presupposed - one in which
a proof incorporates an algorithm for generating axioms together with
computations generating the axioms used, rather than just incorporate
an algorithm for deciding axiomhood - but I see no good reason why
the latter model should be preferred.

  Concluding remarks:

 By Craig's lemma, of course, there is always an axiomatization using
a recursive set of axioms, if there is an axiomatization using a
recursively enumerable set of axioms. But as we know, the axioms generated
by Craig's lemma are distinctly unnatural. So I suggest that

  1] Questions that are usually cast in terms of recursive sets of axioms
are often better cast in terms of recursively enumerable sets of axioms,
with stricter conditions on the form of the axioms. In the case at issue,
I think the question whether PA is axiomatizable using a recursively
enumerable subset of the induction axioms, none of which is a logical
truth, is a better one than the corresponding question for recursive
subsets (which - and this admittedly is just an impression - introduces
questions of decidability extraneous to the epistemological core of the
question), or the corresponding question for recursive axiomatizations
in general (which we have seen has a trivial answer).

  2] When we actually want to consider stronger conditions on axioms
than recursive enumerability, recursiveness to is too weak, and
the concept of schemata or some suitable generalization is much the better
notion.