On Thu, Feb 13, 2014 at 10:42:21AM +0100, Bruno Marchal wrote: > > On 13 Feb 2014, at 05:38, Russell Standish wrote: > > >On Wed, Feb 12, 2014 at 12:24:18PM +0100, Bruno Marchal wrote: > >> > >>On 12 Feb 2014, at 02:02, Russell Standish wrote: > >> > >>>On Tue, Feb 11, 2014 at 07:31:24PM +0100, Bruno Marchal wrote: > >>>> > >>>>You are right, the qualia are in X1* \ X1, like we get quanta in > >>>>S4Grz1, Z1*, X1*. > >>> > >>>The only thing you can say is that qualia ought to obey the > >>>axioms of > >>>X1*\X1, (and even that supposes that Z captures all observations, > >>>which I think is debatable), > >> > >>By UDA, "p" to refer to a "physical certainty" needs to > >> > >>1) UD generated (= sigma_1 arithmetical and true). > >>2) provable (true in all consistent extensions) > >>3) and non "trivially" provable (= there must be at least one > >>consistent extension) > >> > >>This give the []p & <>t, with p sigma_1. > >> > >>So the logic of observable certainty should be given by the Z1* > >>logic. > >> > >> > > > >This is certainly an interesting understanding that I hadn't met in > >your writings before. > > You worry me a bit, as I think this is explained in all papers and > the thesis. I know that I am concise. > Normally, if everything get clear, you should see that this is what > I am explaining everywhere. >
Indeed this doesn't come out with your Lille thesis. There is almost no connection between Chapter 5 and the previous 4 chapters of the thesis. This doesn't bother me - if you ever bothered to read my thesis (not that I'm recommending you do so), you would find it consists of two faily different topics, with only the most tenuous connection between them. This was because it actually was two different topics with two different supervisors. I was actually lightly chided by one of the thesis reviewers for attempting to draw out the connection between the topics :). I had a look at your SANE paper, which is the main paper where you describe your work that you published since your thesis. I can sort of see you saying something a bit like the above on page 11 "Now DU [sic - should be UD in English] is emulated platonistically by the verifiable propositions of arithmetic. They are equivalent to sentences of the form ``if exists n such that P(n)'' with P(n) decidable." That is actually rather confusing. Obviously a UD executes all proofs of all true Sigma 1 sentences, but I think what you are trying to say that all programs executed by the UD correspond to a proof of some true Sigma 1 sentence. Is that obvious? I didn't get that when I read the SANE paper originally, only got it in context of your statements above. > > > > >In associating provable with "true in all consistent extensions", > > In case of "provable", this is Gödel COMPLEteness result (not > incompleteness!). > In case of an abstract box, in a modal logic having a Kripke > semantics, this is just the semantics of Kripke. > > > > > >are > >you meaning that so long as something (ie proposition) is computed by > >all programs instantiating your current state, no matter how far in > >the future that calculation might require, then that something is > >(sigma_1) provable. > > I am not sure. "true in all consistent extensions" is a very general > notion. > It is your term. I take it to mean all programs compatible with your current state, your current here-and-now. > What happens is that, in arithmetic, the sigma_1 sentences, when > true, are provable (already by RA). > > So they verify the formula A -> []A. (called TRIV for trivial, as > that sentence makes many modal logic collapsing, but not so in the > provability logic, not even in the 1p S4Grz). Yes - thanks for reminding me. > > In fact a machine is Turing universal iff for all sigma_1 sentences > A we have A -> []A. So "A -> []A" is the Turing universality axiom, > when A is put for any sigma_1 sentence. Where []A means provable by the machine in question, I take it. > > G1 is G + A->[]A. Visser proved an equivalent of Solovay theorem for > G1 and G1*. You can find it in Boolos 1993. > > It is a way to restrict the logic of the different points of view on > the UD*. "To be a finite piece of computation" is itself given by a > sigma_1 formula, and the sigma-1 sentences model computations. > > > > > > > >Then 1&2 gives your hypostase for knowledge, ie S4Grz1. > > Only G1 at that stage. To get knowledge, you need to do 1 and 2, but > on []p & p, But p statisfying 1&2 => p&[]p, so why is this G1 and not S4Grz1? Perhaps you mean p satisfying p->[]p (-p v p&[]p), which can be added to G (Visser's move). > like to get observation/probability/expectation, you > need to do 1 and 2, but on (3) []p & <>t. > And to get sensible observation, you can mix knowledge ( " & p"), > and "consistency" <>t. Yes - I still don't get that - either in the full or Sigma_1 restricted sense. Where the penny dropped, if only slightly, was that the existence of a universal dovetailer entails comp immortality, which entails the no cul-de-sac conjecture, which can be written as []p&<>t restricted to sigma_1. But is this the approach you are taking? I always felt that the AUDA stood apart from the UDA. > Incompleteness makes all those views obeying to different logic. > > > > >It is, of > >course the sigma_1 restriction of Theatetus's definition of knowledge, > >which both Brent & I share quibbles with, but accept for the "sake of > >the argument". > > Since Plato, many philosophers quibble on Theaetetus' definition. > The fist quibbler being Socrate, who refuted it. > The magic things happening with comp, is that Socrate's refutation > does no more apply, How so? Because comp => p->[]p ? Actually seeing the equivalence between executed programs and proofs of sigma_1 sentences probably alleviates my quibble, but I need to think it over some more. > and the only argument against it which remains, > is the argument put forward by people who believe that they can > distinguish, immediately in the 1p view, simulations or dreams from > reality. But this we have already abandoned when we accept an > artificial brain (like in step 6). > I can't even see the relevance. How is that quibble supposed to work? > > > > > >But assuming 3) above is equivalent to assuming the no cul-de-sac > >conjecture by fiat. > > The beauty is that incompleteness makes sense of that move. In most > modal logic []p -> <>t. > > > > > > >I don't feel comfortable in assuming that axiomatically - I was hoping > >for a proof, or even just a better justification for that. > > I am not sure what that would mean. Here the proofs is that the move > need to get a probability notion from a provability notion makes > genuine new sense thanks to incompleteness. > When we predict P(head) = 1/2, we also, but *implicitly*, assume <>t > by fiat. Incompleteness gives the opportunity to see that making it > explicit does change the logic, and that is why observation will > obeys to a different logic than knowledge, and that is exactly what > we need to get physics and knowledge, and belief, ... from the same > arithmetical reality accessible by a machine. > I think I see that. I pretty much do the same thing in getting equation (D.5) of my book, which in words states that the probability for getting a result of an observation (any result) is 1. A cul-de-sac state would be one for which no result is obtained from performing a measurement. I can see that would completely mess up quantum mechanics (and for that matter probability theory, which assumes the probability of the certain event is 1). > A rumor, alluded in the book by Franzen (on the abuse of Gödel!), is > that I define probability by provability, but of course, that is not > the case. Knowledge and probability are intensional nuance of > provability, not provability itself. > > Best, > > Bruno > > > http://iridia.ulb.ac.be/~marchal/ > > > > -- > You received this message because you are subscribed to the Google Groups > "Everything List" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to [email protected]. > To post to this group, send email to [email protected]. > Visit this group at http://groups.google.com/group/everything-list. > For more options, visit https://groups.google.com/groups/opt_out. -- ---------------------------------------------------------------------------- Prof Russell Standish Phone 0425 253119 (mobile) Principal, High Performance Coders Visiting Professor of Mathematics [email protected] University of New South Wales http://www.hpcoders.com.au ---------------------------------------------------------------------------- -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
