FOM: Do proofs have to be from a decidable axiom set?

[Neil Tennant]

Torkel objects that it is demanding too much to require that a set of axioms
for a mathematical theory be decidable (= recursive), and proposes instead
the requirement that the set of axioms be only recursively enumerable.

He did not satisfactorily address, however, the epistemological objection
that one would not then, in general, be able to tell when a given construction
was a proof establishing the truth of its conclusion.

Certainly, if you successfully enumerate far enough to get, say, A1,...,An
confirmed as axioms, and then use only A1,...,An as undischarged assumptions
in a proof of C, then you have shown C to be a truth of the area in question.
But in that case your `proof' consists of more than just the conventional
proof that starts by assuming (or asserting) A1,...,An and then taking
logical steps eventually leading to C. For your `proof' has to contain, in
addition, the information that A1,...,An have all been enumerated by some
finite stage within the official enumeration of all axioms. In this case,
the audience for the proof can `tell effectively', of each of the Ai used,
that it is indeed an axiom.

But suppose someone gives you a proof in the usual sense, namely a deduction
with assumption B1,...,Bm and conclusion C? How can you tell effectively whether that establishes the truth of C for the area of mathematics in question? 
If Torkel sets about using his recursive enumeration to confirm the axiomatic 
status of B1,...,Bm, he *might* be lucky and find that each of these Bi is 
generated in due course. But at any stage before all of them have been confirmed as axioms (by appearing somewhere in his enumeration of axioms) he will not 
know whether the non-appearance, thus far, of any given Bj is owing to the fact that Bj is further down in the enumeration, or the fact thast Bj will never 
appear in the enumeration.  So he will be unable to *tell*, effectively, that 
the construction offered is indeed a proof of C.

Neil Tennant