Allow nested negation and universal quantification in rules about typeql HOT 3 OPEN

@cxdorn

from typeql.

From "Logic for Mathematicians" by A.G. Hamilton, sec. 3.2, p. 51:

We have seen that the existential quantifier can be defined in terms of the universal quantifier, so we need have only one of them.

from typeql.

(I realize my earlier thumbs up reaction wasn't very helpful, but I actually wasn't sure whether there was a question implied here!)

With regards to the question: can we do everything with 'exists' that we can do with 'forall'?

• Propositionally (i.e. for truth values) yes. $\forall x. \phi(x)$ and $\neg \exists x. \neg \phi(x)$ are equi-derivable in predicate logic (if you assume the axiom of excluded middle $\neg \neg \phi(x) \Rightarrow \phi(x)$, which holds in the 'negation as failure' semantics we are using).
• Type-theoretically (i.e. for data instances) no. The way we interpret an existence statement in TypeQL is as a query for all data instances of that statement. If we write $\exists (y : T). \psi(y)$ we want to find all $y$ of type $T$ with property $\psi(y)$. Similarly, a 'forall' statement can query for data instances. For instance, for the query $\forall (x : S). \{y : T; \phi(x,y) \}$ (by which I mean $\forall (x : S). \exists (y : T). \phi(x,y)$ ), if we'd really list all data instances to that statement, we would want to find all functions of data instances $f : S \to T$ such that $\phi(x, f(x))$ holds true. Whereas for the query $\neg \exists (x : S). \neg \exists (y : T). \phi(x,y)$ we'd not return any witnesses, but just a truth value, namely, whether or not the statement $\exists (x : S). \neg \exists (y : T). \phi(x,y)$ has a witness.

But function spaces are generally way too big, so I don't think we'd ever want to implement forall in a data instance sense.

from typeql.