alternative exists_unfolding

[wdcraft01]

@wwitzel .

The current state of the Forall() and Exists() quantifiers in logic/booleans/quantification makes it surprisingly difficult and awkward to translate between an existential such as:

$\exists_{x}\big(\lnot P(x)\big)$

and the equivalent universal:

$\lnot\big(\forall_{x}P(x)\big)$,

with the system currently offering Exists.unfold() and Exists.conclude() methods that depend on the following unfolding and folding theorems:

I propose to add analogous theorems along the lines of:

exists_not_unfolding: $\forall_{n \in \mathbb{N}^{+}}\big[ \forall_{P, Q} \big([\exists_{x_1, \ldots, x_n | Q(x_1, \ldots, x_n)}\lnot P(x_1, \ldots, x_n)] \Rightarrow \big(\lnot\big[\forall_{x_1, \ldots, x_n | Q(x_1, \ldots, x_n)} P(x_1, \ldots, x_n)\big]\big)\big)\big]$

exists_not_folding: $\forall_{n \in \mathbb{N}^{+}}\big[ \forall_{P, Q | \big(\lnot\big[\forall_{x_1, \ldots, x_n | Q(x_1, \ldots, x_n)} P(x_1, \ldots, x_n)\big]\big)} \big(\exists_{x_1, \ldots, x_n | Q(x_1, \ldots, x_n)}\lnot P(x_1, \ldots, x_n)]\big)\big]$

along with new Exists() class methods analogous to the current Exists().unfold and Exists().conclude().

[wdcraft01]

The current Exists().unfold() method is actually problematic right now as well, with the theorem instantiation process apparently assuming that the existential will have an explicit condition. For example, given the simple existential claim $\exists_{x}P(x)$, the current code has the following step:

_P = Lambda(_x, self.operand.body.value),

but the self.operand.body produces simply P(x) instead of a conditional, and thus it has no value attribute. It's not clear why we can't simply take _P = Lambda(_x, self.instance_expr) instead. It's possible some of the Exists() class infrastructure has changed over time or that some of this code simply hadn't yet been tested.