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?

  • $\begingroup$ 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. $\endgroup$ – jozefg Dec 2 '15 at 17:09
  • $\begingroup$ 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.. $\endgroup$ – jozefg Dec 2 '15 at 17:12
  • $\begingroup$ 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... $\endgroup$ – 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.