Re: Connection between Provability Logic (GL) and geometry?
> On 19 Mar 2019, at 19:01, Philip Thrift wrote: > > > > On Tuesday, March 19, 2019 at 9:16:57 AM UTC-5, Bruno Marchal wrote: > >> On 18 Mar 2019, at 20:33, Philip Thrift > >> wrote: >> >> >> Might have something of interest ... >> >> https://mathoverflow.net/questions/325702/connection-between-provability-logic-gl-and-geometry >> >> <https://www.google.com/url?q=https%3A%2F%2Fmathoverflow.net%2Fquestions%2F325702%2Fconnection-between-provability-logic-gl-and-geometry=D=1=AFQjCNF4OHbDm6tYoYD1Y55XxgK8qFi0TQ> >> >> ... >> >> There seems to be an existing literature on topological semantics and >> provability logics. Thomas Icard has slides on this >> <http://logic.berkeley.edu/colloquium/IcardSlides.pdf>, and the Stanford >> Encyclopedia of Philosophy has a bit on the topic >> <https://plato.stanford.edu/entries/logic-provability/#TopoSemaForProvLogi>. >> I'm not sure how related this is to the specific topological/geometric >> intuitions you give here, but it might be of interest more broadly. – Noah >> Schweber <https://mathoverflow.net/users/8133/noah-schweber> 31 mins ago >> <https://mathoverflow.net/questions/325702/connection-between-provability-logic-gl-and-geometry#comment813108_325702> >> >> > > > I know the work of Leo Esakia, (and of Blok) notably his Russian paper (*) > and it is indeed quite interesting. It provides interesting topological > semantics for variants of K4 and GL (called G here). Icard has extended such > semantics for the logic GLP, which is a polymodal logic axiomatising the > provability logic on sequence of stronger and stronger theories. At each > level n we have a box [n] obeying to G, and with the two axioms: > > [n]p -> [n+1]p > p -> [n+1]p > > for all n, Beklemishev has shown that this is complete for the arithmetical > interpretation extended on this succession of theories. I use this in some > more detailed exposition. > In the work of Esakia, the consistency <>p becomes a special sort of abstract > derivative. The idea of using topological model cale from the work of > McKinsey and Tarski, in the spirit of the algebraic semantics of Helena > Rasiowa and Roman Sikorski “The mathematics of Metamathematics” (an excellent > work on algebraic semantics). > > The topological space, in the semantics of Esakia, are not Hausdorff spaces, > and are rather peculiar from a topologist standpoint, but nevertheless, that > work is quite interesting. It is a good complement of the more traditional > Kripke or Krpke-inspired semantics (which I use much more). > > Unfortunately, although this will have interesting application for the > general theology of “growing machine”, the topology is not related directly > to the quantum “geometry” of the “material” variant of G (the Z and X logics > I have shown to exist here). > > But thanks for this link. I missed those slides by Icard, and some references > therein. > > Esakia died in 2010, and was responsible for the great interest in > provability logic in Georgia (Europa). > > Bruno > > > > (*) Esakia, L. (1981). Diagonal constructions, Löb’s formula and Cantor’s > scattered space (Russian). In Studies in logic and semantics, pages 128–143. > Metsniereba, Tbilisi. > > >> - pt >> > > > There are now three links supplied in the MathOverflow post: > > (SEP article) > https://plato.stanford.edu/entries/logic-provability/#TopoSemaForProvLogi This is a good summary … for mathematicians. Not so good for the philosophical applications. > > Topological Semantics for Provability Logics > http://logic.berkeley.edu/colloquium/IcardSlides.pdf Yes, that are the slides by Icard, which I appreciate. To be sure, it is not needed to understand the G* “theology”. It raised the question of formalising GLP* (the truth logic about the sequences of machines obeying GLP). I have some ideas of this, but it is very technical. > > The Topological Structure of Asynchronous Computability > http://cs.brown.edu/people/mph/HerlihyS99/p858-herlihy.pdf That looks quite interesting, and I might read it later. It is not related to the provability logic, as far as I can see. 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 >
Re: Connection between Provability Logic (GL) and geometry?
On Tuesday, March 19, 2019 at 9:16:57 AM UTC-5, Bruno Marchal wrote: > > > On 18 Mar 2019, at 20:33, Philip Thrift > > wrote: > > > Might have something of interest ... > > > https://mathoverflow.net/questions/325702/connection-between-provability-logic-gl-and-geometry > > <https://www.google.com/url?q=https%3A%2F%2Fmathoverflow.net%2Fquestions%2F325702%2Fconnection-between-provability-logic-gl-and-geometry=D=1=AFQjCNF4OHbDm6tYoYD1Y55XxgK8qFi0TQ> > > ... > > There seems to be an existing literature on topological semantics and > provability logics. Thomas Icard has slides on this > <http://logic.berkeley.edu/colloquium/IcardSlides.pdf>, and the Stanford > Encyclopedia of Philosophy has a bit on the topic > <https://plato.stanford.edu/entries/logic-provability/#TopoSemaForProvLogi>. > I'm not sure how related this is to the specific topological/geometric > intuitions you give here, but it might be of interest more broadly. – Noah > Schweber <https://mathoverflow.net/users/8133/noah-schweber> 31 mins ago > <https://mathoverflow.net/questions/325702/connection-between-provability-logic-gl-and-geometry#comment813108_325702> > > > > > I know the work of Leo Esakia, (and of Blok) notably his Russian paper (*) > and it is indeed quite interesting. It provides interesting topological > semantics for variants of K4 and GL (called G here). Icard has extended > such semantics for the logic GLP, which is a polymodal logic axiomatising > the provability logic on sequence of stronger and stronger theories. At > each level n we have a box [n] obeying to G, and with the two axioms: > > [n]p -> [n+1]p > p -> [n+1]p > > for all n, Beklemishev has shown that this is complete for the > arithmetical interpretation extended on this succession of theories. I use > this in some more detailed exposition. > In the work of Esakia, the consistency <>p becomes a special sort of > abstract derivative. The idea of using topological model cale from the work > of McKinsey and Tarski, in the spirit of the algebraic semantics of Helena > Rasiowa and Roman Sikorski “The mathematics of Metamathematics” (an > excellent work on algebraic semantics). > > The topological space, in the semantics of Esakia, are not Hausdorff > spaces, and are rather peculiar from a topologist standpoint, but > nevertheless, that work is quite interesting. It is a good complement of > the more traditional Kripke or Krpke-inspired semantics (which I use much > more). > > Unfortunately, although this will have interesting application for the > general theology of “growing machine”, the topology is not related directly > to the quantum “geometry” of the “material” variant of G (the Z and X > logics I have shown to exist here). > > But thanks for this link. I missed those slides by Icard, and some > references therein. > > Esakia died in 2010, and was responsible for the great interest in > provability logic in Georgia (Europa). > > Bruno > > > > (*) Esakia, L. (1981). Diagonal constructions, Löb’s formula and Cantor’s > scattered space (Russian). In Studies in logic and semantics, pages > 128–143. Metsniereba, Tbilisi. > > > - pt > > There are now three links supplied in the MathOverflow post: (SEP article) https://plato.stanford.edu/entries/logic-provability/#TopoSemaForProvLogi *Topological Semantics for Provability Logics* http://logic.berkeley.edu/colloquium/IcardSlides.pdf *The Topological Structure of Asynchronous Computability* http://cs.brown.edu/people/mph/HerlihyS99/p858-herlihy.pdf - 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: Connection between Provability Logic (GL) and geometry?
> On 18 Mar 2019, at 20:33, Philip Thrift wrote: > > > Might have something of interest ... > > https://mathoverflow.net/questions/325702/connection-between-provability-logic-gl-and-geometry > > ... > > There seems to be an existing literature on topological semantics and > provability logics. Thomas Icard has slides on this > <http://logic.berkeley.edu/colloquium/IcardSlides.pdf>, and the Stanford > Encyclopedia of Philosophy has a bit on the topic > <https://plato.stanford.edu/entries/logic-provability/#TopoSemaForProvLogi>. > I'm not sure how related this is to the specific topological/geometric > intuitions you give here, but it might be of interest more broadly. – Noah > Schweber <https://mathoverflow.net/users/8133/noah-schweber> 31 mins ago > <https://mathoverflow.net/questions/325702/connection-between-provability-logic-gl-and-geometry#comment813108_325702> > > I know the work of Leo Esakia, (and of Blok) notably his Russian paper (*) and it is indeed quite interesting. It provides interesting topological semantics for variants of K4 and GL (called G here). Icard has extended such semantics for the logic GLP, which is a polymodal logic axiomatising the provability logic on sequence of stronger and stronger theories. At each level n we have a box [n] obeying to G, and with the two axioms: [n]p -> [n+1]p p -> [n+1]p for all n, Beklemishev has shown that this is complete for the arithmetical interpretation extended on this succession of theories. I use this in some more detailed exposition. In the work of Esakia, the consistency <>p becomes a special sort of abstract derivative. The idea of using topological model cale from the work of McKinsey and Tarski, in the spirit of the algebraic semantics of Helena Rasiowa and Roman Sikorski “The mathematics of Metamathematics” (an excellent work on algebraic semantics). The topological space, in the semantics of Esakia, are not Hausdorff spaces, and are rather peculiar from a topologist standpoint, but nevertheless, that work is quite interesting. It is a good complement of the more traditional Kripke or Krpke-inspired semantics (which I use much more). Unfortunately, although this will have interesting application for the general theology of “growing machine”, the topology is not related directly to the quantum “geometry” of the “material” variant of G (the Z and X logics I have shown to exist here). But thanks for this link. I missed those slides by Icard, and some references therein. Esakia died in 2010, and was responsible for the great interest in provability logic in Georgia (Europa). Bruno (*) Esakia, L. (1981). Diagonal constructions, Löb’s formula and Cantor’s scattered space (Russian). In Studies in logic and semantics, pages 128–143. Metsniereba, Tbilisi. > - 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.
Connection between Provability Logic (GL) and geometry?
Might have something of interest ... https://mathoverflow.net/questions/325702/connection-between-provability-logic-gl-and-geometry ... There seems to be an existing literature on topological semantics and provability logics. Thomas Icard has slides on this <http://logic.berkeley.edu/colloquium/IcardSlides.pdf>, and the Stanford Encyclopedia of Philosophy has a bit on the topic <https://plato.stanford.edu/entries/logic-provability/#TopoSemaForProvLogi>. I'm not sure how related this is to the specific topological/geometric intuitions you give here, but it might be of interest more broadly. – Noah Schweber <https://mathoverflow.net/users/8133/noah-schweber> 31 mins ago <https://mathoverflow.net/questions/325702/connection-between-provability-logic-gl-and-geometry#comment813108_325702> - 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.
