In response to Colin Tan's request (below), I have posted these remarks as the TCS StackExchange question "Do the undecidable attributes of P pose an obstruction to deciding P versus NP?Do the undecidable attributes of P pose an obstruction to deciding P versus NP?"
That a mathematical idea be "clearly defined" is itself an idea that perhaps could be more clearly defined ... one candidate for a more rigorous assertion is that a mathematical intuition be formally decidable. Moreover, widespread intuitions that are eventually proved to be decidable versus undecidable have an illustrious history in mathematics.
These reflections lead to the suggestion this community wiki's question would be better-posed mathematically (and might perhaps be more useful too) if it were amended to read:
"What intuitions are commonly embraced and/or have proved to be broadly useful, but nonetheless are formally undecidable, in modern mathematics?"One specific example that comes to mind is Emanuele Viola's theoremEmanuele Viola's theorem, 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?"
To show the utility of these reflections, Section 1.5.2 of Sanjeev Arora and Boaz Barak's well-respected textbook Computational Complexity: a Modern Approach is titled "Criticisms of P and some efforts to address them". I have often wished that Arora and Barak had written more on this theme. With the help of Viola theorem, this wich becomes specific and rigorous: a section titled "What properties of P are not decidable in modern mathematics?"
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.
Partially in response to Colin Tan's request (in the comments below), I have posted on TCS StackExchange the specific question "What is the proper role of verification in quantum sampling, simulation, and extended-Church-Turing (E-C-T) testing?What is the proper role of verification in quantum sampling, simulation, and extended-Church-Turing (E-C-T) testing?".
More broadly, on Lance Fortnow's weblog, under the topic "75 Years of Computer Science", the question is raised
"Do there exist languages $L$ that are recognized solely by those Turing machines in $P$ whose runtime exponents are undecidable? Can examples of these machines and languages be finitely constructed?"
... but I am not (yet) prepared to post this as a MathOverflow and/or TCS StackExchange question. Thanks and appreciation are extended to Colin.
