Hi Russell, > I spent a while poring over Bruno's thesis, and borrowed >Boolos from a local university library to udnerstand more what it was >about. I didn't go into too great a length into the results and >structure of Modal logic, although I gained an appreciation, and an >understanding of the symbology. > >However, my main problem with Bruno's work lay not in the technical >details of Model logic, rather with the phrases of the ilk "We >modelise knowledge by Bew(|p|)". I can appreciate its only a model, >but why should I believe that model of knowing has any connection with >reality? I'm afraid none of the Booloses, nor Bruno's posting helped >me with this.
I am glad you borrowed Booloses from a library and that you spent a while poring over my thesis. I want just made precise that I have never try to modelise knowledge by Bew(|p|). This is, actually, a rather sensible point. Most philosopher agree that S4 is a good *axiomatic* of knowledge. Precisely S4 is KT4 + MP,NEC or, explicitely (added to the Hilbert Ackerman axioms) : AXIOMS [](A -> B) -> ([]A ->[]B) K []A -> A T []A -> [][]B 4 RULES A/[]A (A & (A->B)) / B NEC MP. That is, most philosopher (since Plato, but I remember having seen a Buddhist similar writing) agree that: -if A->B is knowable and if A is knowable, then B is knowable. (K) - if A is knowable then A is true. (T) - if A is knowable than that very fact (that A is knowable) is knowable (4) Would you agree with that? 4 makes that knowledge somehow introspective. Now we will see that if []A represent the formal provability of A, or (provability by a sound machine), i.e. Bew(|A|), although 4 and K are verified, we don't have T, that is, we don't have []A -> A provable for all sentence A. Bew(|A|) -> A is not always provable. This entails that formal provability cannot and should not be used for the formalisation of knowledge. You can guess the reason. Consider []FALSE -> FALSE, this is equivalent to -[]FALSE which is the statement of (self-) consistency (by the machine or the formal system), that is <>TRUE, which by Godel's second theorem is NOT provable (by the sound machine). But then, how to formalize knowledge ? When Socrate asked Thaetetus what is "knowledge of p", Thaetetus replied "justification of p". But then Socrate argues that a justification of p can be wrong. Thaetetus proposed then to define knowledge by justification of p *and* truth of p, by definition ! We will see that it is impossible to define "truth of p" in the language of the machine (Tarski theorem), but still we can define knowledge of p (for the machine) by Bew(|p|) *and* p If we define KNOW(A) by []A & A, then the modal "KNOW" obeys S4, that is KNOW(A -> B) ->(KNOW A -> KNOW B), (KNOW A) -> A, etc. (see above). To sum up: I never modelized knowledge of p by Bew(|p|), but I will indeed define knowledge of p (in the language of the machine) by Bew(|p|) & p. How come? Is not Bew(|p|), for the sound machine, trivially equivalent with Bew(|p|) & p ? Yes. But the point is that the sound machine neither can "bew" it, nor "know" it! We will see how precisely the epistemological nuance between Bew(|p|) & p and Bew(|p|) are made necessary by the incompleteness phenomenon. All this will be made transparent with the modal logic G and G* and their arithmetical interpretations. The atomic sentences are interpreted by arithmetical sentences. >I can appreciate its only a model, >but why should I believe that model of knowing has any connection with >reality? I'm afraid none of the Booloses, nor Bruno's posting helped >me with this. The connection with the reality, as you see, is done in the most platonist superb manner, I just add it by definition. Nuancing Bew(|p|) by Bew(|p|) & "truth"(of p). Well, later I will propose another nuancing of Bew(|p|), more appropriate for "measuring probability one" on possible "consistent extension"). Bew(|p|) is nuanced by Bew(|p|) & consistency of p. (a necessary step by UDA actually). The embedding in UD* will be "translated" in the language of the machine by restricting the arithmetical interpretation of p. And to get George's prize I will still need to extract LASE (the little abstract schroedinger equation) from that embedding. And of course i will need to make clear the relationship between LASE and the quantum histories. Bruno