undecidability – Are there undecidable languages which are well defined?

It would be a mess if the answer had to be NO after all these speculations and theorems about these languages but..

I am not conviced liar paradox is well defined. And Godël himself said his theorem is just an exhibit of a liar paradox.

I am not conviced halting problem is well defined.

I am pretty conviced that if you formalize the statement ‘Does this man both having only 2 ears and 3 ears went to his house on monday ?’ you get something that you can not prove true nor false, just because it would suppose to define something in the proof which can not be defined.

I am not conviced that any ‘undecidable’ Godel statement is undecidable in an other meaning than this.

I am pretty conviced than you can not correctly define any consistent theory that would not be decidable by a turing machine. I think this is the profond meaning of Church Thesis.

I am pretty conviced that if you take a statement which would be undecidable even for a turing machine, if you add this statement as axiom to any turing complete theory, you get something inconsistent because I am pretty conviced than you can proof both the statement and it’s unprovability.

I am not sure that the separation of syntax and semantic is relevant anywhere in theoretical computer science, yes you can specify what you are doing and it can help in some application, but I am pretty conviced you do not need this do define mathematics.