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].

Accès au texte / extrait

Cairn

Texte intégral en libre accès disponible sur le portail Cairn. Le texte intégral en libre accès sera disponible à cette adresse en janvier 2018.
Consulter cet article

Plan

1 Philosophy
1.1 Non-constructive and constructive proofs
1.2 Constructivism
2 Mathematics
2.1 Classical and intuitionistic logics
2.2 Copies
2.3 Question: is the copy unique?
2.4 Answer: no

Aperçu du début du texte

1 Philosophy

1.1 Non-constructive and constructive proofs

Mathematicians 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.

Definition 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.

From 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.

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

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

Theorem 3. There are irra...

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 27 avril 2017. URL : http://philosophiascientiae.revues.org/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