[FOM] Finite axiomatisation

[Bill Taylor]

-> Is there a mathematically robust way of recovering a finite 
-> set of axioms from the finite engine?  The kind of thing i have in mind is 
-> a proof due i think to Bill Craig (I have no idea where i learned it) that
-> if T has a r.e. axiomatisation then it has a recursive axiomatisation.
-> The proof is purely syntactic. 

Also, there is some independent interest, I would think, in knowing
the shortest, or close to the shortest, finite axiomatisation of PA.

Does anyone have any ideas on how it would look?  Does anyone want to try it?

-- Bill Taylor