FOM: Decidable axioms sets and algorithms in proofs

[Torkel Franzen]

  Neil says:

  >Can you make plausible any (necessarily classical) predicament in which one
  >knows the set of axioms to be recursive, but one does *not* have such an
  >algorithm?

   Let the set of axioms of the theory T consist of all true
sentences in the language of PA shorter than k symbols, for some
suitable choice of k. This is a recursively axiomatized theory which
decides your favorite open arithmetical problem, but is
epistemologically useless.