Uppsala University Period 1/2 Matematiska Institutionen Ht 1998 Anton Setzer

“Constructive Mathematics and Lambda Calculus” Additional problems

Problem 1 Decide, which of the following implications are constructively valid (by giving, in case of nonvalidity, Brouwerian counter examples or other convincing arguments).

a) (¬¬A→A)→(A ∨ ¬A).

b) (A ∨ ¬A)→(¬¬A→A).

c) (A→∃x.B(x))→∃x(A→B(x)).