Email Gateway (Aug 22 2022 at 13:49): Email Gateway (Aug 22 2022 at 13:49):From: Tobias Nipkow <nipkow@in.tum.de>
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?
smime.p7s
Email Gateway (Aug 22 2022 at 13:49):From: Andreas Röhler <andreas.roehler@easy-emacs.de>
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
Last updated: Apr 25 2024 at 20:15 UTC