search

bor0 / gidti

Book: Introduction to Dependent Types with Idris
https://leanpub.com/gidti
Other
76 stars 4 forks source link

Chapter 2: More info for quantifiers #19

Closed nbloomf closed 5 years ago

nbloomf commented 6 years ago

Section 2.1.2 on quantifiers is a little light on examples and details, particularly for the existential quantifier. This is an important and tricky topic that probably warrants some more fleshing out.

For instance, the negation rules for quantifiers are what they are for a good and intuitive reason.

But also we need to be careful with the quantifiers in intuitionistic logic: $\lnot \forall x . P \Rightarrow \exists x . \lnot P$ is not intuitionistically valid. This makes sense if we remember that intuitionistic truth means constructible, and we can imagine a case where we can construct evidence that P(x) does not hold for any $x$ but can't construct evidence that ~P(x) for any particular x. Similarly, deMorgan's laws are intuitionistically complicated. The bottom of page 6 in this paper says more about this.

bor0 commented 5 years ago

Partially fixed in 38547539bb10492d4d4c45d28b785d679d59f5e5, don't want to distract too much :)