# Lei de Peirce

A Lei de Peirce no cálculo proposicional diz que $((A\to B)\to A)\to A$ onde $\to$ é o símbolo de implicação. Em outras palavras, essa lei diz que A deve ser verdade se você pode demonstrar que A implicando em B obriga A a ser verdade. Foi proposta pelo filósofo e lógico Charles Sanders Peirce.
Esta fórmula é válida na lógica clássica e não é válida na lógica intuicionista ou lógicas intermediárias. Pode-se mostrar que, na lógica intuicionista, há uma certa equivalência entre a Lei de Peirce, a regra da eliminação da dupla negação, a lei do terceiro excluído e a contraposição. A adição de qualquer um destes princípios à lógica intuicionista nos dá toda a lógica clássica.
A lei de Peirce não pode ser deduzida partindo somente do teorema da dedução.
Sob o isomorfismo de Curry-Howard a lei de Peirce é um tipo de operador de continuação.

## Demonstração da Lei de Peirce na lógica clássica

Uma das estratégias de demonstração fundamentais da lógica clássica é o raciocínio por absurdo. Para mostrar uma proposição $A$, supõe-se que $A$ é falso. Se chegarmos a uma contradição, então pode-se deduzir a validade de $A$.
Para mostrar que a implicação $((A\to B)\to A)\to A$ é válida supõe-se, por absurdo, que ela é falsa, isto é, $\neg (((A\to B)\to A)\to A)$. Portanto, $((A\to B)\to A)$ é verdadeira e $A$ é falsa, donde, $A\to B$ é falsa, e portanto $A$ é verdadeira, o que resulta em um absurdo.
Conclui-se que $((A\to B)\to A)\to A$.

## Lógica intuicionista e a lei de Peirce

A lógica intuicionista trata a negação da seguinte maneira :
* Se existe ao mesmo tempo uma proposição $A$ e a sua negação $\lnot A$, então tem-se uma contradição, denotada por $\bot$ (regra da eliminação da negação).
* Se uma proposição $A$ é conduzida a uma contradição, então temos que $\lnot A$ é válida (regra da introdução da negação). Neste sentido, $\lnot A$ é apenas outra forma de denotar $A\to \bot$.
* Se um raciocínio chega a uma contradição, então pode-se deduzir a validade de qualquer proposição (regra do absurdo intuicionista). Esta regra é substituída, na lógica clássica, pelo raciocínio por absurdo.
Considere então as seguintes fórmulas :
* Eliminação da dupla negação : $\lnot \lnot A\to A$
* Terceiro excluído : $A\lor \lnot A$
* Contraposição : $(\lnot A\to \lnot B)\to (B\to A)$
Se partimos da lógica intuicionista e acrescentamos a esta lógica a lei de Peirce, pode-se mostrar que as três fórmulas acima são válidas e que obtém-se a lógica clássica. Antes de mais nada, considere a lei de Peirce substituindo $B$ por uma proposição falsa, obtendo-se $(\lnot A\to A)\to A$.

### Demonstração da eliminação da dupla negação

Assuma como hipótese a fórmula $\neg \neg A$. Supondo-se $\neg A$ chega-se a uma contradição (uma proposição e sua negação). Dessa forma, pode-se deduzir $A$ pela regra do absurdo intuicionista. Por conseguinte, mostrou-se a implicação $\neg A\rightarrow A$. Usando a lei de Peirce (neste formato: $(\lnot A\to A)\to A$) conclui-se que $\neg \neg A\rightarrow A$.

### Demonstração do terceiro excluído

É uma consequência direta da eliminação da dupla negação e do raciocínio por absurdo. Para provar $A\lor \lnot A$, admite-se por absurdo $\neg (A\lor \lnot A)$, que é equivalente a $\neg A\land \neg \neg A$. A partir da eliminação da dupla negação, há uma contradição. Portanto, $A\lor \lnot A$.

### Demonstração da contraposição

É também uma consequência da eliminação da dupla negação. Por absurdo, tem-se:
* $\neg ((\neg A\rightarrow \neg B)\rightarrow (B\rightarrow A))$
* $\neg ((\neg \neg A\lor \neg B)\rightarrow (\neg B\lor A))$
* $\neg ((A\lor \neg B)\rightarrow (\neg B\lor A))$
* $\neg (\neg (A\lor \neg B)\lor (\neg B\lor A))$
* $\neg \neg (A\lor \neg B)\land \neg (\neg B\lor A)$
* $(A\lor \neg B)\land (\neg \neg B\land \neg A)$
* $(A\lor \neg B)\land B\land \neg A$
* $(A\land B\land \neg A)\lor (\neg B\land B\land \neg A)$
* $\perp \lor \perp$
* $\perp$
Portanto, conclui-se que $(\lnot A\to \lnot B)\to (B\to A)$.

## Usando a lei de Peirce com o teorema da dedução

A lei de Peirce permite usar uma técnica que usa o teorema da dedução para provar outros teoremas. Suponha que é dado um conjunto de premissas Γ e que queremos deduzir a proposição Z a partir delas. Com a lei de Peirce, pode-se adicionar (sem nenhum custo) premissas adicionais da forma Z→P a Γ.
Por exemplo, suponha que sejam dados P→Z e (P→Q)→Z e queremos deduzir Z, de modo que nós possamos usar o teorema da dedução para concluir que (P→Z)→(((P→Q)→Z)→Z) é um teorema. Então, podemos adicionar um outra premissa Z→Q. Dessa premissa e de P→Z, teremos P→Q. Usando modus ponens com (P→Q)→Z obtêm-se Z. Aplicando o teorema da dedução obtêm-se (Z→Q)→Z, a partir das premissas originais. Então, usando a lei de Peirce na forma ((Z→Q)→Z)→Z e modus ponens derivamos Z das premissas originais. Então, podemos provar o teorema inicial.
** P→Z 1. hipótese
*** (P→Q)→Z 2. hipótese
**** Z→Q 3. hipótese
***** P 4. hipótese
***** Z 5. modus ponens 4,1
***** Q 6. modus ponens 5,3
**** P→Q 7. dedução de 4 a 6
**** Z 8. modus ponens 7,2
*** (Z→Q)→Z 9. dedução de 3 a 8
*** ((Z→Q)→Z)→Z 10. Lei de Peirce
*** Z 11. modus ponens 9,10
** ((P→Q)→Z)→Z 12. dedução de 2 a 11
* (P→Z)→((P→Q)→Z)→Z) 13. dedução de 1 a 12