# How to construct a conservative extension of classical logic that intuitionistic logic can be translated into?

Is there a canonical way to "embed" a system like intuitionistic logic inside classical logic ... or, equivalently, to extend classical logic with extra logical symbols so that a fragment of the extended system is "isomorphic" in some sense to another system?

The goal is to come up with a system $$S$$ that a formula in intuitionistic logic can be translated into. It should then be possible to negate the formula in $$S$$ and derive $$\bot$$ in $$S$$ . The act of doing that should be equivalent to proving the original formula in intuitionistic logic.

This is similar to double negation translation from classical logic to intuitionistic logic where $$\varphi$$ is a classical taugology iff $$(\varphi \to \bot) \to \bot$$ is an intuitionistic tautology.

Let's use $$\land, \lor, \lnot, \bot$$ for the connectives of classical logic and $$+, \times, \to, \bot$$ for the connectives of intuitionistic logic. So right out of the gate we identify classical falsehood and intuitionistic falsehood.

Classically, we have the following inference rules

And $$\frac{A \land B}{A}$$ , $$\frac{A \land B}{B}$$ , $$\frac{A\;\;\;B}{A \land B}$$

Or $$\frac{A}{A\lor B}$$, $$\frac{B}{A \lor B}$$, $$\frac{A\lor B\;\;\;\lnot A}{B}$$, $$\frac{A \lor B\;\;\;\lnot B}{A}$$

Not $$\frac{A}{\lnot\lnot A}$$, $$\frac{\lnot\lnot A}{A}$$

LNC $$\frac{A\;\;\;\;\lnot A}{\bot}$$

EFQ $$\frac{\bot}{A}$$

Truth $$\frac{\;\;}{\lnot \bot}$$

Intuitionistically we have the following inference rules

Product $$\frac{A\times B}{A}$$, $$\frac{A \times B}{B}$$, $$\frac{A\;\;\;B}{A \times B}$$

Sum $$\frac{A}{A+B}$$, $$\frac{B}{A+B}$$, $$\frac{A+B\;\;\;A\to C\;\;\;B \to C}{C}$$

Function $$\frac{}{A \to A}$$, $$\frac{A}{B \to A}$$, $$\frac{A \to B\;\;\;A}{B}$$

EFQ $$\frac{\bot}{A}$$

If we just take the union of the inference rules, we know something about the connection between various connectives (for instance that $$(A \land B) \iff (A \times B)$$).

But for other pairs of analogous connectives we have some choices to make. In particular, should it be the case that $$(A \lor B)$$ is equivalent to $$(A + B)$$ ?

It's possible to identify them and create a new extended theory. Here's a model of the theory to motivate it.

To make the model, let's borrow the Heyting algebra used for intuitionistic logic. This algebra is defined on the standard topology of the reals, but we can take the interior of any subset of $$\mathbb{R}$$, so let's expand to domain to all subsets of $$\mathbb{R}$$, denoted $$\mathfrak{R}$$ . Expanding the domain to include every subset of $$\mathbb{R}$$ no matter how pathological might break the model; I don't know for certain that it doesn't break the model.

Let $$[\cdot]$$ be a map from the set of well-formed formulas to $$\mathfrak{R}$$ . The map is constrained to respect the connectives in the following way.

$$[\bot] \stackrel{df}{=} \emptyset \tag{1}$$ $$[A \land B] \stackrel{df}{=} [A] \cap [B] \tag{2}$$ $$[A \times B] \stackrel{df}{=} [A] \cap [B] \tag{3}$$ $$[A \lor B] \stackrel{df}{=} [A] \cup [B] \tag{4}$$ $$[A + B] \stackrel{df}{=} [A] \cup [B] \tag{5}$$ $$[A \to B] \stackrel{df}{=} \mathrm{int}((\mathbb{R} \setminus [A]) \cup [B]) \tag{6}$$ $$[\lnot A] \stackrel{df}{=} \mathbb{R} \setminus [A] \tag{7}$$

So, this is kind of nice. Using intuitionistic implication $$\to$$ shaves off the boundaries of sets and classical negation doesn't.

We've also managed to construct a minimally extended classical logic with a single new connective $$\to$$ , corresponding to intuitionistic implication.

So, using the language of our model, it's easy to see why $$\lnot(A \lor (A \to \bot))$$ is not a tautology.

$$(A \cup \mathrm{int}(A^\complement))^\complement \tag{8}$$ $$A ^ \complement \cap \mathrm{int}(A^\complement)^\complement \tag{9}$$ $$A^\complement \cap \overline{A} \tag{10}$$

(10) is not quite the boundary, but it isn't guaranteed to be empty either, so it isn't a tautology. I'm not sure how to make this argument in classical logic extended with $$\to$$ since I don't have symbols for closure. This suggests that there are probably additional axioms that need to be added describing the relationship between $$\to$$ and the classical connectives.

So, I guess my question is: is there a unique or canonical or somehow preferred way of extended a logic so that a subset of it is "isomorphic" in some sense to another logic?

And, is classical logic extended with intuitionistic $$\to$$, as vaguely sketched above, a bona fide conservative extension of classical logic with a "mapping" of some kind from intuitionistic logic into it?

If it is, is there some notion in which it's the "smallest" extension to classical logic with this property?

• Your question is rather open and unclear. However, it is known that intuitionistic disjunction cannot be defined in terms of intutionistic negation, conjunction and implication. This dooms any attempt to interpret intuitionistic propositional logic in classical propositional logic. – Rob Arthan Nov 28 '18 at 0:17
• @RobArthan I'll try to clarify it. I'm not trying to map intuitionistic prop. logic into classical prop. logic itself. I'm asking if there's a way to characterize the "smallest possible conservative extension" of classical logic that intuitionistic logic could be mapped into. For example, linear logic contains fragments that are "isomorphic" in some sense to both classical prop. logic and intuititionistic prop. logic. But linear logic has many connectives that aren't needed to encode either classical or intuitionistic logic. – Gregory Nisbet Nov 28 '18 at 0:22
• It remains unclear what you are asking for: you seem to be confused about "fragments of a logic' (logical weakenings) and "exensions of logic" (logical strengthenings). Try to tell us precisely what properties a mapping of intuitionistic logic into classical logic of the kind you are interested in would enjoy. – Rob Arthan Nov 28 '18 at 0:39
• Sorry. Basically, I'm after a system $S$ that has double negation elimination and a way of encoding intuitionistic logic ($I$) into it. I want to be able to take an arbitrary statement in intuitionistic logic, translate it to $S$, negate it in $S$, and then derive $\bot$ in $S$ as a way of proving the original statement in $I$. The mapping from $S$ to $I$ definitely won't send negation in $I$ to negation in $S$ . I'm after something similar to the double negation translation going from classical ($C$) to $I$ where proving $\varphi$ in $C$ is equivalent to proving $\lnot\lnot\varphi$ in $I$. – Gregory Nisbet Nov 28 '18 at 0:52
• Please edit your question to make that clear. Given that the decision problem for intuitionistic propositional logic is PSPACE-complete while the decision problem for classical propositional logic is NP-complete, any such encoding would have to be have worse than polynomial complexity unless PSPACE=NP. – Rob Arthan Nov 28 '18 at 1:19