Languages decidable by weak models of computation often have certain necessary characteristics, e.g. the pumping lemma for regular languages or the pumping lemma for context-free languages. Such characteristics are useful for determining when a language cannot be decided by that weak model of computation.
Do Turing-decidable languages have any such necessary characteristics? If not, why not?
Such a characteristic should avoid mention of Turing machines.
Motivation: The only way I know to show that a language is not Turing-decidable is diagonalization, or reducing to a language where diagonalization has already been applied. It would be nice to have another method.
I suspect that there aren't any nice characteristics of this type known, or they'd probably be very well-known; but an argument for why they can't exist could be illuminating.
I'd also be interested in the same question with the phrase "Turing-decidable" replaced with any complexity class, e.g. NP. This question seems more tractable (as there are fewer languages under examination).
Edit: Given the comments, I'll be a bit more precise about what I mean by "characteristics." I would be thrilled with either of the following two possibilities:
1) A property that allowed one to show a language was not in the relevant class (Turing-decidable, NP, whatever) without using diagonalization.
Or
2) A property that can be stated in a language too weak to define Turing machines.
Best Answer
As far as I know, the answer is no. We don't have an argument not based (directly or indirectly) on digonalization for even proving there is a language outside Dec (The set of Turing decidable languages).
Characterizing a class means having criteria for showing when a language is in the class and when a language is not. The second part would give us tools to prove lowerbounds on such classes.
For very small classes like $AC^0$ and $AC^0[p]$ there are combinatorial arguments (also for monotone-$AC^0$ circuits), but the current state of knowledge is consistent with $AC^0[6] = NP$. The Razbarov-Rudich (RR) Natural Proofs theorem is related to why the previous combinatorial arguments haven't been successful in separating larger classes. In simple terms, there is no "natural proof" for separating the larger classes unless there is no pseudo-random number generators (many believe they do exists), and all previous proofs were natural. Tim Gowers wrote a number of interesting blog posts on the topic: http://gowers.wordpress.com/2009/09/22/a-conversation-about-complexity-lower-bounds/
The reason that we have pumping lemmas for $Reg$ (regular languages) and $CFL$ (context-free languages) is that the machine models for them are very specific which gives the strings accepted by them special combinatorial structure. For classes defined by Turing machines this is not the case. If a complexity class contains some basic functions (say $AC^0$) and is closed under composition, proving lowerbounds for it becomes a rather difficult task. Note that $Reg$ does not contain $AC^0$ ($\{0^n1^n: n \in \omega \}$ is in $AC^0$ but not in $Reg$.)
EDIT:Comments
part 1. I don't have a theoretical justification right now, but the history of complexity theory shows that the structure of much smaller complexity classes are at least very difficult to understand. Many experts "believe" that there are pseudo-random number generators (PRNG), so RR's Natural Proof theorem applies and there is no "natural" property of sets/functions that can be used to prove a lowerbound for the complexity classes satisfying the condition of the RR theorem. I think a person accepting the existing of PRNGs can at least claim that there are no simple combinatorial structures for these complexity classes.
part 2. You are looking for a combinatorial property of sets of strings in a complexity class. The computational complexity of checking a property is a good measure. Any property stated in the first order logic (on a finite structure) is $AC^0$. The RR theorem applies to properties which are in $P$, i.e. can be checked in polynomial time given the truth table of the functions (characteristic functions of sets restricted to inputs of size n). Encoding Turing Machines (TM) is not difficult, and I think it can be done if one goes a little above $AC^0$, e.g. $TC^0$ is probably capable of checking if a string encodes a TM. You are looking for a property that holds for all functions in a class, but not for those outside it. The negation of it would be a property of the kind considered in RR's theorem. By these considerations, I think there are no properties of the kind you are looking for unless there are no PRNGs.
definitions:
$AC^0$ is class of sets of strings accepted by (uniform) circuits of polynomial size and bounded depth, i.e. there is a constant $d$ and a polynomial $p(n)$ and a sequence of circuits $\{C_n\}_{n \in \omega}$ using unbounded fan-in $\land$,$\lor$,$\lnot$ gates and of depth $d$ and size $p(n)$ that accepts them.
$AC^0[n]$ is the same as $AC^0$ but allows $mod_n$ gates. $p$ is a prime number.
$TC^0$ is the same as $AC^0$ but allows majority/threshold gates.
A property $Q$ is natural if it is:
useful: i.e. does not hold for simple functions (functions of low complexity) but holds for some function in the larger class,
constructive: i.e. can be checked in polytime from the truth table of the functions,
large: i.e. for some k and all large enough n, the property holds for at least $\frac{1}{n^k}$ of the functions.