'Who Killed Aunt Agatha' puzzle

Stream: lean4

[Alexandre Rademaker]

https://aarinc.org/Newsletters/141-2023-06.html#geoff

Geoff Sutcliffe post stimulated my curiosity. Besides his claims, I am also interested on the discusion about the explanability of the refutation-based proofs. Because of that, I am trying to construct a proof in Lean. But I can't close one branch... something trivial I may be missing...

The TPTP formalization is here
My code is here

suggestions?

[Ruben Van de Velde]

The goal appears to be false

[Ruben Van de Velde]

Unless multiple people can have killed her

[Alexandre Rademaker]

I guess in this open branch I will need (at some point) the False.elim too, as I did for the last branch on n = charles

[Alexandre Rademaker]

I didn't find any natural deduction proof for this problem. But many different refutation-based solutions. In one text, the authors suggest that "In other words, the [butler cannot have killed Agatha] because this would contradict the fact that [noone hates everyone]." But I could not see how to produce this contradiction from the hypothesis yet.

[Jeremy Avigad]

I think the fourth clue is supposed to include the fact that Agatha doesn't hate the butler.
https://avigad.github.io/lamr/using_first_order_theorem_provers.html#example-aunt-agatha

[Utensil Song]

I think you need:

variable (pel55_10 : ∀ x, ∃ y, lives y ∧ ¬ hates x y)

variable (pel55_13 : charles ≠ butler)

My verbose refutation-style code here.

[Utensil Song]

Minimized to (be like your style):

import Std.Logic
import Std.Tactic.RCases
-- import Mathlib.Tactic

variable (u : Type)
variable (lives : u → Prop)
variable (killed hates richer : u → u → Prop)
variable (agatha butler charles : u)

variable (pel55_1 : ∃ x : u, lives x ∧ killed x agatha)
variable (pel55_2_1 : lives agatha)
variable (pel55_2_2 : lives butler)
variable (pel55_2_3 : lives charles)
variable (pel55_3 : ∀ x, lives x → x = agatha ∨ x = butler ∨ x = charles)
variable (pel55_4 : ∀ x y, killed x y → hates x y)
variable (pel55_5 : ∀ x y, killed x y → ¬ richer x y)
variable (pel55_6 : ∀ x, hates agatha x → ¬ hates charles x)

variable (pel55_7 : ∀ x, x ≠ butler → hates agatha x)
variable (pel55_8 : ∀ x, ¬ richer x agatha → hates butler x)
variable (pel55_9 : ∀ x, hates agatha x → hates butler x)

variable (pel55_10 : ∀ x, ∃ y, lives y ∧ ¬ hates x y)
variable (pel55_11 : agatha ≠ butler)
-- variable (pel55_12 : agatha ≠ charles)
variable (pel55_13 : charles ≠ butler)

theorem result : killed agatha agatha := by
  have ⟨n, ln, kna⟩ := pel55_1
  clear pel55_2_1 pel55_2_2 pel55_2_3
  have labc := pel55_3 n ln
  rcases labc with la | lb | lc
  . rw [la] at kna
    exact kna
  . rw [lb] at kna
    have nrba : ¬richer butler agatha := pel55_5 butler agatha kna
    have hbb : hates butler butler := pel55_8 butler nrba
    have haa : hates agatha agatha := pel55_7 agatha pel55_11
    have hba : hates butler agatha := pel55_9 agatha haa
    have hac : hates agatha charles := pel55_7 charles pel55_13
    have hbc : hates butler charles := pel55_9 charles hac
    have hbe : ¬∃ y, lives y ∧ ¬hates butler y := by
      apply imp_false.mp
      intro he
      rcases he with ⟨e, lnhbe⟩
      have labc := pel55_3 e
      have ⟨le, nhbe⟩ := lnhbe
      have hl := labc le
      rcases hl with ha | hb | hc
      . rw [ha] at nhbe
        contradiction
      . rw [hb] at nhbe
        contradiction
      . rw [hc] at nhbe
        contradiction
    have nhbe : ∃ y, lives y ∧ ¬hates butler y := pel55_10 butler
    contradiction
  . have hca := pel55_4 n agatha kna
    rw [lc] at hca
    have haa := pel55_7 agatha pel55_11
    have nhca := pel55_6 agatha haa
    contradiction

[Stuart Presnell]

Here's an annotated proof. We don't need to add a clue saying that Agatha doesn't hate the Butler, or any further clues distinguishing the people. But as @Utensil Song notes we do need to modify clue 10 to say that the person not hated lives at Dreadbury Mansion.

import Mathlib.Tactic

variable (u : Type)
variable (lives : u → Prop)
variable (killed hates richer : u → u → Prop)
variable (agatha butler charles : u)

variable (premise1 : ∃ x : u, lives x ∧ killed x agatha)
-- variable (premise2_1 : lives agatha)
-- variable (premise2_2 : lives butler)
-- variable (premise2_3 : lives charles)
variable (premise3 : ∀ x, lives x → x = agatha ∨ x = butler ∨ x = charles)
variable (premise4 : ∀ x y, killed x y → hates x y)
variable (premise5 : ∀ x y, killed x y → ¬ richer x y)
variable (premise6 : ∀ x, hates agatha x → ¬ hates charles x)

variable (premise7 : ∀ x, x ≠ butler → hates agatha x)
-- variable (premise7a : ¬ hates agatha butler)

variable (premise8 : ∀ x, ¬ richer x agatha → hates butler x)
variable (premise9 : ∀ x, hates agatha x → hates butler x)

variable (premise10' : ∀ x, ∃ y, lives y ∧ ¬ hates x y)
variable (premise11 : agatha ≠ butler)


theorem result : killed agatha agatha := by
  have ⟨n,h1,h2⟩ := premise1

  -- First, we can elminate Charles as the killer
  have hC_innocent : ¬killed charles agatha := by
    -- Agatha hates everyone except the butler, so she hates herself
    have h_AA : hates agatha agatha := premise7 agatha premise11
    -- Charles doesn't hate anyone Agatha hates, so Charles doesn't hate Agatha
    have h_CA : ¬hates charles agatha := premise6 agatha h_AA
    -- The killer hates their victim, so Charles didn't kill Agatha
    exact (premise4 charles agatha).mt h_CA

  -- The killer was one of Agatha, the Butler, or Charles
  obtain hk | hk | hk := premise3 n h1
  · rw [hk] at h2; exact h2 -- If the killer was Agatha then we're finished
  swap
  · rw [hk] at h2; exact False.elim (hC_innocent h2)  -- We already eliminated Charles

  -- Now we just have to eliminate the Butler
  -- So let's assume for contradiction that the Butler killed Agatha
  rw [hk] at h2; apply False.elim

  -- If the Butler is Charles then we have already eliminated him
  by_cases (charles = butler)
  · rw [←h] at h2; exact hC_innocent h2
  -- So the Butler is not Charles

  -- We will prove that the Butler hates everyone (who lives at Dreadbury Mansion),
  -- thus giving a contradiction
  suffices ∀ x, lives x → hates butler x by
    let ⟨y,hyl,hyb⟩ := premise10' butler
    exact hyb (this y hyl)

  intro x hx
  obtain hbx | hbx | hbx := premise3 x hx
  · rw [hbx]
    -- The Butler hates Agatha, because he killed her
    exact premise4 butler agatha h2
  · rw [hbx]
    -- The Butler is not richer than Agatha, because he killed her
    have h_BA : ¬richer butler agatha := premise5 butler agatha h2
    -- The Butler hates himself, because he is not richer than Agatha
    exact premise8 butler h_BA
  · rw [hbx]
    -- Agatha hates Charles, because she hates everyone except the Butler
    have h_AC : hates agatha charles := premise7 charles h
    -- The Butler hates Charles, because he hates everyone that Agatha hates
    exact premise9 charles h_AC

[Utensil Song]

Yes, local tweaking also shows pel55_13 is not necessary. But lives y is what I failed to remove from hypotheses, and is missing in both the TPTP formalization and the example in LAMR (sent to Vampire), I'm curious how ATPs have successfully drawn the conclusion.

[Eric Rodriguez]

Would it not be better to have u be an enum?

[Utensil Song]

OK, I got it. lives y is also unnecessary, we just need skolemization.

import Std.Logic
import Std.Tactic.RCases
-- import Mathlib.Tactic

variable (u : Type)
variable (lives : u → Prop)
variable (killed hates richer : u → u → Prop)
variable (agatha butler charles : u)

variable (pel55_1 : ∃ x : u, lives x ∧ killed x agatha)
-- variable (pel55_2_1 : lives agatha)
-- variable (pel55_2_2 : lives butler)
-- variable (pel55_2_3 : lives charles)
variable (pel55_3 : ∀ x, lives x → x = agatha ∨ x = butler ∨ x = charles)
variable (pel55_4 : ∀ x y, killed x y → hates x y)
variable (pel55_5 : ∀ x y, killed x y → ¬ richer x y)
variable (pel55_6 : ∀ x, hates agatha x → ¬ hates charles x)

variable (pel55_7 : ∀ x, x ≠ butler → hates agatha x)
variable (pel55_8 : ∀ x, ¬ richer x agatha → hates butler x)
variable (pel55_9 : ∀ x, hates agatha x → hates butler x)

variable (pel55_10 : ∀ x, ∃ y, ¬ hates x y)
-- variable (pel55_10a : ∀ x, ∃ y, lives y ∧ ¬ hates x y)
variable (pel55_11 : agatha ≠ butler)
-- variable (pel55_12 : agatha ≠ charles)
-- variable (pel55_13 : charles ≠ butler)

theorem result : killed agatha agatha := by
  have haa : hates agatha agatha := pel55_7 agatha pel55_11
  have nkca : ¬killed charles agatha := by
    by_contra kca
    have hca := pel55_4 charles agatha kca
    have nhca := pel55_6 agatha haa
    contradiction
  have ⟨n, ln, kna⟩ := pel55_1
  obtain la | lb | lc := pel55_3 n ln
  . rw [la] at kna
    exact kna
  . rw [lb] at kna
    have nrba : ¬richer butler agatha := pel55_5 butler agatha kna
    have hbb : hates butler butler := pel55_8 butler nrba
    simp [Classical.skolem] at pel55_10
    have ⟨sk, nhsk⟩ := pel55_10
    have nhbsk : ¬hates butler (sk butler) := nhsk butler
    have nhask : ¬hates agatha (sk butler) := by
      by_contra hask
      have hbsk := pel55_9 (sk butler) hask
      contradiction
    have eqsk : sk butler = butler := by
      by_contra nesk
      have hbsk := pel55_7 (sk butler) nesk
      contradiction
    have nhbb := eqsk ▸ nhbsk
    contradiction
  . rw [lc] at kna
    contradiction

[Alexandre Rademaker]

Jeremy Avigad said:

I think the fourth clue is supposed to include the fact that Agatha doesn't hate the butler.
https://avigad.github.io/lamr/using_first_order_theorem_provers.html#example-aunt-agatha

Hi @Jeremy Avigad , I found your formalization in a previous version of your Logic and Mechanized Reasoning. I didn't pay atttention to the differences in the axioms mainly because you called Vampire and I am trying to really construct a proof in Lean, preferable a constructive proof.

But my implementation is based on the formalization in TPTP. I double-checked and Vampire was able to find a proof for the problem using the TPTP formalization. So maybe the classical reasoning will be needed, I am still trying to construct an natural deduction proof from the insights I can get from the proof produced to Vampire.

93. $false [avatar sat refutation 66,71,81,92]
% SZS output end Proof for puz001+1
% ------------------------------
% Version: Vampire 4.4.0 (commit 3dd0ed0c on 2020-02-04 14:57:07 +0100)
% Termination reason: Refutation

% Memory used [KB]: 4861
% Time elapsed: 0.002 s
% ------------------------------

[Alexandre Rademaker]

(deleted)

[Alexandre Rademaker]

Utensil Song said:

OK, I got it. lives y is also unnecessary, we just need skolemization.

Wow! I need to check Classical.skolem, but I thought skolemization was need by resolution only to remove the existentials. Why do we need it in Lean?

[Alexandre Rademaker]

OK, the Classical.skolem evoke the axiomOfChoice and 'The fact that the Axiom of Choice implies Excluded Middle' (from here) this means that @Utensil Song proof is classical.

Now I need to understand @Utensil Song proof. Can I finish my proof using byContradiction only? Restricting its use in the one open branch I have?

[Stuart Presnell]

Here's a constructive proof that formalises the clue "No one hates everyone" as pel55_10' : ¬ ∃ x, ∀ y, lives y → hates x y

variable (u : Type)
variable (lives : u → Prop)
variable (killed hates richer : u → u → Prop)
variable (agatha butler charles : u)

variable (pel55_1 : ∃ x : u, lives x ∧ killed x agatha)
-- variable (pel55_2_1 : lives agatha)
-- variable (pel55_2_2 : lives butler)
-- variable (pel55_2_3 : lives charles)
variable (pel55_3 : ∀ x, lives x → x = agatha ∨ x = butler ∨ x = charles)
variable (pel55_4 : ∀ x y, killed x y → hates x y)
variable (pel55_5 : ∀ x y, killed x y → ¬ richer x y)
variable (pel55_6 : ∀ x, hates agatha x → ¬ hates charles x)

variable (pel55_7 : ∀ x, x ≠ butler → hates agatha x)
variable (pel55_8 : ∀ x, ¬ richer x agatha → hates butler x)
variable (pel55_9 : ∀ x, hates agatha x → hates butler x)

-- variable (pel55_10 : ∀ x, ∃ y, ¬ hates x y)
variable (pel55_10' : ¬ ∃ x, ∀ y, lives y → hates x y)
variable (pel55_11 : agatha ≠ butler)

theorem result : killed agatha agatha := by
  have ⟨n,h1,h2⟩ := pel55_1
--  clear pel55_2_1 pel55_2_2 pel55_2_3
  have h3 := pel55_3 n h1
  have hC_innocent : ¬killed charles agatha := by
    have h_AA : hates agatha agatha := pel55_7 agatha pel55_11
    have h_CA : ¬hates charles agatha := pel55_6 agatha h_AA
    intro H
    exact h_CA (pel55_4 charles agatha H)

  cases h3 with
  | inl h => rw [h] at h2; exact h2
  | inr h => cases h with
    | inl h =>
        rw [h] at h1 h2; clear h
        apply False.elim
        apply pel55_10'; exists butler
        intro y hy
        cases pel55_3 y hy with
        | inl h => rw [h] at *; exact pel55_4 butler agatha h2
        | inr h => cases h with
          | inl h => rw [h]; exact pel55_8 butler (pel55_5 butler agatha h2)
          | inr h => rw [h]
                     apply pel55_9 charles
                     apply pel55_7 charles
                     intro H
                     rw [←H] at h2
                     exact hC_innocent h2
    | inr h =>
       rw [h] at h2
       apply False.elim
       exact hC_innocent h2

#print axioms result  -- 'result' does not depend on any axioms

[Utensil Song]

Yes, in order to have a constructive proof, you'll need lives y to express no one hates everyone. If you look the vampire proof close enough, you'll find that it only uses skolemization if lives y is absent.

[Utensil Song]

TPTP formalization didn't reproduce all the clues needed for a natural language reasoning, namely 10 and 13 that I pointed out initially. Missing 10 forces one to reason charles isn't butler based on he is innocent. Missing lives y in 13 forces one to invoke skolemization which turns the proof classical. Both are unnatural consequences.

[Alexandre Rademaker]

Hi @Stuart Presnell , I didn't know about the #print axioms, where can I find the documentation about the #print command that says that it can get the axioms parameter?

Oh... I found the definition the the Lean builtin commands. But no clear documentation yet.

[Alexandre Rademaker]

@Utensil Song I believe we can reduce the proof to just one application of the exclude middle principle.

[Utensil Song]

Alexandre Rademaker said:

Utensil Song I believe we can reduce the proof to just one application of the exclude middle principle.

I wonder how exactly.

[Alexandre Rademaker]

@Utensil Song it is possible, see https://www.jstor.org/stable/45096843, as far as I understand. I will try more from the proofs above.