> On 25 Apr 2018, at 21:13, Brent Meeker <meeke...@verizon.net> wrote: > > > > On 4/25/2018 3:35 AM, Bruno Marchal wrote: >> G proves that (p <-> ~ []p) is equivalent with (p <-> <>t), or equivalently >> (p <-> ~[]f). So consistency (<>t) is a solution to the (logical) equation x >> <-> ~[]x. > > ?? What does this proof look like?
? That is Gödel’s second theorem, axiomatised in G. p is a sentence equivalent with its non provability (p <-> ~[]p), and Gödel, already in his 1931 papers suggests that this entails that p is equivalent with consistency (<>t). That has been proved by Hilbert and Bernays later, and generalised and simplified by Löb. > Why doesn't it prove f <->~[]f ? ? That is true for an inconstant theory. (Typo error?). If the theory is consistent then 1) t <-> ~[]f (t, not f), 2) but the theory/machine/Löbian-number cannot prove “1)”. Bruno > > Brent > > -- > 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. -- 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.
