CIS301 Exercises for Chapter 6, part 2

Use the Natural-deduction-proof-checker to prove the following sequents, and upload your answers in a zipped folder to K-State Online.

1. FORALLx(F(x) —> G(x)), F(chris) |- EXISTSx(F(x) ^ G(x))
(use EXISTSi, not EXISTSe)

2. EXISTSx(F(x) —> G(x)), FORALLy F(y) |- EXISTSz G(z)
(Use EXISTSi and EXISTSe. )

3. EXISTSx F(x) |- ~(FORALLx ~F(x))

4. FORALLx(F(x) —> EXISTSy G(x,y)) |- (EXISTSz F(z)) -> (EXISTSz EXISTSy G(z,y))