3 ms·
There are two more options: (3) The system's axioms are not finitely enumerable (i.e. not finite, and cannot be generated by a generator of finite length; e.g.
by joshuaissac 4y ago
There are two more options:
(3) The system's axioms are not finitely enumerable (i.e. not finite, and cannot be generated by a generator of finite length; e.g. a system where every true statement is an axiom and there are infinitely many axioms)
(4) The system is not complex enough to express arithmetic (e.g. propositional calculus)
- bumbledraven 4y agoGood point. For (3), I should have said something about the axioms being computable. I think I already excluded cases like (4) by stating that the checker operates on "arithmetical statement[s]".
- Tainnor 4y ago> I think I already excluded cases like (4) by stating that the checker operates on "arithmetical statement[s]". It's at least a bit vague, I think you need something that is at least as strong as Robinson arithmetic. In particular, I believe that if you throw out multiplication (or addition, and keep multiplication), you get a complete theory.