# Classical and intuitionistic propositional logic in the propositions-as-sets interpretation

I'm looking for a way to describe classical and intuitionistic propositional logic such that the transition between the two seems natural and intuitive. I came up with the following but I'm unsure if it's actual true.

Just like the propositions-as-types interpretation for intuitionistic logic, one can give a propositions-as-sets interpretation for classical logic. If the logical language consists of $\land,\lor,\Rightarrow,\bot$, we can interpret these symbols as the set operations $\times,\oplus,\rightarrow,\emptyset$ and a propositional formula $\phi[X_1,\dots,X_n]$ is valid iff we can prove (in set theory enriched by $\times,\oplus,\rightarrow,\emptyset$) that $\exists Y.Y\in\tilde\phi[X_1,\dots,X_n]$ for the corresponding set theoretical term $\tilde\phi$. (Since the $X_i$ appear free in $\tilde\phi$, we can also prove $\forall X_1,\dots,X_n.\exists Y.Y\in\tilde\phi[X_1,\dots,X_n]$ then.)

I'm pretty sure that this part is correct, since basically not much is done, one only asks about emptyness of sets and we know that $X\times Y$ is empty iff $X$ or $Y$ is, $X\oplus Y$ is empty iff $X$ and $Y$ is, $X\rightarrow Y$ is empty iff $X$ but not $Y$ is such as $\emptyset$ is empty.

Now I feel like one could say that the propositions which are intuitionistically true are exactly those where we find canonical inhabitants of the respective set. For example, we can show $\exists Y.Y\in X\oplus(X\rightarrow\emptyset)$ but there is no canonical choice for such $Y$. I thought maybe one could make precise what is meant by 'canonical inhabitant of $\phi$' by saying there exists a (set theoretical) formula $\chi[X_1,\dots,X_n,Y]$ such that we can prove: $$(\exists! Y.\chi[X_1,\dots,X_n,Y])\land(\forall Y.\chi[X_1,\dots,X_n,Y]\Rightarrow Y\in\tilde\phi[X_1,\dots,X_n])$$ (Since the $X_i$ appear free in the formula, as before the $Y$ can depend on them.)

Is there some theory along these lines, if it makes any sense at all?

EDIT: This conjecture is not true, take $\phi[X]:=\bot\Rightarrow X$. Then clearly $\tilde\phi[X]=\emptyset\rightarrow X$ equals $\{\emptyset\}$ (no matter what $X$ is because $\emptyset$ is an initial object in the category of sets) so it contains a very canonical inhabitant (i.e. this inhabitant doesn't even depend on $X$).

But maybe it remains true if we do not translate $\bot$ to $\emptyset$ but just some unspecified fresh variable $X_\bot$ and place the condition $X_\bot\subseteq X_i$ over everything?

• I'm not sure I agree with this, what are the occupants of these sets? If you're thinking of those being programs then you've got realizability theory and there are a lot of interesting insights about computation and classical logic. If you just meant derivations in a formal system than this procedure will work for any logic and there isn't really a valid notion of canonicity a prior. In any case there should not be a derivation in intuitionistic logic of $\forall A. A \vee \neg A$ so there should be no occupant of that set, canonical or not. – jozefg Dec 2 '15 at 17:09
• Ps your notion of canonicity is the uniform quantification operator. It was defined first in the context of computational type theory by the Nuprl project. I don't have a good citation off hand though.. – jozefg Dec 2 '15 at 17:12
• Hm, I just tried find some picture (not necessarily a theoretical useful one, more like one which helps me with my intuition) in which classical and intuitionistic logic lie as close as possible together. So, I know that my picture does not correspond to the classical propositions-as-sets picture inspired by type theory, where $A\lor\neg A$ indeed contains no inhabitant, I like to call this one propositions-as-types, to underline the difference, if that makes any sense... – fweth Dec 2 '15 at 17:16

There is a topological interpretation where propositions are open sets and negation is interior of the complement. The rest is the same as in classical logic. $\wedge$ is intersection, $\vee$ is union, and $\implies$ is $\subset$, tautology is the whole set, impossibility is the empty set.
Witnesses to $\exists x$ do not need to be unique in constructive mathematics. They just need to not depend on perfect true/false distinctions and coverings by overlapping open sets model that for disjunction. The rest is the same with and without excluded middle.