LESSWRONG
LW

4049
ruv
0010
Message
Dialogue
Subscribe

Posts

Sorted by New

Wikitag Contributions

Comments

Sorted by
Newest
No posts to display.
No wikitag contributions to display.
Basic building blocks of dependent type theory
ruv2d10

a logic formula like this:

∀x(x∉A∨x∈B)


At the first glance, it seems like the law of excluded middle is implied here (i.e., for any x, it either does not belong to A or belongs to A), and that's a typo. Then it should probably read:

  ∀𝑥(𝑥∉𝐀 ∨ 𝑥∈𝐀)

(i.e., "𝐀" instead of "𝐁")
 

Reply