Unexpected hanging paradox

Hanging.lean

import Init.Data.Ord

namespace Weekday

/- Weekdays -/
inductive Weekday where
  | monday : Weekday
  | tuesday : Weekday
  | wednesday : Weekday
  | thursday  : Weekday
  | friday    : Weekday

deriving instance BEq for Weekday
deriving instance Ord for Weekday

end Weekday

open Weekday
open Weekday.Weekday

/- We can either be on a day in the week, or sometime before. -/
inductive WeekAndBefore where
  | dayBefore : WeekAndBefore
  | someWeekday : Weekday -> WeekAndBefore

open WeekAndBefore

instance : Ord WeekAndBefore where
  compare
    | dayBefore, someWeekday _ => Ordering.lt
    | someWeekday a, someWeekday b => compare a b
    | _, _ => Ordering.eq

/- Indicates that the hanging happend on this day. -/
constant hangingOnDay : Weekday -> Prop

/- Hanging must happen on some weekday -/
def hangingHappens : Prop := ∃ (d : Weekday), hangingOnDay d

/- Interpret that hanging _may_ happen as the lack of a proof that it can't.-/
def hangingMayHappen : Weekday -> Prop :=
  fun (d : Weekday) => ¬¬(hangingOnDay d)

/- Is one day (potentially out of the week) before another? -/
def isBefore (x : WeekAndBefore) (y : Weekday) : Prop :=
  compare x (someWeekday y) == Ordering.lt

/- Given a day, express that we have not yet been hanged. -/
def notHangedYet : WeekAndBefore -> Prop :=
  fun (td : WeekAndBefore) => ∀ (d : Weekday),
    (¬ isBefore td d) -> ¬ (hangingOnDay d)

/- Some axioms -/
axiom hangingDefinitelyHappens : hangingHappens

axiom hangingHappensOnce : ∀ d : Weekday, hangingOnDay d ->
  forall d' : Weekday, d != d' -> ¬ hangingOnDay d'

axiom pastIsKnown : ∀ d : Weekday, ∀ td : WeekAndBefore, ¬(isBefore td d) ->
  hangingOnDay d ∨ ¬ hangingOnDay d

axiom futureIsUncertain : ∀ td : WeekAndBefore, notHangedYet td ->
  ∀ d : Weekday, isBefore td d -> hangingMayHappen d

  /- What is the nature of surprise? -/

def surprise : Prop := ∀ td : WeekAndBefore, ∀ d : Weekday,
  hangingOnDay d -> ¬ isBefore td d

/- Auxiliary theorems -/

/- Hanging implies this proposition -/
def ifHangingThen : (Weekday -> Prop) -> Prop :=
  fun can => forall d : Weekday, hangingOnDay d -> can d

theorem dni : {p : Prop} -> p -> ¬¬p := by
  intros P p h
  exact (h p)

/- If hanging took place on day d, then it can take place.
  Proving this is double negation introduction.
-/
theorem doesImpCan : ifHangingThen hangingMayHappen := sorry


theorem weKnowOnFriday : notHangedYet (someWeekday thursday) <-> hangingOnDay friday := sorry

theorem unsurprising : ¬surprise := sorry