(1) Given a recursively axiomatizable theory with finitely many axioms, and with 'length of proof' defined as the sum of the lengths of the formulas that are the lines in the proof, is there an algorithm to determine. for any given theorem, the least length of a proof?
(2) Given a recursively axiomatizable theory with infinitely many axioms, and with 'length of proof' defined as the sum of the lengths of the formulas that are the lines in the proof, is there an algorithm to determine, for any given theorem, the least length of a proof?
(3) Given a recursively axiomatizable theory with finitely many axioms, and with 'length of proof' defined as the number of lines in the proof, is there an algorithm to determine, for any given theorem, the least length of a proof?
(4) Given a recursively axiomatizable theory with infinitely many axioms, and with 'length of proof' defined as the number of lines in the proof, is there an algorithm to determine, for any given theorem, the least length of a proof?