Lei de Peirce - Peirce's law

Na lógica , a lei de Peirce leva o nome do filósofo e lógico Charles Sanders Peirce . Foi tomado como um axioma em sua primeira axiomatização da lógica proposicional . Pode ser pensada como a lei do meio excluído escrita de uma forma que envolve apenas um tipo de conectivo, a saber, implicação.

No cálculo proposicional , a lei de Peirce diz que (( P → Q ) → P ) → P . Escrito, isso significa que P deve ser verdadeiro se houver uma proposição Q tal que a verdade de P decorra da verdade de "se P então Q ". Em particular, quando Q é considerado uma fórmula falsa, a lei diz que se P deve ser verdadeiro sempre que implica falsidade, então P é verdadeiro. Desse modo, a lei de Peirce implica a lei do terceiro excluído .

A lei de Peirce não se aplica à lógica intuicionista ou à lógica intermediária e não pode ser deduzida apenas do teorema da dedução .

Sob o isomorfismo de Curry-Howard , a lei de Peirce é o tipo de operadores de continuação , por exemplo, call / cc no Scheme .

História

Aqui está a declaração de lei do próprio Peirce:

Um quinto ícone é necessário para o princípio do meio excluído e outras proposições relacionadas a ele. Uma das fórmulas mais simples desse tipo é:

Isso dificilmente é axiomático. Que é verdade aparece da seguinte forma. Só pode ser falso porque o consequente final x é falso, enquanto seu antecedente ( x → y ) → x é verdadeiro. Se isso for verdadeiro, ou seu consequente, x , é verdadeiro, quando toda a fórmula seria verdadeira, ou seu antecedente x → y é falso. Mas, no último caso, o antecedente de x → y , ou seja , x , deve ser verdadeiro. (Peirce, The Collected Papers 3.384).

Peirce prossegue apontando uma aplicação imediata da lei:

A partir da fórmula que acabamos de fornecer, obtemos imediatamente:

onde o a é usado em tal sentido que ( x → y ) → a significa que de ( x → y ) toda proposição segue. Com esse entendimento, a fórmula estabelece o princípio do terceiro excluído, que da falsidade da negação de x decorre a verdade de x . (Peirce, The Collected Papers 3.384).

Aviso : (( x → y ) → a ) → x não é uma tautologia . No entanto, [ a → x ] → [(( x → y ) → a ) → x ] é uma tautologia.

Outras provas

Aqui está uma prova simples da lei de Peirce assumindo dupla negação e derivando a disjunção padrão de uma implicação : ${\ displaystyle (\ neg \ neg P \ iff P)}$${\ displaystyle ((P \ rightarrow Q) \ Rightarrow (\ neg P \ vee Q))}$

${\ displaystyle {\ begin {alinhado} (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 {alinhado}}}$

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

A lei de Peirce permite aprimorar a técnica de uso do teorema da dedução para provar teoremas. Suponha que recebamos um conjunto de premissas Γ e desejemos deduzir uma proposição Z a partir delas. Com a lei de Peirce, pode-se adicionar (sem custo) premissas adicionais da forma Z → P a Γ. Por exemplo, suponha que recebamos P → Z e ( P → Q ) → Z e desejamos deduzir Z para que possamos usar o teorema de dedução para concluir que ( P → Z ) → ((( P → Q ) → Z ) → Z ) é um teorema. Então, podemos adicionar outra premissa Z → Q . A partir desse e P → Z , temos P → Q . Em seguida, aplicamos modus ponens com ( P → Q ) → Z como a principal premissa para obter Z . Aplicando o teorema da dedução, obtemos que ( Z → Q ) → Z segue das premissas originais. Então usamos a lei de Peirce na forma (( Z → Q ) → Z ) → Z e modus ponens para derivar Z das premissas originais. Então podemos terminar provando o teorema como pretendíamos originalmente.

Completude do cálculo proposicional implicacional

Uma razão pela qual a lei de Peirce é importante é que ela pode substituir a lei do terceiro excluído na lógica que usa apenas implicação. As sentenças que podem ser deduzidas dos esquemas axioma:

• P → ( Q → P )
• ( P → ( Q → R )) → (( P → Q ) → ( P → R ))
• (( P → Q ) → P ) → P
• de P e P → Q inferir Q

(onde P , Q , R contêm apenas "→" como um conectivo) são todas as tautologias que usam apenas "→" como um conectivo.

Veja também

• Bibliografia de Charles Sanders Peirce

Notas

Leitura adicional

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