Hi Jacques, >I know that any machine or formal system has a Godel proposition which >express it own non-provability, and therefore is true but not provable if >the system is consistant. But shouldn't we consider that the machine really >know something with certainty only if it can prove it ?
As far as a certain kind of knowledge is concerned I agree. I use frequently the old definition of knowledge given by Platon in the Theetete : (to know p) is (to prove p AND p is true). With the godelian logic of provability, as you know, the consistent machine cannot prove that by proving p, p is true. So this definition is not trivial. It makes the knower not prouvably formalisable by the knower for exemple. But we know much more than we can prove in the sense that we can also make inference of p with p true. I think that a more general sort of knowledge is given by a mixture of these two types of knowledge, proof and inference. In particular a consistent machine cannot prove his own consistency, but nothing prevent it to infer it, or to bet on it. Like Helmholtz I think that part of our conscious perception are really produced by (unconscious, instinctive) inference processes. And this explains also why people confuse belief and knowledge in many situation. Scientific knowledge is typically of the inference type. >It seems clear to me that the physical laws are mathematical. >But do you want to derive only the physical laws of OUR universe ? Remember that by "mechanism" I mean the (personal) belief that you can survive a discrete (finite, digital) substitution of yourself, at some substitution level. With mechanism, I don't think there is something like a universe obeying physical laws, in which we inhabit. All computationnal histories exist embedded in the necessary relations between numbers. Some computationnal histories are very deep (in Bennett sense, see the book of LI & VITANYI recommended by Wei Dai), and relatively dense. For these histories there is a notion of mean point of view, where there are relatively different machines able to communicate classicaly about their most probable continuation. They can also discover "indeterminism" below their substitution level and other "physical things like that". But physical laws themselves are the result of the interference of many (a non denombrable set of) computationnal histories. The interference comes from our unabililty to make distinctions between some computationnal histories. Like James I like OCCAM's razor. That is why, at least when I am in a mechanist mood, I suspect there is no such thing we could call our universe nor could there been really objective physical laws. Bruno.
