Re: OMs are events

From: Hal Finney <hal.domain.name.hidden>
Date: Fri, 5 Aug 2005 13:53:45 -0700 (PDT)

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
Received on Fri Aug 05 2005 - 17:50:04 PDT