Re: [isabelle] Surprise!





On 18.07.2016 07:59, Tobias Nipkow wrote:
New AFP Article: > > Surprise Paradox Joachim Breitner > > In 1964, Fitch showed that
the paradox of the surprise hanging can be > resolved by showing that the judgeâs verdict is inconsistent. His > formalization builds on GÃdelâs coding of provability. In this > theory, we reproduce his proof in Isabelle, building on Paulsonâs > formalisation of GÃdelâs incompleteness theorems. > > https://www.isa-afp.org/entries/Surprise_Paradox.shtml > > Surprised? >

As GÃdel was mentioned lately but no appropriate response:

IIUC GÃdel spoke about an incompleteness being inherent, i.e. despite any effort to avoid it.

Might be worth to discriminate the fundamental issue GÃdel was about and this simple case, where contradictions are delivered. resp. not sufficient informations to decide a question.

If something "cannot be proven from the given assumptions", it doesn't say yet, "there is no way to complete the assumptions". Substance of GÃdelâs incompleteness theorem seems not affected so far.

Cheers,

Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.