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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and