Section 1.5.2 of Sanjeev Arora and Boaz Barak's well-respected textbook <i>Computational Complexity: a Modern Approach</i> is titled <i>"Criticisms of P and some efforts to address them"</i>.  

I have often wished that Arora and Barak had written more on this theme, and in particular, that a subsection was included having the title "What&nbsp;notions of P are not <i>decidable</i> in modern mathematics?" 

Here the common-sense point is that is more rigorous to <i>prove</i> that a widespread mathematical intuition is "undecidable" than to <i>assert</i> that it is "not clearly defined."  Moreover, widespread intuitions that are proved to be undecidable have an illustrious history in mathematics.

These reflections lead to the suggestion that this community wiki's question would be better-posed (and might perhaps be more useful) if it were amended to read:<blockquote>"What intuitions are widely used and/or have proved to be broadly useful, but nonetheless are formally <i>undecidable</i>, in modern mathematics?"</blockquote>As a  specific example, I have in mind [Emanuele Viola's theorem][1], with its implication that the set of Turing machines {M} associated to P has no decidable runtime ordering ... Viola's proof of undecidability was eye-opening to me, and it has filled the valuable role of leading me to wonder "What else is out there?"

No doubt many more examples of "undecidable intuitions of modern mathematics" could be posted, and it would be great fun to read other people's examples. However, it seems inappropriate to amend the topic of a community wiki in such a fundamental respect, and so I am posting this amended question as a suggested general "answer" instead.

[1]:http://cstheory.stackexchange.com/questions/5004/are-runtime-bounds-in-p-decidable-answer-no