== The following puzzle is due to L. Schubert == == A mysterious death at Dreadbury Mansion ... == == 1: Someone who lives at Dreadbury Mansion killed Aunt Agatha. == 2: Only Agatha, the butler and Charles has lived at Dreadbury Mansion. == 3: A killer always hates their victim. == 4: A killer is never richer than their victim. == 5: Charles hates no-one that Aunt Agatha hates. == 6: Aunt Agatha hates everyone but the butler. == 7: The butler hates everyone who is not richer than Aunt Agatha. == 8: The butler hates everyone Aunt Agatha hates. == 9: No-one hates everyone. == 10: Aunt Agatha is not identical with the butler, of course. == == Question: Who killed Aunt Agatha? == environ reserve x1,x2,z,u,v,w for Person; given Agatha, butler, Charles being Person; 1: ex x1 st LivesatDBM[x1] & Killed[x1,Agatha]; 2: for x1 st LivesatDBM[x1] holds x1=Agatha or x1=butler or x1=Charles; 3: for x1,x2 st Killed[x1,x2] holds Hates[x1,x2]; 4: for x1,x2 st Killed[x1,x2] holds not Richer[x1,x2]; 5: for x1 st Hates[Agatha,x1] holds not Hates[Charles,x1]; 6: for x1 st x1<>butler holds Hates[Agatha,x1]; 7: for x1 st not Richer[x1,Agatha] holds Hates[butler,x1]; 8: for x1 st Hates[Agatha,x1] holds Hates[butler,x1]; 9: for x1 ex x2 st not Hates[x1,x2]; 10: Agatha<>butler begin Killed[Agatha, Agatha] proof 11: for x1 st x1<>butler holds Hates[butler,x1] proof let u be Person; assume 11a: u<>butler; thus Hates[butler,u] proof 11b: Hates[Agatha,u] by 11a,6; thus thesis by 8,11b; end; end; 12: ex x2 st not Hates[butler,x2] by 9; consider u such that 13: not Hates[butler,u] by 12; 14: u=butler proof assume 14a: u<>butler; 14b: Hates[butler,u] by 11,14a; thus contradiction by 13,14b; end; 15: not Hates[butler,butler] by 13,14; 16: Richer[butler,Agatha] by 7,15; 17: not Killed[butler,Agatha] by 4,16; 18: Hates[Agatha,Agatha] by 6,10; 19: not Hates[Charles,Agatha] by 5,18; 20: not Killed[Charles,Agatha] by 3,19; consider u such that 21: LivesatDBM[u] & Killed[u,Agatha] by 1; 22: u=Agatha or u=butler or u=Charles by 2,21; 23: u<>butler & u<>Charles by 17,20,21; 24: u=Agatha by 22,23; thus thesis by 21,24; end

environ == The following example is due to L. Schubert. == == Wolves, foxes, birds, caterpillars, and snails are animals, and there == are some of each of them. reserve x, y, w, f, b, c, s for animal; A: ex w, f, b, c, s st wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s]; == Also, there are some grains, and grains are plants. reserve p, g for plants; P: ex g st grain[g]; == Every animal either likes to eat all plants or all animals much smaller == than itself that like to eat some plants. 1LIKES: for x holds (for p holds likes[x,p]) or (for y st smaller[y,x] & (ex p st likes[y,p]) holds likes[x,y]); == Caterpillars and snails are much smaller than birds, which are much smaller == than foxes, which in turn are much smaller than wolves. 1SMALLER: for x, y st (caterpillar[x] or snail[x]) & bird[y] holds smaller[x,y]; 2SMALLER: for x, y st bird[x] & fox[y] holds smaller[x,y]; 3SMALLER: for x, y st fox[x] & wolf[y] holds smaller[x,y]; == Wolves do not like to eat foxes or grains, while birds like to eat == caterpillars but not snails. 2LIKES: for x, y, p st wolf[x] & fox[y] & grain[p] holds not likes[x,y] & not likes[x,p]; 3LIKES: for x, y st bird[x] holds (caterpillar[y] implies likes[x,y]) & (snail[y] implies not likes[x,y]); == Caterpillars and snails like to eat some plants. 4LIKES: for x st caterpillar[x] or snail[x] ex p st likes[x,p] == Therefore there is an animal that likes to eat a grain-eating animal. begin ex x, y, p st likes[x,y] & likes[y,p] & grain[p] proof consider w, f, b, c, s such that WFBCS: wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s] by A; consider g such that G: grain[g] by P; 0: not likes[b,s] & (ex p st likes[s,p]) & smaller[s,b] by 3LIKES, 4LIKES, 1SMALLER, WFBCS; 1: likes[b,g] by 0, 1LIKES; 2: smaller[f,w] & not likes[w,f] & not likes[w,g] by 3SMALLER, 2LIKES, G, WFBCS; 3: not likes[f,g] by 2, 1LIKES; 4: smaller[b,f] by 2SMALLER, WFBCS; 5: likes[f,b] by 1, 3, 4, 1LIKES; thus thesis by G, 1, 5 end; == A bit shorter, but messier. ex x, y, p st likes[x,y] & likes[y,p] & grain[p] proof consider w, f, b, c, s such that WFBCS: wolf[w] & fox[f] & bird[b] & caterpillar[c] & snail[s] by A; consider g such that G: grain[g] by P; 1: not likes[b,s] & (ex p st likes[s,p]) & smaller[s,b] & smaller[f,w] & not likes[w,f] & not likes[w,g] & smaller[b,f] by 1SMALLER, 2SMALLER, 3SMALLER, 2LIKES, 3LIKES, 4LIKES, G, WFBCS; 2: likes[b,g] & not likes[f,g] by 1, 1LIKES; 3: likes[b,g] & likes[f,b] by 1, 2, 1LIKES; thus thesis by G, 3 end == Who will make it any shorter?