A Lei de Peirce no cálculo proposicional diz que onde é 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 editar

Uma das estratégias de demonstração fundamentais da lógica clássica é o raciocínio por absurdo. Para mostrar uma proposição  , supõe-se que   é falso. Se chegarmos a uma contradição, então pode-se deduzir a validade de  .

Para mostrar que a implicação   é válida supõe-se, por absurdo, que ela é falsa, isto é,  . Portanto,   é verdadeira e   é falsa, donde,   é falsa, e portanto   é verdadeira, o que resulta em um absurdo.

Conclui-se que  .

Lógica intuicionista e a lei de Peirce editar

A lógica intuicionista trata a negação da seguinte maneira :

  • Se existe ao mesmo tempo uma proposição   e a sua negação  , então tem-se uma contradição, denotada por   (regra da eliminação da negação).
  • Se uma proposição   é conduzida a uma contradição, então temos que   é válida (regra da introdução da negação). Neste sentido,   é apenas outra forma de denotar  .
  • 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 :  
  • Terceiro excluído :  
  • Contraposição :  

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   por uma proposição falsa, obtendo-se  .

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

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

Demonstração do terceiro excluído editar

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

Demonstração da contraposição editar

É também uma consequência da eliminação da dupla negação. Por absurdo, tem-se:

  1.  
  2.  
  3.  
  4.  
  5.  
  6.  
  7.  
  8.  
  9.  
  10.  

Portanto, conclui-se que  .

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

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.

    • PZ 1. hipótese
      • (PQ)→Z 2. hipótese
        • ZQ 3. hipótese
          • P 4. hipótese
          • Z 5. modus ponens 4,1
          • Q 6. modus ponens 5,3
        • PQ 7. dedução de 4 a 6
        • Z 8. modus ponens 7,2
      • (ZQ)→Z 9. dedução de 3 a 8
      • ((ZQ)→Z)→Z 10. Lei de Peirce
      • Z 11. modus ponens 9,10
    • ((PQ)→Z)→Z 12. dedução de 2 a 11
  • (PZ)→((PQ)→Z)→Z) 13. dedução de 1 a 12

Referências editar

  • Peirce, C.S., "On the Algebra of Logic: A Contribution to the Philosophy of Notation", American Journal of Mathematics 7, 180–202 (1885). Reprinted, CP 3.359–403 and CE 5, 162–190.
  • Peirce, C.S., Collected Papers of Charles Sanders Peirce, Vols. 1–6, Charles Hartshorne and Paul Weiss (eds.), Vols. 7–8, Arthur W. Burks (ed.), Harvard University Press, Cambridge, MA, 1931–1935, 1958.

Ver também editar

Ligações externas editar