coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Unexpected hanging formalization

From: Polina Vinogradova <polina.vino AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Unexpected hanging formalization
Date: Thu, 20 May 2021 15:44:48 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=polina.vino AT gmail.com; spf=Pass smtp.mailfrom=polina.vino AT gmail.com; spf=None smtp.helo=postmaster AT mail-ot1-f53.google.com
Ironport-data: A9a23:Ugi/7KwzKTxaKChmU5V6t+dVxyrEfRIJ4+MujC/XYbTApDh2hDMHy2AWWmiDPauOMGP2eY8lat7ioUoO75aGmN9nOVdlrnsFo1Bi+ZOUX4zBRqvTF3rPdZObFBoPA/3z27AsFehsJpPnjkrrYuKJQUVUj/nSH+KhUb+cZEideCc9IMsfoUI78wIGqtUw6TSJK1vlVeLa+6UzCnf9s9JHGj58B5a4lf9alK+aVAX0EbAJTasjUFf2zxH5BX+ETE27ByOQroJ8RoZWSwtfpYxV8F81/z91Yj+kurPyc0lPRaKLeAbT0TxZXK+thhUErSs3uko5HKBEOAEH1nPTxog3lY4lWZ+YEW/FOoXUn+AcVRAeDSB4OoVJ/bbGJT60tsn7I0juLiO9mak1UR9tVWEf0r8vXTsmGeYjADsKd1WIg/+86KmqT/FlwMUlNsjieo0F0kyMZxnNVaN8B8/XGvCSo4dMhmJowJofTK/KPJ9BL2d7M0HpfTlkP3M7CLYflcGUnF3BchhM8QrA++5u9wA/1yR02bnpdd3JI5mEGJ4TkUGfqWbLuW/+B3kn2BWk4WLt2hqRaiXnxEsXmb7+FYFUMtZviVyXg2sPUVgYCAD9rv6+hUqzHdlYLiT4PwJGQbcarCSWohvVBnVUY0JoejYTXtNRF6sx7wTlJm/8/VOCHmZdJtJeQIVOiSL1LADGEneGmtroAXpkt7j9pbe1nluLhWvaBBX55lPuqcPJocXpLjUjTEwOYsrzc+te
Ironport-hdrordr: A9a23:mL9TB61S6BoR8SlvZqerUwqjBMckLtp133Aq2lEZdPU7SKClfqyV8cjzqyWbtN95YhhJ8uxoU5PufZqzz/RI3bU=
Ironport-phdr: A9a23:rStNbR32F74Yn4ansmDOUwQyDhhOgF0UFjAc5pdvsb9SaKPrp82kYBWOo68y1RSQBdiTwskHotKei7rnV20E7MTJm1E5W7sIaSU4j94LlRcrGs+PBB6zBvfraysnAJYKDwc9rDm0PkdPBcnxeUDZrGGs4j4OABX/Mhd+KvjoFoLIgMm7yuS/94fNbwhKmTaxbq5+IAm2oA7MqsQYnIxuJ7orxBDUuHVIYeNWxW1pJVKXgRnx49q78YBg/SpNpf8v7tZMXqrmcas2S7xYFykmPHsu5ML3rxnDTBCA6WUaX24LjxdHGQnF7BX9Xpfsriv3s/d21SeGMcHqS70/RDKv5LppRhD1kicKLzE2/mHZhMJzkaxVvg6uqgdlzILIeoyYLuZycr/fcN4cWGFPXtxRVytEAo6kdYUPCO4BPeder4bnulABohq+BQ+rBOPg0D9HnGL53aok0+s7DArL2xQgH9UKsHTVqtX6Lr0eUf60zKnOyjXOdPxW2TLn54jJdhAtu+2DXbV1ccfIz0QkCgzKgEmKp4P/IzOVyvoCs3Kd7+d4S++hhGAqpgBtrjWy2ssiipTEiIwVx17L6yl0wok4KcO7RUN7fNKoDIVcuj+ZOoV4QM4sTW9ltTokxrACpJO3Yi4Hw4kpyR7YbvyIaYmI4hT7WeaeIDd4mHJleK+kiBqo7Uegzej8W8+p21hJtipIisfAumwJ2hDJ6cWKSuFx8lm81TqTzQze6u9JLEYpnqTBMZEh2KQ/lp8LvETDACD2nEL2gbeTdko+++io7/3rYrL6ppOBLoN0hAHzP6o0lsywBuQ4NQcOX2yF9uimyLLj+kj5TK1Ljv0wjKbZrIjXKdoHqqO9GQNY0YYu5wyhAzu7zNgUh3kKIVxddBKClYfpOlXOIP7iDfe4hlShiC9rx/fCPr3gBJXCNGLPkKngfbZ77E5R0wUzzdVF6JJVDrENOu78Wkj0tNDAFB82LxS0w/r7CNV6zo4RRWWPAraAPKzOtV+I+/kgLvKXZI4VvTb9M+Iq6+TvjX8/g18dfLOm0YEZaHCiTbxaJBCSZmOpidMcG08LuBA/Rarkkg6sSzlWMk61W6M673kFCYShAp3KSoezifTVxCC/H5tfIH5HDFekHnLhdoHCUPAJPnHBavR9myAJAODyA7Qq0guj4VeSI1tPK+PV/mgfqcum2oUuoeLUkh42+Hp/CMHPiwllqkl7m2oJQ3k926Ut+SSVJX+M1KF5h7pTEtkBvpt0

Hello everyone!

The unexpected hanging paradox is really well known, but I haven't seen a formalization of it. If you have, I'd love to see it too! I took a crack at it using constructive logic, see

https://github.com/polinavino/unexpected_hanging/blob/master/unexpected_hanging.v

The gist of the results is this :

This formalization defines the axiom system which the unexpected hanging paradox informally describes. Unsurprisingly, a reasonably defined notion of "surprise", when introduced into the system as one of the axioms, ie. one of the requirements of the hanging paradox system, introduces inconsistency.

As a result, admitting the SURPRISE axiom allows us to prove everything (from False). The unexpected hanging situation is not a "paradox" so much as it is having contradictory requirements for the system to specify, making it inconsistent

If we do not require to be surprised by a Friday hanging on Thursday, there is no inconsistency.

NOTE : this adjusted definition of SURPRISE that excludes today being Thursday (and allows for predictability of surprise on Friday) is just changing the requirements to be surprised, NOT excluding these from the axiom system.

Polina

[Coq-Club] Unexpected hanging formalization, Polina Vinogradova, 05/20/2021