4 Now a TCS StackExchange question, per Colin Tan's request

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?"

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 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 eﬀorts 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?".

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.

3 Respose to Colin Tan

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 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 eﬀorts 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?".

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.

2 Reordered the paragraphs ... main paragraph now first.; deleted 9 characters in body

Section 1.5.2 of Sanjeev Arora and Boaz Barak's well-respected textbook Computational Complexity:

That a Modern Approach is titled mathematical idea be "Criticisms of P and some eﬀorts to address themclearly defined" .

I have often wished is itself an idea that Arora and Barak had written perhaps could be more on this theme, and in particular, that clearly defined ... one candidate for a subsection was included having the title "What notions of P are not decidable in modern mathematics?"

Here the common-sense point is that is more rigorous to proveassertion is that a widespread mathematical intuition is "undecidable" than to assert that it is "not clearly defined." 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 that 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 widely used commonly embraced and/or have proved to be broadly useful, but nonetheless are formally undecidable, in modern mathematics?"
As a One specific example , I have in that comes to mind is Emanuele 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 eﬀorts 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?"