Not sure of the exact formal meaning but I think Bruno is talking
something related to Godel's incompleteness for second order and
"higher" logics. (sorry if that was already obvious)
> > 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
I'd guess that this can be translated into the computability problem
(problems of the class of HALTING) for the Universal TM. i.e.
"Reachability" in ANY Turing Machine is limited to "sub-HALTING"
problems (very very vague and informal on my part).
The church turing thesis also is infact a statement about
computability in the universal sense, independant of the model of
Or maybe I am totally off, in that case, sorry for blabbering without
reading up what "modal logics G and G*" exactly are.
Aditya Varun Chadha
adichad AT gmail.com