### 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.

### License

BSD License

### Topics

- Logic/Proof theory

### Session Surprise_Paradox

- Surprise_Paradox

### Depends on

- Gödel’s Incompleteness Theorems

### Auto-related entries

- The Transcendence of e

## Cite

×

Surprise_Paradox-AFP

    @article{Surprise_Paradox-AFP,
      author  = {Joachim Breitner},
      title   = {Surprise Paradox},
      journal = {Archive of Formal Proofs},
      month   = {July},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Surprise_Paradox.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Jul 17, 2016 : Isabelle2016