Answer: not known.
The questions asked are natural, open, and apparently difficult; the question now is a community wiki.
Overview
The question seeks to divide languages belonging to the complexity class $P$ — together with the decision Turing machines (TMs) that accept these languages — into two complementary subclasses:
- gnostic languages and TMs (that are feasible to validate/understand), versus
- cryptic languages and TMs (that are infeasible to validate/understand).
Definitions: gnostic vs cryptic numbers, TMs, and languages
Within the axiom frameworks PA and ZFC, we distinguish gnostic from cryptic Turing machines and languages as follows:
D0 We say that a computable real number $r$ is gnostic iff it is associated to a non-empty set of TMs, with each TM specified in PA as an explicit list of numbers comprising valid code upon a universal TM, such that for any accuracy $\epsilon\gt0$ supplied as an input, each TM provably (in ZFC) halts with an output number $o$ that provably (in ZFC) satisfies $r-\epsilon\lt o\lt r+\epsilon$.
Remark It is known that some computable reals are not gnostic (for a concrete example see Raphael Reitzig's answer to jkff's question "Are there non-constructive algorithm existence proofs?"). To avoid grappling with these computable-yet-awkward numbers, the restriction is imposed that runtime exponents be computable by TMs that are explicitly enumerated in PA (as contrasted with TMs implicitly specified in ZFC). For further discussion see the section Definitional considerations (below).
Now we seek definitions that capture the intuition that the complexity class $P$ includes a subset of cryptic languages to which no (gnostic) runtime exponent lower-bound can provably be assigned.
To look ahead, the concluding definition (D5) specifies the idea of a canonically cryptic decision TM, whose definition is crafted with a view toward obviating reductions that (trivially) mask cryptic computations by overlaying computationally superfluous epi-computations. The rationale and sources of this key definition are discussed later on — under the heading Definitional Considerations — and the contributions of comments by Timothy Chow, Peter Shor, Sasho Nikolov, and Luca Trevisan are gratefully acknowledged.
D1 Given a Turing machine M that halts for all input strings, M is called cryptic iff the following statement is neither provable nor refutable for at least one gnostic real number $r \ge 0$:
Statement: M's runtime is ${O}(n^r)$ with respect to input length $n$
Turing machines that are not cryptic we say are gnostic TMs.
D2 We say that a decision Turing machine M is efficient iff it has a gnostic runtime exponent $r$ such that the language L that M accepts is accepted by no other TM having a gnostic runtime exponent smaller than $r$.
D3 We say that a language L is cryptic iff it is accepted by (a) at least one Turing machine M is that is both efficient and cryptic, and moreover (b) no TM that is both efficient and gnostic provably accepts L.
To express D3 another way, a language is cryptic iff the TMs that accept that language most efficiently are themselves cryptic.
Languages that are not cryptic we say are gnostic languages.
D4 We say that a cryptic TM is strongly cryptic iff the language it accepts is cryptic.
D5 We say that a strongly cryptic TM is canonically cryptic iff it is efficient.
To express D5 another way, every cryptic language is accepted by a set of canonically cryptic decision TMs, which are the most efficient decision TMs that accept that language.
The questions asked
The following conjecture C0 is natural and (apparently) open:
C0 The complexity class P contains at least one cryptic language.
Three questions are asked, Q1–Q3, of which the first is:
Q1 Is the C0 conjecture independent of PA or ZFC?
Under the assumption that C0 is true — either provably in ZFC, or as an independent axiom that is supplemental to ZFC — two further questions are natural:
Q2 Can at least one cryptic language in P be presented concretely, that is, exhibited as a dictionary of explicit words in a finite alphabet that includes all words up to any specified length? If so, exhibit such a dictionary.
Q3 Can at least one canonically cryptic decision TM be presented concretely, that is, as an enabling description for building a physical Turing machine that decides (in polynomial time) all the words of the dictionary of Q2? If so, construct such a Turing machine and by computing with it, exhibit the cryptic language dictionary of Q2.
Definitional considerations
Definition D0 implies that every gnostic real number is computable, but it is known that some computable real numbers are not gnostic. For examples, see answers on MathOverflow by Michaël Cadilhac and Ryan Williams and on TCS StackExchange by Raphael Reitzig. More generally, definitions D0–D5 are crafted to exclude references to non-gnostic runtime exponents.
As discussed in the TCS wiki "Does P contain incomprehensible languages?," definitions D0–D5 ensure that every cryptic language is accepted by at least one TM that is canonically cryptic. (Note also that in the present question the word "cryptic" replaces the less descriptive word "incomprehensible" used in the wiki).
Moreover — in view of D3(a) and D3(b) — there exists no computationally trivial reduction of a canonically cryptic TM to a gnostic TM that provably recognizes the same language. In particular, D3(a) and D3(b) obstruct the polylimiter reduction strategies that were outlined in comments by Peter Shor, and by Sasho Nikolov, and independently by Luca Trevisan, and obstructs too the polynomially clocked reduction strategy of Timothy Chow, all of which similarly mask cryptic computations by overlaying a computationally superfluous epi-computation.
In general, the definitions of "gnostic" and "cryptic" are deliberately tuned so as to be robust with respect to mathematically trivial reductions (and it is entirely possible that further tuning of these definitions may be desirable).
Methodological considerations
Lance Fortnow's review "The status of the P versus NP problem" surveys methods for establishing the independence (or otherwise) of conjectures in complexity theory; particularly desired are suggestions as to how the methods that Lance reviews might help (or not) to answer Q1.
It is clear that many further questions are natural. E.g., the Hartmanis-Stearns Conjecture inspires us to ask "Do cryptic real-time multitape Turing machines exist? Is their existence (or not) independent of PA or ZFC?"
Zeilberger-type considerations
In the event that Q1 is answered by "yes", then oracles that decide membership in $P$ exist outside of PA or ZFC, and therefore, an essential element of modern complexity theory is (at present) not known to reside within any formal system of logic.
In this respect complexity theory stands apart from most mathematical disciplines, such that the apprehensions that Doron Zeilberger expresses in his recent "Opinion 125: Now that Alan Turing turned 100-years-old, it is time to have a Fresh Look at His Seminal Contributions, that did lots of Good But Also Lots of Harm" arguably are well-founded.
Zeilberger's concerns take explicit form as the criterion Z0 $\equiv $ ( !Q1 ) && ( !C0 ), which is equivalent to the following criterion:
Z0: Zeilberger's sensibility criterion Definitions of the complexity class P are called Zeilberger-sensible iff all languages in P are provably gnostic.
At present it is not known whether Stephen Cook's definition of the complexity class P is Zeilberger-sensible.
Motivational considerations
The definitions of "gnostic" and "cryptic" are crafted with a view toward (eventually) deciding conjectures like the following:
C1 Let $P'$ and $NP'$ be the gnostic restrictions of $P$ and $NP$ resp. Then $P' \ne NP'$ is either provable or refutable in PA or ZFC.
C2 $P' \ne NP'$ (as explicitly proved in PA or ZFC)
Clearly C2 $\to$ C1, and conversely it is conceivable that a proof of the (meta) theorem C1 might provide guidance toward a proof of the (stronger) theorem C2.
The overall motivation is the expectation/intuition/hope that for some well-tuned distinction between gnostic and cryptic TMs and languages, a proof of C1 and possibly even C2 might illuminate — and even have comparable practical implications to — a presumably far harder and deeper proof that $P\ne NP$.
Juris Hartmanis was among the first complexity theorists to seriously pursue this line of investigation; see Hartmanis' monograph Feasible Computations and Provable Complexity Properties (1978), for example.
Nomenclatural considerations
From the Oxford English Dictionary (OED) we have:
gnostic (adj) Relating to knowledge; cognitive; intellectual "They [the numbers] exist in a vital, gnostic, and speculative, but not in an operative manner."
cryptic (adj) Not immediately understandable; mysterious, enigmatic "Instead of plain Rules useful to Mankind, they [philosophers] obtrude cruptick and dark Sentences."
Apparently no Mathematical Review has previously used the word "gnostic" in any sense whatsoever. However, attention is drawn to Marcus Kracht’s recent article “Gnosis” (Journal of Philosophical Logic, MR2802332), which uses the OED sense.
Apparently no Mathematical Review has used the word "cryptic" — in its technical sense — with relation to complexity theory. However, attention is drawn to Charles H. Bennett's article "Logical Depth and Physical Complexity" (in The Universal Turing Machine: A Half-Century Survey, 1988) which contains the passage
Another kind of complexity associated with an object would be the difficulty, given the object, of finding a plausible hypothesis to explain it. Objects having this kind of complexity might be called "cryptic": to find a plausible origin for the object is like solving a cryptogram.
Considerations of naturality, openness, and difficulty
The naturality of these questions illustrates the thesis of Juris Hartmanis' monograph Feasible Computations and Provable Complexity Properties (1978) that:
"Results about the complexity of algorithms change quite radically if we consider only properties of computations which can be proven formally."
The openness and difficulty of these questions are broadly consonant with the conclusion of Lance Fortnow's review "The Status of the P Versus NP Problem" (2009) that:
"None of us truly understands the P versus NP problem, we have only begun to peel the layers around this increasingly complex question."
Wiki guidance
Particularly sought are definitional adjustments and proof strategies specifically relating to the questions Q1–Q3 and broadly illuminating the Hartmanis-type conjectures C1–C2.