| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Surprise Paradox
| Title: | Surprise Paradox |
| Author: | Joachim Breitner (joachim /at/ cis /dot/ upenn /dot/ edu) |
| Submission date: | 2016-07-17 |
| Abstract: | 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. |
| BibTeX: |
@article{Surprise_Paradox-AFP,
author = {Joachim Breitner},
title = {Surprise Paradox},
journal = {Archive of Formal Proofs},
month = jul,
year = 2016,
note = {\url{https://isa-afp.org/entries/Surprise_Paradox.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Incompleteness |
| Status: [ok] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |