>> There is a good reason for that which is that FOL + arithmetic is undecidable for reasons Kurt Godel discovered. Undecidability is overrated. We have comput

>> There is a good reason for that which is that FOL + arithmetic is undecidable for reasons Kurt Godel discovered. Undecidability is overrated. We have computers, no? Particularly for FOL undecidability does not mean that every FOL formula is undecidable, it just means that there exist some formulae which are undecidable. There may even be an infinite number of undecidable formulae ... and an infinite number of decidable ones, too. If you think about it, Gödel's proof was the construction of one undecidable formula ("this sentence is false"). His proof followed multiple similar proofs in different contexts all proposed around the same time, in the early 1920's, for example Russel's paradox and all more or less variations of one of Epimeneide's paradox. I don't know if anyone has since produced any more instances of undecidable problems in FOL. If there were an infinity of such undecidable problems (or classes of problems) wouldn't we have stumbled on them a lot more often? Anyway the simple solution to do arithmetic in FOL-based languages is well-known to the logic programming community: constraint logic programming (an idea which I recently learned also came from Alain Colmerauer, creator of Prolog): https://en.wikipedia.org/wiki/Constraint_logic_programming https://en.wikipedia.org/wiki/Constraint_logic_programming https://www.swi-prolog.org/pldoc/man?section=clpfd-arith-constraints https://www.swi-prolog.org/pldoc/man?section=clpfd-arith-con...