Corrected Symbolic Logic Translation

Page 345 - Symbolic / Predicate Logic

∀x∀y[Nx·Tx·Ny·¬Ty → x≠y ]
Nights other than this night are different from it.

∀x[Nx·¬Tx → [∃y(Cy·Eyx) ∧ ∃y(My·Eyx)]] ∧
  ∀x[Nx·Tx → [∃y(My·Eyx) ∧ ∀y(Eyx → My)]]
On nights other than this one we eat both chametz and matzah;
on this night we eat matzah and only matzah.

∀x[Nx·¬Tx → ∀y(Hy → Eyx)] ∧ ∀x[Nx·Tx → ∃y(By·Eyx)]
On nights other than this one we eat all kinds of herbs;
on this night we eat bitter herbs.

∀x[Nx·¬Tx → ¬∃yDyx] ∧
  ∀x[Nx·Tx → ∃y∃z(Dyx·Dzx·(y≠z)·∀w[Dwx → (w=y ∨ w=z)])]
On nights other than this one we don't dip even once;
on this night we dip exactly twice.

∀x[Nx·¬Tx → (Sx v Rx)] ∧ ∀x[Nx·Tx → Rx]
On nights other than this one we eat either sitting up or reclining;
on this night we eat reclining.

∀x[Nx·¬Tx → Ox] ∧ ∀x[Nx·Tx → ¬Ox]
On nights other than this one we eat in an ordinary manner;
on this night we eat with special ceremony.

Intended interpretations:
Nx:  x is a night
Tx:  x occurs today
Cy:  y is chametz
My:  y is matzo
Hy:  y is an herb
By:  y is bitter herbs
Eyx:  we eat y during x
Dyx:  y is a dipping during x
Sx:  we eat sitting up on x
Rx:  we eat reclining on x
Ox:  we eat in an ordinary manner on x

Correction provided by: Larry Denenberg; Newton, MA
PhD from Harvard University in Applied Mathematics, whose thesis was on Computational Logic.

© Copyright Spiegel-Stein Publishing