Answer: not knownMany thanks to all who helped refine this question and the definitions associated to it.  The definitions of this wiki provided the starting point for the more recent TCS wiki Does P contain languages whose existence is independent of PA or ZFC? (TCS community wiki).  The more recent wiki is preferred because its definitions and nomenclature are substantially more sophisticated than those of this older wiki.  In particular, this older wiki's nomenclature incomprehensible $\Leftrightarrow$ comprehensible  languages and TMs is supplanted in the newer wiki by cryptic $\Leftrightarrow$ gnostic.  Aside from definitional details — which however are important — the two wikis address a similar class of questions.Further answers are welcomeFurther answers are welcome (needless to say), and it is likely that further definitional tuning is appropriate.  One main lesson has been that this class of questions is challenging to formulate and still more challenging to answer rigorously. As background, Sasho Nikolov's answer was rated  accepted, because it provided a formulation that captured the intent of the question: the answer to the question is (apparently) not known.  Philip White's valuable answer motivated the graded definition of TMs that are incomprehensible, versus strongly incomprehensible, versus canonically incomprehensible (per the list graded definitions of incomprehensibility below).The following statement of the question provisionally incorporates valuable insights and suggestions provided by Tsuyoshi Ito,  Marzio De Biasi, Huck Bennett, Ricky Demer, Peter Shor, and also a valuable weblog post by Luca Trevisan. Formal definitionIncomprehensible Turing machines are defined (within ZFC) as follows:D1  Given a Turing machine M that provably halts for all input strings, M is called incomprehensible iff the following statement is neither provable nor refutable for at least one positive semidefinite real number $r$:Statement: M's runtime is ${O}(n^r)$ with respect to input length $n$ Conversely, M is called comprehensible iff it is not incomprehensible.Disambiguating decidableThe Wikipedia entry Undecidable problem: Examples of undecidable statements concisely reviews the differing senses of the term undecidable that are customary in the proof-theoretic versus computability-theoretic literature.  With a view to avoiding ambiguity, the definitions and questions asked employ exclusively the terminology neither provable nor refutable.Further references in this regard are Jeremy Avigad's course notes Incompleteness via the Halting Problem, Scott Aaronson's weblog essay Rossers Theorem via Turing machines and Luca Trevisan's weblog post Two interesting questions. On the existence of incomprehensible Turing machinesThat incomprehensible Turing machines exist follows concretely from a construction by Emmanuele Viola and broadly from the complexity-theoretic framework of Juris Hartmanis.  In particular, Viola's construction provides, via the methods of Jeremy Avigad's course notes (as I understand them), the following lemma: Lemma [Viola's Implication]    (if a language L is accepted by a comprehensible TM) $\to$        (L is accepted by an incomprehensible TM).Respecting naturality in defining incomprehensibilityIt is natural to wonder whether the converse implication to Viola's Implication is true.  Considerations of naturality require that the converse implication be posed carefully, in that Philip White's comment below shows how to trivially reduce incomprehensible TMs to comprehensible TMs via polylimiters, which are computational modules that (in effect) pad the runtime of an incomprehensible machine so as to reduce it to a comprehensible machine. In particular, it is natural to require that we not “unaesthetically mask old elements of incomprehensibility by introducing new elements of incomprehensibility.” The key challenge associated to the question asked amounts to Does there exist a natural definition of incomprehensibility? … which (given the discussion here of TCS) we should perhaps regard as a nontrivial meta-question that may have more than one natural answer.With a view to this guiding naturality principle, graded definitions of incomprehensibility are specified as follows.Graded definitions of incomprehensibilityD2  We say that a Turing machine M is efficient iff it has a runtime exponent $r$ such that the language L that M accepts is accepted by no other TM having a runtime exponent smaller than $r$.D3  We say that a language L is incomprehensible iff it is accepted by (a) at least one Turing machine M is that is both efficient and incomprehensible, and moreover (b) there is no efficient and comprehensible TM that provably (in ZFC) accepts L.  D4  We say that an incomprehensible TM is strongly incomprehensible iff the language it accepts is incomprehensible.D5  We say that a strongly incomprehensible TM is canonically incomprehensible iff it is efficient.These definitions ensure that every incomprehensible language is accepted by at least one TM that is canonically incomprehensible, and moreover — in view of D3(a) and D3(b) — there exists no trivial polylimiter reduction of a canonically incomprehensible TM to a comprehensible TM that provably recognizes the same language.The three questions askedQ1  Does the complexity class P contain incomprehensible languages?Q2  Can at least one incomprehensible language be represented concretely? (if so, provide a constructive example).Q3  Can at least one canonically incomprehensible TM be represented concretely? (if so, provide a constructive example).MotivationThe incomprehensible properties of the complexity class P obstructs the understanding of a broad class of problems that (for the original proposer of this question) includes Terry Tao's Blue-Eyed Islanders Puzzle,  Dick Lipton and Ken Regan's Urn-Choice Game, and their hybridization in the context of Newcomb's Paradox via the Balanced Advantage Newcomb Game.  As Juris Hartmanis' monograph Feasible computations and provable complexity properties (1978) puts it:Results about the complexity of algorithms change quite radically if we consider only properties of computations which can be proven formally.The struggle to construct well-posed definitions and postulates that capture Hartmanis' insight helps us to a better appreciation that the complexity class P has some exceedingly peculiar languages in it, that are recognized by exceedingly peculiar Turing machines, whose properties we are (at present) very far from grasping.  It is striking that in a completely rigorous sense, it is not presently known whether the complexity class P is comprehensible.Many thanks are extended to all who have contributed comments and answers.
Does P contain incomprehensible languages? (TCS community wiki)
cc.complexity theory;complexity classes;turing machines;decidability
(I am retiring as no longer relevant the portion of the answer that just explained why there are no undecidable instances of a problem/no polytime algorithms with uncomputable time bound)Now the question has changed to a question about TMs whose running time is provable in some logical theory. For any (powerful enough) logical theory $T$, there exists a machine $M$ whose running time is polynomial but both the sentence the running time of $M$ is polynomial and its negation cannot be proved in $T$. In particular that means that there are polytime TMs whose running time bound cannot be proved in ZFC. This should follow from Viola's reduction with some additional tricks as in Scott's blog post. But rather than figure this out, look at the last comment by Luca in this blog post. In a way, Luca answers your question here. He shows that:there exists a polytime machine $M$ such that ZFC cannot prove that $M$ does not take exponential timefor any polytime machine $M$ there exists a machine $M'$ which decides the same language and whose running time is provably (in ZFC say) polynomial (the simple simulation that proves this was also offered by Peter Shor in a comment)So it seems that the answer to your question is no: any language decidable in polytime by some machine is decided by a provably polytime machine. But maybe your question should be:is there a polytime machine $M$ such that any machine $M'$ which decides the same language either cannot be proved (in ZFC) to decide the same language as $M$ or cannot be proved (in ZFC) to run in polynomial time.I suspect that the answer is yes, but right now I do not have any more time to devote to this.