Re: A Program to Compute Gödel-Löb Fixpoints

2019-03-05 Thread Bruno Marchal

> On 2 Mar 2019, at 14:19, Lawrence Crowell  
> wrote:
> 
> I guess I am not sure what a Gödel-Löb fixed point is. Is this somehow 
> analogous to a Brouwer fixed points in maps or diffeomorphisms of spaces?


There are some analogies, some of which can be made technically precise, but 
that requires sophisticated semantics for the variant of probability.

The fixed point theorem in provability logic is that self-reference have fixed 
point, like with the diagonalisation lemma.

By the diagonalisation lemma, you can find sentence asserting anything 
computable about them, and you can eliminate the self-reference. For example, 
you can find p such that PA proves p <-> []p, that gives the Löbian fixed point 
t, and PA will prove it, PA will prove p <-> t. 
Similarly PA can prove, for some p, that p <-> ~[]p, that gives the famous 
Gödel sentences, and PA will prove that p is equivalent, in this case, to <>t 
(= ~[]f = consistency).
There are many others, and even if they involved other sentences, it is always 
possible to eliminate the self-reference.
Three different proofs are given in Boolos 1993. It is a very important result 
in the provability logic, aka machine theology (to be sure the theology is G*, 
the true extension of the provability logic G, coming from Solovay second 
completeness theorem, which generalises a lot the incompleteness theorem. 
Indeed all the true propositional modal truth are axiomatised by G*, also known 
as GLS (Gödel-Löb-Solovay) in the literature.



> 
> I read Rucker's Infinity and the Mind last spring, after having read it many 
> years ago. I could tell he had a penchant for various mystical ideas. This 
> tends blog entry of his suggests he has ideas similar to what Gödel thought, 
> and which I think were a part of leading  him into paranoid delusions. When I 
> clicked on this for some reason I thought this was about monoids, and was a 
> bit disappointed to see it is more philosophical. However, I think the Kant 
> noumena is not really directly knowable, and I think from quantum mechanics 
> we can't know this as either purely epistemic or ontic. I am not sure how 
> ideas of mind fit into this.

With mechanism, it fits remarkably. Indeed it makes physics a branch of 
machine’s theology. See my papers for all details, or my posts here. Physics 
can be sued to refute that theology, but we get only confirmation up to now. 
The physicalist theory of mind requires endowing matter with some magics, for 
which no evidence exist.

Bruno



> 
> LC
> 
> On Saturday, March 2, 2019 at 3:26:18 AM UTC-6, Philip Thrift wrote:
> 
> 
> A Program to Compute Gödel-Löb Fixpoints
> Melvin Fitting [ http://melvinfitting.org/ <http://melvinfitting.org/> ]
> 
> https://www.researchgate.net/publication/285841645_A_program_to_compute_Godel-Lob_fixpoints
>  
> <https://www.google.com/url?q=https%3A%2F%2Fwww.researchgate.net%2Fpublication%2F285841645_A_program_to_compute_Godel-Lob_fixpoints=D=1=AFQjCNFQ4ORDwOhT81xzkzLgV9unsTybRg>
> 
> 
> A loose motivation for much of Melvin Fitting's work can be formulated 
> succinctly as follows. There are many logics. Our principles of reasoning 
> vary with context and subject matter. Multiplicity is one of the glories of 
> modern formal logic. The common thread tying logics together is a concern for 
> what can be said (syntax), what that means (semantics), and relationships 
> between the two. A philosophical position that can be embodied in a formal 
> logic has been shown to be coherent, not correct. Logic is a tool, not a 
> master, but it is an enjoyable tool to use.
> [ https://en.wikipedia.org/wiki/Melvin_Fitting 
> <https://en.wikipedia.org/wiki/Melvin_Fitting> ]
> 
> 
> also (a bit offbeat):
> 
> “Simply Gödel,” Phenomenology, and Monads
> Rudy Rucker
> http://www.rudyrucker.com/blog/2017/03/17/godel-phenomonology-and-monads/ 
> <http://www.rudyrucker.com/blog/2017/03/17/godel-phenomonology-and-monads/>
> 
> - pt
> 
> -- 
> 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 everything-list+unsubscr...@googlegroups.com 
> <mailto:everything-list+unsubscr...@googlegroups.com>.
> To post to this group, send email to everything-list@googlegroups.com 
> <mailto:everything-list@googlegroups.com>.
> Visit this group at https://groups.google.com/group/everything-list 
> <https://groups.google.com/group/everything-list>.
> For more options, visit https://groups.google.com/d/optout 
> <https://groups.google.com/d/optout>.

-- 
You received this message because you are subscribed to the Google Groups 
"Everything List" group.
To unsubscribe 

Re: A Program to Compute Gödel-Löb Fixpoints

2019-03-03 Thread Bruno Marchal

> On 2 Mar 2019, at 10:26, Philip Thrift  wrote:
> 
> 
> 
> A Program to Compute Gödel-Löb Fixpoints
> Melvin Fitting [ http://melvinfitting.org/ ]
> 
> https://www.researchgate.net/publication/285841645_A_program_to_compute_Godel-Lob_fixpoints
> 
> 
> A loose motivation for much of Melvin Fitting's work can be formulated 
> succinctly as follows. There are many logics. Our principles of reasoning 
> vary with context and subject matter. Multiplicity is one of the glories of 
> modern formal logic. The common thread tying logics together is a concern for 
> what can be said (syntax), what that means (semantics), and relationships 
> between the two. A philosophical position that can be embodied in a formal 
> logic has been shown to be coherent, not correct. Logic is a tool, not a 
> master, but it is an enjoyable tool to use.
> [ https://en.wikipedia.org/wiki/Melvin_Fitting ]
> 
> 
> also (a bit offbeat):
> 
> “Simply Gödel,” Phenomenology, and Monads
> Rudy Rucker
> http://www.rudyrucker.com/blog/2017/03/17/godel-phenomonology-and-monads/


I like very much Rudy Ricker. Both Smullyan and Franzen have been a bit unfair 
in their critics, and not quite rigorous.

Fitting is also very good, in modal logic, notably. He wrote very good books. 
He was a main student of Smullyan.

Note that you can find an algorithm to compute Löbian fixed point in Boolos 
1979, and I used it a lot, in the interview of the universal machine. I 
implemented in Lisp, a Lon time ago. Will read Fitting’s paper asap …

Bruno




> 
> - pt
> 
> -- 
> 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 everything-list+unsubscr...@googlegroups.com 
> <mailto:everything-list+unsubscr...@googlegroups.com>.
> To post to this group, send email to everything-list@googlegroups.com 
> <mailto:everything-list@googlegroups.com>.
> Visit this group at https://groups.google.com/group/everything-list 
> <https://groups.google.com/group/everything-list>.
> For more options, visit https://groups.google.com/d/optout 
> <https://groups.google.com/d/optout>.

-- 
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.


Re: A Program to Compute Gödel-Löb Fixpoints

2019-03-02 Thread Philip Thrift


"Fixed point" here is a term in the subject of provability logic (PL):

   https://plato.stanford.edu/entries/logic-provability/#FixePoinTheo

How this relates to a Brouwer fixed point  - * how does provability logic 
relate to topology*  - is a subject that is interesting but is outside what 
I know about.

Fixed points, monads, monoids, all arise in PL and PLT. So what do they 
have to do with qualia of experience?  TBD.

- pt


On Saturday, March 2, 2019 at 7:19:01 AM UTC-6, Lawrence Crowell wrote:
>
> I guess I am not sure what a Gödel-Löb fixed point is. Is this somehow 
> analogous to a Brouwer fixed points in maps or diffeomorphisms of spaces?
>
> I read Rucker's *Infinity and the Mind* last spring, after having read it 
> many years ago. I could tell he had a penchant for various mystical ideas. 
> This tends blog entry of his suggests he has ideas similar to what Gödel 
> thought, and which I think were a part of leading  him into paranoid 
> delusions. When I clicked on this for some reason I thought this was about 
> monoids, and was a bit disappointed to see it is more philosophical. 
> However, I think the Kant noumena is not really directly knowable, and I 
> think from quantum mechanics we can't know this as either purely epistemic 
> or ontic. I am not sure how ideas of mind fit into this.
>
> LC
>
> On Saturday, March 2, 2019 at 3:26:18 AM UTC-6, Philip Thrift wrote:
>>
>>
>>
>> *A Program to Compute Gödel-Löb Fixpoints*
>> Melvin Fitting [ http://melvinfitting.org/ ]
>>
>>
>> https://www.researchgate.net/publication/285841645_A_program_to_compute_Godel-Lob_fixpoints
>>  
>> <https://www.google.com/url?q=https%3A%2F%2Fwww.researchgate.net%2Fpublication%2F285841645_A_program_to_compute_Godel-Lob_fixpoints=D=1=AFQjCNFQ4ORDwOhT81xzkzLgV9unsTybRg>
>>
>>
>> *A loose motivation for much of Melvin Fitting's work can be formulated 
>> succinctly as follows. There are many logics. Our principles of reasoning 
>> vary with context and subject matter. Multiplicity is one of the glories of 
>> modern formal logic. The common thread tying logics together is a concern 
>> for what can be said (syntax), what that means (semantics), and 
>> relationships between the two. A philosophical position that can be 
>> embodied in a formal logic has been shown to be coherent, not correct. 
>> Logic is a tool, not a master, but it is an enjoyable tool to use.*
>> [ https://en.wikipedia.org/wiki/Melvin_Fitting ]
>>
>>
>> also (a bit offbeat):
>>
>> “Simply Gödel,” Phenomenology, and Monads
>> Rudy Rucker
>> http://www.rudyrucker.com/blog/2017/03/17/godel-phenomonology-and-monads/
>>
>> - pt
>>
>

-- 
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.


Re: A Program to Compute Gödel-Löb Fixpoints

2019-03-02 Thread Lawrence Crowell
I guess I am not sure what a Gödel-Löb fixed point is. Is this somehow 
analogous to a Brouwer fixed points in maps or diffeomorphisms of spaces?

I read Rucker's *Infinity and the Mind* last spring, after having read it 
many years ago. I could tell he had a penchant for various mystical ideas. 
This tends blog entry of his suggests he has ideas similar to what Gödel 
thought, and which I think were a part of leading  him into paranoid 
delusions. When I clicked on this for some reason I thought this was about 
monoids, and was a bit disappointed to see it is more philosophical. 
However, I think the Kant noumena is not really directly knowable, and I 
think from quantum mechanics we can't know this as either purely epistemic 
or ontic. I am not sure how ideas of mind fit into this.

LC

On Saturday, March 2, 2019 at 3:26:18 AM UTC-6, Philip Thrift wrote:
>
>
>
> *A Program to Compute Gödel-Löb Fixpoints*
> Melvin Fitting [ http://melvinfitting.org/ ]
>
>
> https://www.researchgate.net/publication/285841645_A_program_to_compute_Godel-Lob_fixpoints
>  
> <https://www.google.com/url?q=https%3A%2F%2Fwww.researchgate.net%2Fpublication%2F285841645_A_program_to_compute_Godel-Lob_fixpoints=D=1=AFQjCNFQ4ORDwOhT81xzkzLgV9unsTybRg>
>
>
> *A loose motivation for much of Melvin Fitting's work can be formulated 
> succinctly as follows. There are many logics. Our principles of reasoning 
> vary with context and subject matter. Multiplicity is one of the glories of 
> modern formal logic. The common thread tying logics together is a concern 
> for what can be said (syntax), what that means (semantics), and 
> relationships between the two. A philosophical position that can be 
> embodied in a formal logic has been shown to be coherent, not correct. 
> Logic is a tool, not a master, but it is an enjoyable tool to use.*
> [ https://en.wikipedia.org/wiki/Melvin_Fitting ]
>
>
> also (a bit offbeat):
>
> “Simply Gödel,” Phenomenology, and Monads
> Rudy Rucker
> http://www.rudyrucker.com/blog/2017/03/17/godel-phenomonology-and-monads/
>
> - pt
>

-- 
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.


A Program to Compute Gödel-Löb Fixpoints

2019-03-02 Thread Philip Thrift


*A Program to Compute Gödel-Löb Fixpoints*
Melvin Fitting [ http://melvinfitting.org/ ]

https://www.researchgate.net/publication/285841645_A_program_to_compute_Godel-Lob_fixpoints


*A loose motivation for much of Melvin Fitting's work can be formulated 
succinctly as follows. There are many logics. Our principles of reasoning 
vary with context and subject matter. Multiplicity is one of the glories of 
modern formal logic. The common thread tying logics together is a concern 
for what can be said (syntax), what that means (semantics), and 
relationships between the two. A philosophical position that can be 
embodied in a formal logic has been shown to be coherent, not correct. 
Logic is a tool, not a master, but it is an enjoyable tool to use.*
[ https://en.wikipedia.org/wiki/Melvin_Fitting ]


also (a bit offbeat):

“Simply Gödel,” Phenomenology, and Monads
Rudy Rucker
http://www.rudyrucker.com/blog/2017/03/17/godel-phenomonology-and-monads/

- pt

-- 
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 everything-list+unsubscr...@googlegroups.com.
To post to this group, send email to everything-list@googlegroups.com.
Visit this group at https://groups.google.com/group/everything-list.
For more options, visit https://groups.google.com/d/optout.