Exercises for Chapter 6, part 2

Use the EXISTSi and EXISTSe rules to prove these sequents. Use the Natural-deduction-proof-checker tool, and submit your answers within a zipped folder.

1. F(charlie), FORALLx(F(x) -> G(x)) |- EXISTSx( F(x) ^ G(x))
(some intuition: F == healthy; G == happy)

2. FORALLx (F(x) -> (EXISTSy H(y,x))), EXISTSx F(x) |- EXISTSxEXISTSy H(y,x)
(some intution: F == hasAjob; H == isBossOf)

3. EXISTSx(F(x) ^ G(x)) |- (EXISTSy F(y)) ^ (EXISTSz G(z))
(The converse cannot be proved: Let F == healthy; G == happy. Perhaps there are two people, one healthy and one happy, but no one is both healthy and happy at the same time.)

4. EXISTSx F(x) |- ~(FORALLx ~F(x))
(some intuition: F == isLeftHanded)