For a name and formula , form the set of pairs with in the immediate domain of , a Boolean truth value, and some name satisfying . Full separation makes this a set, and intuitionistic collection gives a set of witness names covering all its pairs. A name with these witnesses in its domain collects the entire Boolean value of every existential assertion over , without selecting one witness whose value is top. No choice or maximum principle is used.
Articles by others on the same topic
There are currently no matching articles.