Marc Horowitz 24.151 ∀pril 2, 1992

(1) W(ιx)Pxm (∃x)((∀y)(Pym ↔ y=x) ∧ Wx)

(2) I(ιx)Pxm w (∃x)((∀y)(Pym ↔ y=x) ∧ Ixw)

(3) M(ιx)Pxm (ιy)Pyh (∃w)((∀x)(Pxm ↔ x=w) ∧ Mw(ιy)Pyh) (∃w)((∀x)(Pxm ↔ x=w) ∧ (∃y)((∀z)(Pzh ↔ z=y) Mwy))

(4) ¬(E!x)(ιx)Pxc ¬(∃x)(∀y)(Pyc ↔ y=x)

(5) ¬(ιx)Pxm = (ιy)Pyh) (∃w)((∀x)(Pxm ↔ x=w) ∧ (∃y)((∀z)(Pzh ↔ z=y) w=y))

(6) ¬P(ιx)Pxm h ¬(∃x)((∀y)(Pym ↔ y=x) ∧ Pxh)

(7) I(ιx)Pxm w → W(ιx)Pxm (∃x)((∀y)(Pym ↔ y=x) ∧ Ixw) → (∃x)((∀y)(Pyh ↔ y=x) ∧ Wx)