Exercise 1 Which of the following implications are valid in intuitionistic logic ? Give either a tableau proof or a counterexample.
(a) cp a f -> f a <p
(b) y/^ ((9 a i//) vi//)
(c) (--f -»• (<p -»• f)
(d) 9 -> —<p
(e) ((<pAf)vf)^f
(f) —9 9
(g)
(h) ->(->f a -.1//) -»• (<p v 1//) (This one is tricky.)
(i) 9 -»• 3x<p (j) Vx<f> -> cp
(k) VxR(x,x) ^ Vx3yR(f(x),y)
(1) 3x(<p v 1//) -»• 3x<p v 3xi//
(m) 3xcp v 3xi// -»■ 3x(<p v 1//)
(n) Vx<p a Vxi// —>• Vx(<p a 1//)
(o) Vx(<p a 1//) -»• Vx<p a Vxi//
(p) VxV;/[<p(x) «-»• 9(7)] a 3x<p(x) -»• Vx<p(x)
1