Navigation – Plan du site
Logic and Philosophy of Science in Nancy (I)

Copies of Classical Logic in Intuitionistic Logic

Jaime Gaspar
p. 5-11

Résumé

La logique classique (la logique des mathématiques non-constructives) est plus forte que la logique intuitionniste (la logique des mathématiques constructives). Malgré cela, il existe des copies de la logique classique dans la logique intuitionniste. Toutes les copies habituellement trouvées dans la littérature sont les mêmes. Ce qui soulève la question suivante : la copie est-elle unique ? Nous répondons négativement en présentant trois copies différentes.

Haut de page

Notes de la rédaction

Financially supported by the French Fondation Sciences Mathématiques de Paris. This article is essentially a written version of a talk given at the 14th Congress of Logic, Methodology and Philosophy of Science (Nancy, France, 19–26 July 2011), reporting on results in a PhD thesis [Gaspar 2011, chap. 14] and in an article [Gaspar 2013].

Texte intégral

1 Philosophy

1.1 Non-constructive and constructive proofs

1Mathematicians commonly use an indirect method of proof called non-constructive proof: they prove the existence of an object without presenting (constructing) the object. However, many times they can also use a direct method of proof called constructive proof: to prove the existence of an object by presenting (constructing) the object.

2Definition 1

  • A non-constructive proof is a proof that proves the existence of an object without presenting the object.

  • A constructive proof is a proof that proves the existence of an object by presenting the object.

3From a logical point of view, a non-constructive proof uses the law of excluded middle while a constructive proof does not use the law of excluded middle.

4Definition 2. The law of excluded middle is the assertion “every statement is true or false”.

5To illustrate this discussion, let us see the usual example of a theorem with non-constructive and constructive proofs.

6Theorem 3. There are irrational numbers x and y such that xy is a rational number.

Non-constructive proof. By the law of excluded middle, Image 100002000000001F00000018175E2FFD.png is a rational number or an irrational number.

Case Image 100002000000001F00000018175E2FFD.png is a rational number. Let Image 100002000000002C00000013D5600A4A.png and Image 100002000000002D0000001353E721A5.png. Then x and y are irrational numbers such that Image 100002000000003F00000018BF19A09D.png is a rational number.

Case Image 100002000000001F00000018175E2FFD.png is an irrational number. Let Image 100002000000003800000019309CA7DB.png and Image 100002000000002D0000001353E721A5.png. Then x and y are irrational numbers such that xy = 2 is a rational number.

7Note that the above proof is non-constructive because the proof does not present x and y since the proof does not decide which case holds true. Also note that the proof uses the law of excluded middle.

Constructive proof. Let Image 100002000000003800000019309CA7DB.png and Image 100002000000002D0000001353E721A5.png. Then x (by the Gelfond-Schneider theorem) and y are irrational numbers such that xy = 2 is a rational number.

8Note that the above proof is constructive because the proof presents x and y. Also note that the proof does not use the law of excluded middle.

1.2 Constructivism

9We saw that mathematicians use both non-constructive and constructive proofs. There is a school of thought in philosophy of mathematics, called constructivism, which rejects non-constructive proofs in favour of constructive proofs.

10Definition 4. Constructivism is the philosophy of mathematics that insists on constructive proofs.

11Let us see some motivations for constructivism.

Philosophical motivations.

  • The more radical constructivists simply consider non-constructive proofs unsound. The less radical constructivists consider that non-constructive proofs may be sound, but not as sound as constructive proofs.

  • Some constructivists reject the mind-independent nature of mathematical objects. So for a mathematician to prove the existence of an object, he/she has to give existence to the object by constructing the object in his/her mind.

  • Non-constructivism puts the emphasis on truth (as in “every statement is true or false”), while constructivism puts the emphasis on justification (as in “we have a justification to believe that a statement is true, or we have a justification to believe that the statement is false”). Given an arbitrary statement, in general there is no justification to believe that the statement is true and no justification to believe that the statement is false, so a constructivist would not assert “every statement is true or false”, that is a constructivist rejects the law of excluded middle.

  • Non-constructivism does not differentiate between the quantifications ¬∀x¬ and ∃x, but constructivism is more refined because it differentiates between them:
    – ¬∀x¬ means the usual “there exists an x”;
    – ∃x has the stronger meaning of “there exists an x and we know x”.

Mathematical motivations.

12Constructive proofs are more informative than non-constructive proofs because they not only prove the existence of an object, but even give us an example of such an object.

  • We can use the constructive setting to study non-constructive principles. In the usual setting of mathematics, which includes non-constructive principles, there is no way to tell the difference between what results from the setting and what results from the non-constructive principles. But in a constructive setting we can isolate the role of non-constructive principles. For example, if we want to determine which theorems are implied by the axiom of choice, we need to do it in set theory without the axiom of choice.

  • There are several tools in mathematical logic that work fine for constructive proofs but not for non-constructive proofs. So in order to benefit from these tools we should move to a constructive setting. For example, the extraction of computational content using Gödel’s functional interpretation can always be done for constructive proofs but has restrictions for non-constructive proofs.

13Historical motivation.

  • Until the 19th century all proofs in mathematics were more or less constructive. Then in the second half of the 19th century there were introduced powerful, infinitary, abstract, non-constructive principles. These principles were already polemic at the time. Even worse, at the turn of the century there were discovered paradoxes related to these non-constructive principles. Then it was not only a question of what principles are acceptable, but even the consistency of mathematics was at stake. Constructivism proposes a solution to this crisis: to restrict ourselves to the safer constructive principles, which are less likely to produce paradoxes.

2 Mathematics

2.1 Classical and intuitionistic logics

14We saw that non-constructivism uses the law of excluded middle while constructivism does not use the law of excluded middle. Let us now formulate this idea in terms of logic.

  • Classical logic CL is (informally) the usual logic of mathematics including the law of excluded middle.

  • Intuitionistic logic IL is (informally) the usual logic of mathematics excluding the law of excluded middle.

15To be sure, CL corresponds to non-constructivism, and IL corresponds to constructivism.

16Now let us compare CL and IL. We can prove the following.

  • CL is strictly stronger than IL (that is there are theorems of CL that are not theorems of IL, but every theorem of IL is a theorem of CL).

  • CL is non-constructive (that is there are proofs in CL that cannot be turned into constructive proofs) while IL is constructive (that is every proof in IL can be turned into a constructive proof).

2.2 Copies

17To introduce the notion of a copy of classical logic in intuitionistic logic, first we need to introduce the notion of a negative translation.

18Defintion 6. A negative translation is a mapping N of formulas that embeds CL in IL in the sense of satisfying the following two conditions.

19Respecting provability. For all formulas A and sets Γ of formulas we have the implication CL + Γ ⊦ A ⇒ IL + ΓN ⊦ AN (where ΓN = {AN : A ∈ Γ});

20Faithfulness. For all formulas A we have CL ⊦ A ↔ AN.

21A copy of classical logic in intuitionistic logic is the image im N (the set of all formulas of the form AN) of a negative translation N (Gaspar 2011, para. 14.5), (Gaspar 2013, definition 1).

22Let us explain why it is fair to say that an image is a copy of classical logic in intuitionistic logic. From the definition of a negative translation we get the following equivalence:

$CL ⊦ A ↔ IL ⊦ AN.

23We can read this equivalence in the following way: the formulas AN in im N are mirroring in IL the behaviour of CL. So im N is a reflection, a copy, of classical logic in intuitionistic logic.

2.3 Question: is the copy unique?

24There are four negative translations usually found in the literature; they are due to Kolmogorov, Gödel-Gentzen, Kuroda and Krivine. The simplest one to describe is Kolmogorov’s negative translation: it simply double negates every subformula of a given formula.

25All the usual negative translations give the same copy: the negative fragment.

26Definition 7. The negative fragment NF is (essentially) the set of formulas without and ∃.

27The fact that all the usual negative translations give the same copy leads us to ask: is the copy unique?

28Here we should mention that when we say that two copies are equal, we do not mean “syntactically/literally equal” (that would be too strong and easily falsified); we mean “equal modulo IL” (that is “modulo identifying formulas that are provably equivalent in IL”).

2.4 Answer: no

29In the following theorem we show that the answer to our question is no by presenting three different copies.

30Theorem 8. Let us fix a formula F such that CL ⊦ ¬F but IL ⊬ ¬F (there are such formulas F). Then

  • NF

  • NF ∨ F = {AF : A ∈ NF}

  • NF[F/⊥] = {A[F/⊥] : A ∈ NF}

are pairwise different copies [Gaspar 2011, paragraph 14.10], (Gaspar 2013, lemma 7.1, theorem 8 and proposition 9].

31Sketch of the proof. We have to show the following three things.

32There is an F such that CL ⊦ ¬F but IL ⊬ ¬F. We can prove that F = ¬(∀x ¬¬P(x) → ∀xP(x)) (where P(x) is a unary predicate symbol) is in the desired conditions [Gaspar 2011, paragraph. 14.11.6], [Gaspar 2013 proof of lemma 7.1].

33NF, NF ∨ F and NF[F/⊥] are copies. Let K be Kolmogorov’s negative translation, AM = AKF and AN = AK[F/⊥] [Gaspar 2011, paragraph 14.8], [Gaspar 2013 definition 6]. We can prove that K, M and N are negative translations (here we use the hypothesis CL ⊦ ¬F) such that im K = NF, im M = NF ∨ F and im N = NF[F/⊥] [Gaspar 2011, paragraph 14.10], [Gaspar 2013 theorem 8]. This is pictured in figure 1.

34NF, NF ∨ F and NF[F/⊥] are different. We can prove that the images of two negative translations are equal if and only if the negative translations are pointwise equal (modulo IL) [Gaspar 2011, paragraph 14.11.4]. And we can prove that K, M and N are not pointwise equal by proving IL ⊬ ⊥M → ⊥K, IL ⊬ ⊥N → ⊥K and IL ⊬ PNPM (where P is a nullary predicate symbol different from ⊥) (here we use the hypothesis IL ⊬ ¬F) [Gaspar 2011, paragraph 14.11], [Gaspar 2013, proofs of theorem 8.3 and proposition 9].

Figure 1. The negative translations K, M and N, and the copies NF, NF ∨ F and NF[F/⊥].

Image 1000000000000247000000A988304019.png

Haut de page

Bibliographie

Gaspar, Jaime [2011], Proof Interpretations: Theoretical and Practical Aspects, Ph.D. thesis, Technical University of Darmstadt, Germany.

— [2013], Negative translations not intuitionistically equivalent to the usual ones, Studia Logica, 101(1), 45–63, doi:10.1007/s11225-011-9367-6.

Haut de page

Pour citer cet article

Référence électronique

Jaime Gaspar, « Copies of Classical Logic in Intuitionistic Logic », Philosophia Scientiæ [En ligne], 18-3 | 2014, mis en ligne le 21 novembre 2014, consulté le 20 juin 2018. URL : http://journals.openedition.org/philosophiascientiae/963 ; DOI : 10.4000/philosophiascientiae.963

Haut de page

Auteur

Jaime Gaspar

INRIA Paris-Rocquencourt, πr2 , Univ Paris Diderot, Sorbonne Paris Cité (France Philosophy).

Haut de page

Droits d’auteur

Tous droits réservés

Haut de page