> On 25 Apr 2018, at 21:13, Brent Meeker <[email protected]> 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 [email protected]. > To post to this group, send email to [email protected]. > 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 [email protected]. To post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
