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

[Torkel Franzen]

  Neil says:

  >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?

  Well, I did note that


   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.


   Part of my claim was that the "proof in the usual sense" that you
describe above is incomplete as a model of proofs in the general case,
since even if the set of axioms is recursive, and indeed even if we
know the set of axioms to be recursive, we can't necessarily decide
whether a deduction with assumption B1,..Bm and conclusion C is
a proof. We also need an algorithm to decide whether or not a formula
is an axiom.