've been reading up on formal systems and Gödel's incompleteness theorem, and I'm pretty sure I understand them both very well.
Something that has been bothering me though... It seems like it should be possible to create complete and consistent formal systems with an infinite number of axioms. It would, of course, be equivalent to the halting problem to enumerate the first n axioms of such a system, since we would define axiom n as the first statement (given by some arbitrary "alphabetical" order, the definition of which would also define the system) which cannot be proved nor disproved given the first n-1 axioms.
Indeed, we couldn't program a computer to use this system, but... What could we learn from considering such a system?
Or more practically, what could we learn from systems that are complete and consistent "locally" (for lack of a better term)? i.e. formal systems which only allow a limited number of inferences? (In this case, there are well-defined procedures to determine if a given statement is a theorem) Do non-trivial systems of this type even exist?
If anyone knows of literature on these kinds of systems (or e.g. a name for them for me to put into Google), I would love to know about it