Use the Natural-deduction-proof-checker tool to prove your answers to the following questions, and submit your answers to K-State Online in a zipped folder.
1. In a domain of happy people, we have these laws: (i) if someone likes you, you like them back;
(ii) if someone is kind, cindy likes them. We can prove in this domain that when chris is kind, chris also likes cindy.
Show this by a proof of this sequent:
FORALLyFORALLz (Flikes(y,z) -> Flikes(z,y)), FORALLx(Fkind(x) -> Flikes(cindy,x)) |- Fkind(chris) -> Flikes(chris,cindy)
Use FORALLe along with ->e.
2.
"Forall" and "and" interact nicely with each other. Prove this:
FORALLz F(z), FORALLx G(x) |- FORALLy(F(y) ^ G(y))
UseFORALLi and FORALLe. (By the way, it is easy to prove the converse result: FORALLy(F(y) ^ G(y)) |- (FORALLz F(z)) ^ (FORALLx G(x)), but you don't have to just now.)
3.
"Forall" and "not" interact in just one direction (prove it):
FORALLy ~F(y) |- ~(FORALLx F(x))
Say that F means ``has brown eyes.'' How does the above sequent read in English words? Can we use our logic rules to prove the converse claim: ~(FORALLx F(x)) |- FORALLy ~F(y) ? Why not? Think about this (say that F means ``has brown eyes''); you don't need to submit an answer to grade.
4.
"Forall" and "or" interact in just this one direction (prove it):
(FORALLx F(x)) v (FORALLx G(x)) |- FORALLx(F(x) v G(x))
You cannot prove the converse. Here's why: Say that F means ``is left-handed'' and G means ``is right-handed.'' The formula, FORALLx(F(x) v G(x)) merely says everyone is either left- or right-handed. But does this guarantee that (FORALLx F(x)) v (FORALLx G(x))? Why not? Think about this; you don't need to submit an answer to grade.