-
* How shall we handle \[[∃x]]? As we said, GS&V really tell us how to interpret \[[∃xPx]], but for our purposes, what they say about this can be broken naturally into two pieces, such that we represent the update of our starting set `u` with \[[∃xPx]] as:
<pre><code>u >>= \[[∃x]] >>= \[[Px]]
That would be the meaning of \[[∃]], which we'd use like this:
- <pre><code>\[[∃]] \[[Q]]
+ <pre><code>\[[∃]] ( \[[Q]] )
</code></pre>
or this: