Le 06-août-05, à 00:19, Aditya Varun Chadha a écrit :
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)
G and G* do not really depend on the logical order of the
theory/machine concerned, as far as the proofs given by the machine are
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!
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).
I would say "reachability" = "halting".
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.
I will come back on this. Meanwhile you can read my posts:
or better my paper available here:
It gives a description of Solovay's theorem which makes the link
between the modal logic G and G* and the Godel Lob incompleteness