Kurt Gödel introduced a mapping from Intuitionism to Classical S4 Modal Logic as follows:
$A’=\Box A$ where $A$ is a positive atomic formula.
$(\sim A)’=\Box \sim (A’)$
$(A \land B)’=A’ \land B’$
$(A \lor B)’=A’ \lor B’$
$(A \implies B)’=\Box (A’ \implies B’)$
By adding the following:
$(\neg A)’=\sim \Box (A’)$,
one obtains a propositional logic that roughly accounts for distinct negations, namely “impossibility” and “unnecessity” respectively.
Further, it is known that Intuitionistic Logic is equivalent to Heyting Algebra, Simply-Typed Lambda Calculus, and other mathematical structures/systems. Are there mathematical structures/systems that already correspond to this logic, and what might it take to transform e.g., Heyting Algebra into an algebra sufficient for this logic?
Note that though this logic is a naive extension of Intuitionism, it is non-constructive since the Law of the Excluded Middle is provable for the new negation operator.
Best Answer
You notice that for any propositional formula in the logical language $(\wedge, \vee, \rightarrow, \sim)$ (where $\sim$ denotes the usual negation), we have $\vdash_{IPC} \varphi$ precisely if $\vdash_{S4} \varphi'$.
By analogy, you consider a logical system $p$, defined in such a way that for any propositional formula $\varphi$ in the extended logical language $(\wedge, \vee, \rightarrow, \sim, \neg)$, we have $\vdash_p \varphi$ precisely if $\vdash_{S4} \varphi'$.
You claim that the system $p$ constitutes "a naive extension of" intuitionistic logic. As we shall see, this claim fails, and no reasonable algebraic structure or system can correspond to $p$. In particular, it's not possible to extend the variety of Heyting algebras into a semantics for $p$.
I. Why is your system not an extension of intuitionistic propositional logic $IPC$? Given any propositional formulas $\varphi, \psi$ of intuitionistic logic, we always have $\vdash_{IPC} (\varphi \rightarrow \:\sim\!\psi) \rightarrow (\psi \rightarrow \:\sim\!\varphi)$. However, we don't have $\vdash_p (\varphi \rightarrow\:\sim\!\psi) \rightarrow (\psi \rightarrow \:\sim\!\varphi)$.
Set $\varphi$ to the atomic formula $A$, and $\psi$ to the formula $\neg A$. Applying the $'$-translation to the resulting $p$-formula $ (A \rightarrow \:\sim\!\neg A) \rightarrow (\neg A \rightarrow \:\sim\! A)$ gives us the $S4$-formula $$\Box (\Box (\Box A \rightarrow \Box (\sim \sim\! \Box \Box A)) \rightarrow \Box (\sim\! \Box \Box A \rightarrow \Box \!\sim\! \Box A))$$ which one cannot actually prove in $S4$! It fails because generally $\sim\!\Box x$ does not imply $\Box \!\sim\! \Box x$.
This means that, unlike intuitionistic logic, the system $p$ does not enjoy closure under substitution: from $\vdash_p \varphi$ you cannot conclude $\vdash_p \varphi[A := \psi]$.
The lack of closure under substitution makes the system $p$ extremely ill-behaved: in particular, it rules out the existence of any sort of sound/complete algebraic semantics for $p$.
II. What happens if we try to fix the bad behavior by taking the "closure" $q$ of system $p$ under variable substitution? We can do this, but we get something really boring: classical propositional logic. I will show this using a model-theoretic argument, but with a little effort one can turn the argument below into a direct $q$-proof of excluded middle for ordinary negation.
As you noted, your system has $\vdash_p A \vee \neg A$, so the closed system has $\vdash_q \varphi \vee \neg \varphi$ for all $\varphi$.
Moreover, I claim that $\vdash_p \sim\!\neg P \rightarrow P$ also holds, since the $'$-translation gives
$$(\sim\!\neg P)' = \Box \sim (\neg P)' = \Box\sim \sim \Box P' = \Box\!\sim \sim\!\Box \Box P$$
and consequently
$$(\sim\!\neg P \rightarrow P)' = \Box ((\sim\!\neg P)' \rightarrow P') = \Box (\Box\!\sim \sim\!\Box \Box P \rightarrow \Box P) $$
as well. Now, one can establish $\vdash_{S4} \Box (\Box\!\sim \sim\!\Box \Box P \rightarrow \Box P)$ e.g. by using the necessitation rule, then applying double-negation elimination to get rid of $\sim\sim$, and using the fact that $\Box = \Box\Box$ in S4. A nigh-identical argument gives $\vdash_p P \rightarrow \sim\!\neg P$ as well. It follows that $\vdash_q \varphi \leftrightarrow \sim\!\neg \varphi$ for all $q$-formulas $\varphi$.
Consequently, a model of $q$ would have to be a Heyting algebra $H$ equipped with a unary operator $\neg$ satisfying both $x \vee \neg x = \top$ and $\neg x \rightarrow \bot = x$ for all $x \in H$. I now show that all such Heyting algebras are Boolean algebras.
It suffices to show that $\neg x = x \rightarrow \bot$, since at that point $x \vee \neg x = \top$ will imply excluded middle.
First we show that $\neg x \leq x \rightarrow \bot$ by proving $\neg x \rightarrow (x \rightarrow \bot) = \top$. We can prove this as follows: $\neg x \rightarrow (x \rightarrow \bot) = x \rightarrow (\neg x \rightarrow \bot) = x \rightarrow x = \top$.
For the other direction $y \rightarrow \bot \leq \neg y$, notice that we already know $\neg x \leq x \rightarrow \bot$, so we can set $x = \neg y$ to conclude $\neg\neg y \leq \neg y \rightarrow \bot = y$. But if $\neg \neg y \leq y$, then by negating the inequality $y \rightarrow \bot \leq \neg\neg y \rightarrow \bot = \neg y$. Both inequalities hold, so we get that $y \rightarrow \bot = \neg y$ as claimed. Therefore, all models of $q$ are Boolean algebras.
III. How did I know in advance that your system was going to be ill-behaved? Well, generally, Heyting algebras describe how the open subsets of a topological space behave under the finitary operations of intersection, union, and "interior of the complement". The algebras corresponding to modal logic $S4$, so-called interior algebras, describe how all subsets of a topological space behave under the finitary operations of intersection, union, complement, and interior.
An open subset of a topological space is precisely a subset that coincides with its own interior. This is what makes Gödel's translation work: we simply treat the variables of intuitionistic logic as variables ranging over open sets inside the algebra of all sets.
Your attempted translation of the new operation $\neg$ breaks with this nice correspondence: it insists on translating $A$ as the complement ($\sim$) of an open set ($\Box$). But unfortunately, the complement of an open set is very rarely open! It would have required a remarkable coincidence to get something that respects substitution out of this.
After making this observation, all I had to do was look for a bad substitution instance. Once I had the substitution instance in hand, it quickly led me to the proof of Part II as well.