The Church-Turing thesis states that the computation ability of Turing machine is stronger or equal to any "computability model" (whatever that means) we can come up with. Are we able to find some property, satisfied by Turing machine, and any other "computability model" satisfying the property, is Turing complete?
In summary, what I'm hoping for is:
- Some suitable definition of a computability model (which should include Turing machine);
- A property of computability models;
- A proof that Turing machine satisfies this property;
- A proof that any computability model satisfying this property is Turing complete.
A possible answer could be partial combinatory algebra. It seems that any pas that is combinatory complete can (roughly) express the untyped $\lambda$-calculus, thus Turing complete, but I'm not very sure.
If you read Turing's paper, you'll find that Turing tried to figure out a way to capture any kind of computation ... and this is what led him to the notion of what we now call the Turing-machine. And if you read his paper and reflect on it, you'll find that it is indeed quite plausible that any computation would be reducable to Turing-computation. But can we prove it? No. You would be trying to prove that this mathematical definition of a Turing-machine does capture out intuitive concept of computation ... and that is just not mathematically provable.
It's like Cantor's notion of cardinality. We can't prove that cardinality is the correct way to think about the 'sizes' of infinite sets and how to compare their relative sizes ... but it sure turns out to be a very useful definition.