3.7 Exercises

[letrec]

Explicit requirement to use classical logic for section 2 exercises somewhat implies that section 1 exercises are meant to be proven constructively, which contradicts the section 3 suggestion to prove ¬(p ↔ ¬p) (listed under 1) without using classical logic.

[avigad]

I will just delete it from problem 1. Thanks.