La loi de Peirce - Peirce's law

En logique , la loi de Peirce porte le nom du philosophe et logicien Charles Sanders Peirce . Il a été pris comme un axiome dans sa première axiomatisation de la logique propositionnelle . Elle peut être considérée comme la loi du tiers exclu écrite sous une forme qui n'implique qu'une sorte de connecteur, à savoir l'implication.

En calcul propositionnel , la loi de Peirce dit que (( P → Q )→ P )→ P . Écrit, cela signifie que P doit être vrai s'il existe une proposition Q telle que la vérité de P découle de la vérité de "si P alors Q ". En particulier, lorsque Q est considéré comme une formule fausse, la loi dit que si P doit être vrai chaque fois qu'il implique la fausseté, alors P est vrai. De cette façon, la loi de Peirce implique la loi du tiers exclu .

La loi de Peirce ne tient pas dans la logique intuitionniste ou les logiques intermédiaires et ne peut être déduite du théorème de déduction seul.

Sous l' isomorphisme de Curry-Howard , la loi de Peirce est le type d' opérateurs de continuation , par exemple call/cc dans Scheme .

Histoire

Voici la propre déclaration de Peirce sur la loi :

Une cinquième icône est requise pour le principe du tiers exclu et les autres propositions qui s'y rattachent. Une des formules les plus simples de ce genre est :

Ce n'est guère axiomatique. Que cela soit vrai apparaît comme suit. Il ne peut être faux que si le conséquent final x est faux alors que son antécédent ( x → y ) → x est vrai. Si cela est vrai, soit son conséquent, x , est vrai, alors que toute la formule serait vraie, soit son antécédent x → y est faux. Mais dans le dernier cas l'antécédent de x → y , c'est-à-dire x , doit être vrai. (Peirce, les papiers collectés 3.384).

Peirce poursuit en soulignant une application immédiate de la loi :

De la formule qui vient d'être donnée, on obtient aussitôt :

où le a est utilisé dans un sens tel que ( x → y ) → a signifie que de ( x → y ) toute proposition suit. Avec cette compréhension, la formule énonce le principe du tiers exclu, que de la fausseté de la négation de x découle la vérité de x . (Peirce, les papiers collectés 3.384).

Attention : (( x → y )→ a )→ x n'est pas une tautologie . Cependant, [ a → x ]→[(( x → y )→ a )→ x ] est une tautologie.

Autres preuves

Voici une preuve simple de la loi de Peirce en supposant une double négation et en dérivant la disjonction standard d'une implication : ${\style d'affichage (\neg \neg P\iff P)}$${\style d'affichage ((P\rightarrow Q)\Rightarrow (\neg P\vee Q))}$

${\displaystyle {\begin{aligned}(p\rightarrow q)\rightarrow p\\\neg (p\rightarrow q)\lor p\\\neg (\neg p\lor q)\lor p\\(p \land \neg q)\lor p\\p\lor p\\p.\\\end{aligned}}}$

Utilisation de la loi de Peirce avec le théorème de déduction

La loi de Peirce permet d'améliorer la technique consistant à utiliser le théorème de déduction pour prouver des théorèmes. Supposons que l' on est donné un ensemble de locaux Γ et on veut en déduire une proposition Z d'eux. Avec la loi de Peirce, on peut ajouter (sans frais) des prémisses supplémentaires de la forme Z → P à Γ. Par exemple, supposons que l'on nous donne P → Z et ( P → Q )→ Z et que nous souhaitions en déduire Z pour pouvoir utiliser le théorème de déduction pour conclure que ( P → Z )→((( P → Q )→ Z )→ Z ) est un théorème. Ensuite, nous pouvons ajouter une autre prémisse Z → Q . De là et P → Z , on obtient P → Q . Ensuite, nous appliquons le modus ponens avec ( P → Q )→ Z comme prémisse majeure pour obtenir Z . En appliquant le théorème de déduction, nous obtenons que ( Z → Q )→ Z découle des prémisses originales. Ensuite, nous utilisons la loi de Peirce sous la forme (( Z → Q )→ Z )→ Z et modus ponens pour dériver Z des prémisses originales. Ensuite, nous pouvons terminer la démonstration du théorème comme nous l'avions initialement prévu.

Complétude du calcul propositionnel implicationnel

L'une des raisons pour lesquelles la loi de Peirce est importante est qu'elle peut se substituer à la loi du tiers exclu dans la logique qui n'utilise que l'implication. Les phrases que l'on peut déduire des schémas axiomes :

• P →( Q → P )
• ( P →( Q → R ))→(( P → Q )→( P → R ))
• (( P → Q )→ P )→ P
• de P et P → Q déduire Q

(où P , Q , R ne contiennent que "→" comme connecteur) sont toutes les tautologies qui n'utilisent que "→" comme connecteur.

Voir également

• Bibliographie de Charles Sanders Peirce

Remarques

Lectures complémentaires

• Peirce, CS, "Sur l'algèbre de la logique: une contribution à la philosophie de la notation", American Journal of Mathematics 7, 180-202 (1885). Réimprimé, les Papiers Collectés de Charles Sanders Peirce 3.359-403 et les Écrits de Charles S. Peirce : Une Édition Chronologique 5, 162-190.
• Peirce, CS, Collected Papers of Charles Sanders Peirce , Vols. 1–6, Charles Hartshorne et Paul Weiss (éd.), Vols. 7-8, Arthur W. Burks (éd.), Harvard University Press, Cambridge, MA, 1931-1935, 1958.