Paradoxe de Curry

Le paradoxe de Curry fut présenté par le mathématicien Haskell Curry en 1942 et permet d'arriver à n'importe quelle conclusion à partir d'une phrase auto-référentielle et de quelques règles logiques simples. Une telle phrase s'énonce : Si cette phrase est vraie, alors le monstre du Memphrémagog existe. Il est aussi nommé le paradoxe de Löb puisque la preuve se déroule de manière semblable à celle du théorème de Löb publié en 1955 par le mathématicien Martin Löb. On peut déduire l'existence d'un certain monstre légendaire comme suit : on peut se demander de façon spéculative, si la phrase était vraie, alors là, le monstre existerait-il ? Si on acceptait que la phrase soit vraie, on devrait accepter ce qu'elle dit. Or, elle dit que si elle est vraie, le monstre existe. Il semble que la réponse à notre question spéculative doit être oui : si la phrase est vraie, alors le monstre existe. Mais voilà ce qu'affirmait la phrase - non que le monstre existe, mais qu'il existe si la phrase est vraie. Alors il semble qu'il faille avouer que la phrase est vraie. Et bien sûr, puisque la phrase est vraie, il existe. Donc il y a vraiment un monstre au fond du lac Memphrémagog. Puisqu'il est évident que n'importe quelle monstruosité pourrait se prouver de façon pareille, il s'agit d'un paradoxe. Cela peut s'exprimer de façon tout à fait formelle. Désignons par Y l'existence du monstre, et par X la phrase qui affirme Y à condition que X. C'est-à-dire, la définition de X est X → Y. Le symbole « → » est le connecteur d'implication logique. Dans le calcul classique des propositions, le connecteur d'implication n'est qu'une abréviation pour une disjonction et une négation ; par « si A, alors B » on entend « non A ou B ». Notre phrase auto-référentielle devient donc « cette phrase est fausse, ou le monstre du Memphrémagog existe », ce qui est une modification légère du paradoxe du menteur. Or la réponse classique à celui-ci est de nier la possibilité de phrase auto-référentielle. Un énoncé doit se composer de façon acyclique de propositions primitives liées par des connecteurs logiques.

À propos de ce résultat

Cette page est générée automatiquement et peut contenir des informations qui ne sont pas correctes, complètes, à jour ou pertinentes par rapport à votre recherche. Il en va de même pour toutes les autres pages de ce site. Veillez à vérifier les informations auprès des sources officielles de l'EPFL.

Concepts associés (9)

Séances de cours associées (1)

Philosophie de Mathématiques : Ontologie et Structures HUM-417: Philosophical perspectives on the exact sciences I

Explore l'existence d'objets mathématiques, la vérité des propositions, et la connaissance à leur sujet, couvrant le platonisme, l'intuitisme, le structuralisme, le nominalisme, le logique et le formalisme.

Lambda lifting

Lambda lifting is a meta-process that restructures a computer program so that functions are defined independently of each other in a global scope. An individual "lift" transforms a local function into a global function. It is a two step process, consisting of; Eliminating free variables in the function by adding parameters. Moving functions from a restricted scope to broader or global scope. The term "lambda lifting" was first introduced by Thomas Johnsson around 1982 and was historically considered as a mechanism for implementing functional programming languages.

Deductive lambda calculus

Deductive lambda calculus considers what happens when lambda terms are regarded as mathematical expressions. One interpretation of the untyped lambda calculus is as a programming language where evaluation proceeds by performing reductions on an expression until it is in normal form. In this interpretation, if the expression never reduces to normal form then the program never terminates, and the value is undefined. Considered as a mathematical deductive system, each reduction would not alter the value of the expression.

Let expression

In computer science, a "let" expression associates a function definition with a restricted scope. The "let" expression may also be defined in mathematics, where it associates a Boolean condition with a restricted scope. The "let" expression may be considered as a lambda abstraction applied to a value. Within mathematics, a let expression may also be considered as a conjunction of expressions, within an existential quantifier which restricts the scope of the variable.