Encoding a Raymond Smullyan Logic Puzzle Proof

Stream: new members

[Mark Fischer]

I found this article where the author creates a model checker for some of Smullyan's puzzles and I thought to myself that this formalization would also work via a proof in Lean.

I'm not sure if this is the best way to encode something like this. I wasn't really sure how to create a return type that didn't give away the answer beforehand (and unless you're creating a puzzle, why would you even want to?)

The setup is that everybody is either always truthful or always a liar. Furthermore brothers are always of the same inclination, so they either both tell the truth or they both lie.

Here's the puzzle:

Now, I heard a story of two brothers, Bahman and Perviz, who were once asked if they were married. They gave the following replies:

Bahman: We are both married.

Perviz: I am not married.

“Is Bahman married or not? And what about Perviz?”

and here is my proof that (married Bahman = false) ∧ (married Perviz = true). The thing I'm not sure about is whether ∃a b : Bool ... is too permissive? Actually, I'm pretty sure it is. Classically, this seems just trivially true without even looking at the hypothesis in question.

Is there a better way to encode this?

import Mathlib

opaque Object : Type

def Predicate := Object → Prop

open Classical

example
  (truthful married : Predicate)
  (Bahman Perviz : Object)
  (h1 : truthful Bahman ↔ truthful Perviz)
  (h2 : truthful Bahman ↔ married Bahman ∧ married Perviz)
  (h3 : truthful Perviz ↔ ¬ married Perviz)
  : ∃a b : Bool, (married Bahman = a) ∧ (married Perviz = b) := by

  cases Classical.em <| truthful Bahman with
  | inl h =>
    have mpe := (h2.mp h).right
    have nmp := h3.mp <| h1.mp h
    contradiction
  | inr h =>
    have ntp := (iff_false_left h).mp h1
    have mpe := not_not.mp <| mt h3.mpr ntp
    have nmor := not_and_or.mp <| (iff_false_left h).mp h2
    have nmb := nmor.resolve_right (not_not.mpr mpe)
    use false, true
    simp only [eq_iff_iff, iff_false, iff_true]
    exact ⟨nmb, mpe⟩

[Mark Fischer]

Maybe this is more compelling as you need to provide actual data for each claim?

example
  (truthful married : Predicate)
  (Bahman Perviz : Object)
  (h1 : truthful Bahman ↔ truthful Perviz)
  (h2 : truthful Bahman ↔ married Bahman ∧ married Perviz)
  (h3 : truthful Perviz ↔ ¬ married Perviz)
  : {x : Bool × Bool // married Bahman = x.1 ∧ married Perviz = x.2} := by

  use (false, true)
  simp only [eq_iff_iff, iff_false, iff_true]
  cases Classical.em <| truthful Bahman with
  | inl h =>
    have mpe := (h2.mp h).right
    have nmp := h3.mp <| h1.mp h
    contradiction
  | inr h =>
    have ntp := (iff_false_left h).mp h1
    have mpe := not_not.mp <| mt h3.mpr ntp
    have nmor := not_and_or.mp <| (iff_false_left h).mp h2
    have nmb := nmor.resolve_right (not_not.mpr mpe)
    exact ⟨nmb, mpe⟩

[Notification Bot]

Junyan Xu has marked this topic as resolved.

[Notification Bot]

Junyan Xu has marked this topic as unresolved.