nLab
double negation translation

Contents

Idea

The double negation translation is a method for converting propositions valid in classical logic into propositions valid in intuitionistic logic. It was discovered independently by a number of mathematicians including Kurt Gödel, Gerhard Gentzen, and Andrey Kolmogorov, and is also called the Gödel–Gentzen negative translation.

Construction

The traditional descriptions are highly syntactic, but can be motivated by recalling some conceptual relationships between Boolean algebras (which are algebras for classical propositional logic) and Heyting algebras (which are algebras for intuitionistic propositional logic).

Propositional case

Recall from the article Heyting algebra that the left adjoint FF to the forgetful functor

U:BoolHeytU \colon Bool \to Heyt

is given objectwise by taking a Heyting algebra LL to the poset L ¬¬L_{\neg\neg} of regular elements xLx \in L, i.e., those satisfying x=¬¬xx = \neg \neg x. It was shown that L ¬¬L_{\neg\neg} is a Boolean algebra, and ¬¬:LL ¬¬\neg \neg \colon L \to L_{\neg\neg} is a Heyting algebra homomorphism which is universal among Heyting algebra maps LUBL \to U B into Boolean algebras.

In particular, if Heyt(S)Heyt(S) is the free Heyting algebra on a set of variables SS, it follows by composing left adjoints

SetfreeHeytFBoolSet \stackrel{free}{\to} Heyt \stackrel{F}{\to} Bool

that Heyt(S) ¬¬Heyt(S)_{\neg\neg} is the free Boolean algebra on SS.

Furthermore, it was shown in Heyting algebra that for Heyting algebras LL,

  • ¬¬:LL\neg\neg \colon L \to L preserves finite meets;

  • ¬¬:LL\neg\neg \colon L \to L preserves the implication operation \Rightarrow.

Consequently, the inclusion of regular elements L ¬¬LL_{\neg\neg} \to L also preserves meets and implications, strictly. This gives the following result.

Glivenko’s Theorem

If pqp \Rightarrow q is a tautology in classical propositional logic, then (¬¬p)(¬¬q)(\neg \neg p) \Rightarrow (\neg \neg q) is a tautology in intuitionistic propositional logic, and conversely.

Proof

Here pp and qq are term expressions in variables x iSx_i \in S over the signature (0,1,,,)(0, 1, \vee, \wedge, \Rightarrow). To say pqp \Rightarrow q is a classical tautology means that 1(pq)1 \leq (p \Rightarrow q) holds when interpreted in Bool(S)Bool(S). But since Bool(S)=Heyt(S) ¬¬Bool(S) = Heyt(S)_{\neg\neg}, this is equivalent to saying that

1¬¬(pq)=(¬¬p)(¬¬q)1 \leq \neg\neg(p \Rightarrow q) = (\neg\neg p) \Rightarrow (\neg\neg q)

when interpreted in Heyt(S)Heyt(S), which is to say that (¬¬p)(¬¬q)(\neg \neg p) \Rightarrow (\neg\neg q) is an intuitionistic tautology.

Continuing this thought: the join \vee in Bool(S)=Heyt ¬¬Bool(S) = Heyt_{\neg\neg} is computed as

a Boolb=¬¬(a Heytb)a \vee_{Bool} b = \neg\neg(a \vee_{Heyt} b)

since ¬¬:Heyt(S)Heyt(S) ¬¬\neg\neg \colon Heyt(S) \to Heyt(S)_{\neg\neg} preserves joins (it is a left adjoint). Putting all this together, because ¬¬:Heyt(S)Heyt(S) ¬¬\neg\neg \colon Heyt(S) \to Heyt(S)_{\neg\neg} preserves Heyting algebra structure, we arrive the following syntactic translation.

Definition

The double-negation translation pp Np \mapsto p^{N} on term expressions in the theory of Heyting algebras LL is defined by induction as follows.

  • x N=¬¬xx^N = \neg\neg x for variables xx.

  • 0 N=00^N = 0 (since ¬¬:LL\neg\neg \colon L \to L preserves 00)

  • 1 N=11^N = 1 (since ¬¬:LL\neg\neg \colon L \to L preserves 11)

  • (pq) N=p Nq N(p \wedge q)^N = p^N \wedge q^N (since ¬¬:LL\neg\neg \colon L \to L preserves the meet operation)

  • (pq) N=p Nq N(p \Rightarrow q)^N = p^N \Rightarrow q^N (since ¬¬:LL\neg\neg \colon L \to L preserves the implication operation)

  • (pq) N=¬¬(p Nq N)(p \vee q)^N = \neg\neg(p^N \vee q^N).

Thus, by Glivenko’s theorem, pp is a classical tautology if and only if p Np^N is an intuitionistic tautology. This result may be extended to theories as well: suppose LL is an intuitionistic theory or Heyting algebra, given by a presentation as a coequalizer in HeytHeyt:

Heyt(T)Heyt(S)L.Heyt(T) \stackrel{\to}{\to} Heyt(S) \to L.

Then, since the functor LL ¬¬L \mapsto L_{\neg\neg} is a left adjoint, it takes this coequalizer to a coequalizer

Bool(T)Bool(S)L ¬¬Bool(T) \stackrel{\to}{\to} Bool(S) \to L_{\neg\neg}

so that an term expression pp is a theorem in the classical theory L ¬¬L_{\neg\neg} if and only if p Np^N is a theorem in the intuitionistic theory LL.

First-order case

Higher-order case

The basic idea here is that any topos EE gives rise to a Boolean topos E ¬¬E_{\neg\neg}.

Revised on July 31, 2012 23:49:05 by Toby Bartels (98.16.162.107)