- (∀x)[Dx → (∃y)(Py · By)]
or (∃x)Dx → (∃y)(Py · By)
- These variations seem acceptable but are not: (∃x)[Dx
→ (∃y)(Py · By)], and (∃x)(∃y)[Dx
→ (Py · By)]. The reason is that they are
*existentially
quantified conditionals*. Existentially quantified conditionals are
trivially true, they are true if there is but one thing that does not
satisfy the antecedent.

- (∀x)(Dx → Cx)
- ~(∃x)Dx → (∀y)(Py
→ ~By) or (∃x)(∀y)[~Dx
→ (Py → ~By)]
- (∀x)[[Dx · (∀y)(Py
→ ~By)] → ~Cx] or (∀x)(∃y)[[Dx · (Py
→ ~By)] → ~Cx]
- Here the "if something" initially pushes us to use an existentially
quantified conditional; but since such expressions don't mean what we want them
to, we retreat to a universal quantifier. Hence the paraphrase underlying our
translation is: All things that are damaged when nobody is blamed will not be
charged to the tenant. Or: Nothing which is damaged when nobody is blamed will
be charged to the tenant.

- (∀x)[(Bx · Yx) → Rx]
- (∃x)(Bx · Yx) → (∃y)(By · Ry)
or (∀x)(∃y)[(Bx · Yx)
→ (By · Ry)]
- Note this is
*not* an existentially quantified conditional.
It is an conditional with an existentially quantified
antecedent and consequent.

- (∀x)[(Bx · Yx) → [(∀y)[(By · Yy)
→ Ry] → Rx]]
- See comments to exercises 4, above. The x quantifier
cannot be existential, for then we'd have an existentially quantified
conditional.

- (∀x)[(Bx · Rx) → Yx]
→ (∃y)(Yy · Ry) or (∃x)(∃y){[(Bx · Rx)
→ Yx] → (Yy · Ry)}
- See comments to exercises 4, above. The x quantifier
cannot be existential, for then we'd have an existentially quantified
conditional.

- (∀x)[(Ox ·
Px) → (Cx v Mx)] → [(∃y)(Cy · Py)
v (∃z)(Mz · Pz)]
- (∀x)[(Ox · Px) → [(∀y)(My
→ ~Py) v Mx]]
- See comments to exercises 4, above. The x quantifier
cannot be existential, for then we'd have an existentially quantified
conditional.

- (∃x)(Ox · Px) → [(∀y)((Oy · Py)
→ Cy) → (∃z)(Cz · Pz)]
- (∀x)[(Ox · Px) → [(∀y)[(Oy · Py)
→ Cy] → Cx]]
- (∀x)[(Sx → Fx) · (Sx
→ Wx)] → [(∃y)(Sy)
→ (∃z)(Wz · Fz)]
- (∀x)[(Sx · Wx) → [(∀y)(Wy
→ Fy) → Fx]]
- (∀x)[[(Sx) · (∀y)(Sy
→ Wy)] → Wx]
- [(∀x)(Px → Fx) · (y∀)(Ey
→ ~Ly)] → (∃z)(Ez · Sz)
- (∀x)[(Ex · Lx) → [(∃y)(Py · ~Fy)
→ ~Sx]]
- [(∃x)(Ex · Lx) · (∃y)(Py · ~Fy)]
→ (∃z)(Ez · ~Sz)
- (∃x)(Hx · ~Sx) → [(∀y)(Wy
→ Ay) → (∃z)(Wz · Dz)]
- (∀x)[(Hx · ~Sx) → [(∃y)(Wy · Ay)
→ Ux]]

Prenexed and Purified forms of these answers