Bruno writes: > Now an important fact is the following: computations themselves can be > seen as proofs.
I have often seen this stated, but I'm not sure I have ever actually seen the construction. I could imagine turning a TM computation into a proof in the following way. There would be one axiom, which is the initial configuration of the TM: its initial tape, its head position, and its head state. Then the state transition table of the TM would correspond to rules of inference such that only one would apply at each state. Then starting with our one axiom, we go through successive lines of the proof, applying the single applicable rule of inference at each line, which exactly corresponds to what the TM would do at each state. > But with Church thesis, the notion of computation is > absolute: it does not depend on the formal system chosen (java = C = > turing = quantum computer = ...). So... a computation in one of these frameworks can be transformed into an equivalent computation in any other. > But provability is a relative notion > (like the notion of *total* (everywhere defined) computable functions. So in the case of the TM computation a theorem that is "provable" given the axioms and rules of inference would be a state that is "reachable" from the corresponding initial state and transition table. The question of whether a given theorem is "provable" is equivalent to asking whether a given computational state is ever reached. And of course that depends on precisely what computation is being done: on the specific program and data which are running. > To say "A is proved" has no meaning, you should always say: A is proved > in this or that theory (or by this or that machine). Right, if someone asked, does a program ever reach a state where x = 0? Then we must respond, which program? It is a meaningless question to ask unless we specify what program is running. That would be the corresponding statement, in computational terms. > Of course > provability can obey universal principles: for example the notion of > classical checkable proof in sufficiently rich system is completely > captured by the modal logics G and G*. Well, you lost me on that one! Hal Finney
