Under the propositions-as-types paradigms, a proposition is identified with the type of all its proofs. From a more classical perspective (and assuming the full-blown axiom of choice), it sometimes makes sense to think of propositions as representing not mere truthvalues, but rather, sets of witnesses. We can then define that a proposition is true iff it represents a non-empty set.
For example, a proposition of the form
$$\exists x \in X.P(x)$$
could be identified with the set of all $x \in X$ such that $P(x).$ Along a similar vein, a proposition of the form
$$\forall x \in X, \exists y \in Y . P(x,y)$$
could be identified with the set of all functions $y:X \rightarrow Y$ such that $P(x,y(x))$ holds for all $x \in X$.
More generally, to work out what set is represented by a proposition, we can:
- Convert to prenex normal form.
- Shuffle all the existential quantifiers left across the universal quantifiers. For example, a formula of the form $(\forall x \in X)(\exists y \in Y)(\varphi)$ would be transformed into a formula of the form $(\exists y : X \rightarrow Y)(\forall x \in X)([y(x)/x]\varphi)$. Do this until all the existential quantifiers are at the left-most position. Compare with Skolem normal form.
- Replace the existential quantifiers with set abstraction. e.g. $(\exists x \in X)(\forall y \in Y)(\varphi)$ would become $\{x \in X \mid (\forall y \in Y)(\varphi)\}.$
Caveat. I'm not sure this actually makes sense. In particular, if there are many different ways of transforming a formula into prenex normal form, then perhaps these correspond to different sets.
Question 0. Does this suggestion fall prey to the aforementioned caveat? If so, I'd like to see an explicit example of the problem.
Question 1. Have any authors suggested anything like this? If so, I'd appreciate a link or reference.