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?
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.