That works for finitely axiomatized theories. If you have axiom schemas as in standard ZF(C) or PA then there is no small set of well defined moves.
The axiom schemas are countable, which is small enough for the procedure described in the grandparent to work. Unless I’m not understanding something?
The size of the search space and lack of any reasonable heuristic.
That works for finitely axiomatized theories. If you have axiom schemas as in standard ZF(C) or PA then there is no small set of well defined moves.
The axiom schemas are countable, which is small enough for the procedure described in the grandparent to work. Unless I’m not understanding something?
The size of the search space and lack of any reasonable heuristic.