6) About "The integers are a fun example!". That is not a clear description of a system, while Rule 110 is. Are you referring to First Order Logic with Peano Axioms, that Godel used for his incompleteness theorem? Which actually proofs Turing Completeness, while that term was not invented yet?

5) You wrote "Now, over a decade later, no one knows a good undecidable problem about it." Undecidability is about a class of problems, not a single problem.

@VilleSalo 1) I think your comments are valuable for people that want to know more about this. 2). The original question did not ask about proofs, but about 'attractive'. I think Rule 110 because of its simplicity. 3) If something is Turin complete, then it means that you can simulate a Turing machine in it and that means you can encode a Turing Halting problem in it. 4) However, there I agree with you, then you have to translate the problem back to the orginal construction. I didn't do that properly.

@VilleSalo I don't see the problem. If you have any Turing Complete system, then you can make an undecidable problem out of it. For the initial state, I assume (but I didn't researched it), that it is finite. So, that at a certain point to the left and right you only have zeros.

@VilleSalo It is of course decidable what the state will be after n steps. The Wikipedia tells that it is 'Turing Complete'. This implies that it is undecidable whether a cell will flip eventually to 1 given a certain begin state (so, not knowing the number of steps).

Thanks, so, basically if you are creating a checker, you have two directions you can go. When introducing a function the user must provide a proof that it is well-defined, or enforce it by construction (which seems to be more standard). Still, in literature and student material, IMHO, don't propose functions in FOL at all, or also cover this aspect, but don't do half a job.

Thanks, I have that book, I will take a look.

For instance, if you define the remainder function, you can define it as predicate as follows: $R(x, y, z) = z < y \land \exists v: x = vy + z$ However, if you have FOL extended with functions, what is the normal notation to make that a function? That should only be allowed if the function is single-valued and total (otherwise, certain axioms are not valid).

No, that is quite obvious. My question is how do theorem checkers in general deal with this? So, I see suddenly a new function, but not defined in such way that it can de described in a formal language.