Paradoxo de Curry - Curry's paradox

O paradoxo de Curry é um paradoxo no qual uma afirmação arbitrária F é provada pela mera existência de uma sentença C que diz de si mesma "Se C , então F ", exigindo apenas algumas regras de dedução lógicas aparentemente inócuas. Visto que F é arbitrário, qualquer lógica com essas regras permite provar tudo. O paradoxo pode ser expresso em linguagem natural e em várias lógicas , incluindo certas formas de teoria dos conjuntos , cálculo lambda e lógica combinatória .

O paradoxo tem o nome do lógico Haskell Curry . Ele também tem sido chamado paradoxo de Löb após Martin Hugo Löb , devido à sua relação com o teorema de Löb .

Em linguagem natural

Reivindicações da forma "se A, então B" são chamadas de reivindicações condicionais . O paradoxo de Curry usa um tipo particular de sentença condicional autorreferencial, conforme demonstrado neste exemplo:

Mesmo que a Alemanha não faça fronteira com a China , a frase de exemplo certamente é uma frase em linguagem natural e, portanto, a verdade dessa frase pode ser analisada. O paradoxo decorre dessa análise. A análise consiste em duas etapas.

1. Primeiro, técnicas comuns de prova em linguagem natural podem ser usadas para provar que a frase de exemplo é verdadeira.
2. Em segundo lugar, a verdade da frase de exemplo pode ser usada para provar que a Alemanha faz fronteira com a China. Como a Alemanha não faz fronteira com a China, isso sugere que houve um erro em uma das provas.

A afirmação "Alemanha faz fronteira com a China" poderia ser substituída por qualquer outra afirmação, e a sentença ainda seria demonstrável. Assim, todas as sentenças parecem ser prováveis. Como a prova usa apenas métodos de dedução bem aceitos e porque nenhum desses métodos parece estar incorreto, essa situação é paradoxal.

Prova informal

O método padrão para provar sentenças condicionais (sentenças da forma "se A, então B") é chamado de " prova condicional ". Neste método, a fim de provar "se A, então B", primeiro A é assumido e então com essa premissa B mostra-se verdadeiro.

Para produzir o paradoxo de Curry, conforme descrito nas duas etapas acima, aplique este método à frase "se esta frase for verdadeira, então a Alemanha faz fronteira com a China". Aqui, A, "esta frase é verdadeira", refere-se à frase geral, enquanto B é "A Alemanha faz fronteira com a China". Portanto, assumir A é o mesmo que assumir "Se A, então B". Portanto, ao assumir A, assumimos A e "Se A, então B". Portanto, B é verdadeiro, por modus ponens , e nós provamos "Se esta frase for verdadeira, então 'Alemanha faz fronteira com a China' é verdade." da maneira usual, assumindo a hipótese e derivando a conclusão.

Agora, porque provamos "Se esta frase for verdadeira, então 'Alemanha faz fronteira com a China' é verdadeira", então podemos aplicar novamente o modus ponens, porque sabemos que a afirmação "esta frase é verdadeira" está correta. Dessa forma, podemos deduzir que a Alemanha faz fronteira com a China.

Prova formal

Lógica sentencial

O exemplo da seção anterior usou raciocínio de linguagem natural não formalizado. O paradoxo de Curry também ocorre em algumas variedades de lógica formal . Nesse contexto, mostra que se assumirmos que existe uma sentença formal (X → Y), onde o próprio X é equivalente a (X → Y), então podemos provar Y com uma prova formal. Um exemplo de tal prova formal é o seguinte. Para obter uma explicação da notação lógica usada nesta seção, consulte a lista de símbolos lógicos .

1. X: = (X → Y)
   
   suposição , o ponto de partida, equivalente a "Se esta frase for verdadeira, então Y"
2. X → X
   
   lei de identidade
3. X → (X → Y)
   
   substitua o lado direito de 2 , uma vez que X é equivalente a X → Y por 1
4. X → Y
   
   de 3 por contração
5. X
   
   substituto 4 , por 1
6. Y
   
   de 5 e 4 por modus ponens

Uma prova alternativa é a lei de Peirce . Se X = X → Y então (X → Y) → X. Isso junto com a lei de Peirce ((X → Y) → X) → X e modus ponens implicam em X e subsequentemente Y (como na prova acima).

Portanto, se Y é uma afirmação improvável em um sistema formal, não há nenhuma afirmação X nesse sistema de forma que X seja equivalente à implicação (X → Y). Em contraste, a seção anterior mostra que na linguagem natural (não formalizada), para cada declaração de linguagem natural Y há uma declaração de linguagem natural Z tal que Z é equivalente a (Z → Y) em linguagem natural. A saber, Z é "Se esta frase for verdadeira, então Y".

Em casos específicos em que a classificação de Y já é conhecida, alguns passos são necessários para revelar a contradição. Por exemplo, quando Y é "A Alemanha faz fronteira com a China", sabe-se que Y é falso.

1. X = (X → Y)
   
   suposição
2. X = (X → falso)
   
   substituir valor conhecido de Y
3. X = (¬X ∨ falso)
   
   implicação
4. X = ¬X
   
   identidade

Teoria dos conjuntos ingênua

Mesmo que a lógica matemática subjacente não admita nenhuma frase autorreferencial, certas formas ingênuas da teoria dos conjuntos ainda são vulneráveis ​​ao paradoxo de Curry. Em teorias de conjunto que permitem compreensão irrestrita , podemos, no entanto, provar qualquer afirmação lógica Y examinando o conjunto

Supondo que tenha precedência sobre ambos e , a prova procede da seguinte forma: ${\ displaystyle \ in}$ ${\ displaystyle \ to}$${\ displaystyle \ leftrightarrow}$

1. ${\ displaystyle X = \ left \ {x \ mid x \ in x \ to Y \ right \}}$
   
   Definição de X
2. ${\ displaystyle x = X \ to (x \ in x \ leftrightarrow X \ in X)}$
   
   Substituição de grupos iguais na associação
3. ${\ displaystyle x = X \ to ((x \ in x \ to Y) \ leftrightarrow (X \ in X \ to Y))}$
   
   A adição de um consequente a ambos os lados de um bicondicional (de 2)
4. ${\ displaystyle X \ in X \ leftrightarrow (X \ in X \ to Y)}$
   
   Lei da concreção (de 1 e 3)
5. ${\ displaystyle X \ in X \ to (X \ in X \ to Y)}$
   
   Eliminação bicondicional (de 4)
6. ${\ displaystyle X \ in X \ to Y}$
   
   Contração (de 5)
7. ${\ displaystyle (X \ em X \ a Y) \ a X \ em X}$
   
   Eliminação bicondicional (de 4)
8. ${\ displaystyle X \ in X}$
   
   Modus ponens (de 6 e 7)
9. ${\ displaystyle Y}$
   
   Modus ponens (de 8 e 6)

A etapa 4 é a única etapa inválida em uma teoria de conjuntos consistente. Na teoria dos conjuntos de Zermelo-Fraenkel , uma hipótese extra afirmando que X é um conjunto seria necessária, o que não é demonstrável em ZF ou em sua extensão ZFC (com o axioma de escolha ).

Portanto, em uma teoria de conjuntos consistente, o conjunto não existe para Y falso . Isso pode ser visto como uma variante do paradoxo de Russell , mas não é idêntico. Algumas propostas para a teoria dos conjuntos tentaram lidar com o paradoxo de Russell não restringindo a regra da compreensão, mas restringindo as regras da lógica de modo que tolere a natureza contraditória do conjunto de todos os conjuntos que não são membros de si mesmos. A existência de provas como a anterior mostra que tal tarefa não é tão simples, pois pelo menos uma das regras de dedução utilizadas na prova acima deve ser omitida ou restringida. ${\ displaystyle \ left \ {x \ mid x \ in x \ to Y \ right \}}$

Cálculo lambda

O paradoxo de Curry pode ser expresso em cálculo lambda não tipado , enriquecido por lógica mínima restrita . Para lidar com as restrições sintáticas do cálculo lambda, deve denotar a função de implicação tomando dois parâmetros, ou seja, o termo lambda deve ser equivalente à notação infixa usual . ${\ displaystyle m}$${\ displaystyle ((mA) B)}$ ${\ displaystyle A \ a B}$

Uma fórmula arbitrária pode ser provada definindo uma função lambda , e , onde denota o combinador de ponto fixo de Curry . Então, por definição de e , portanto, a prova lógica sentencial acima pode ser duplicada no cálculo: ${\ displaystyle Z}$${\ displaystyle N: = \ lambda p. ((mp) Z)}$${\ displaystyle X: = ({\ textf {Y}} N)}$${\ displaystyle {\ textf {Y}}}$${\ displaystyle X = (NX) = ((mX) Z)}$${\ displaystyle {\ textf {Y}}}$${\ displaystyle N}$

No cálculo lambda simplesmente digitado , os combinadores de ponto fixo não podem ser digitados e, portanto, não são permitidos.

Lógica combinatória

O paradoxo de Curry também pode ser expresso na lógica combinatória , que tem poder expressivo equivalente ao cálculo lambda . Qualquer expressão lambda pode ser traduzida em lógica combinatória, portanto, uma tradução da implementação do paradoxo de Curry no cálculo lambda seria suficiente.

O termo acima se traduz em lógica combinatória, onde ${\ displaystyle X}$${\ displaystyle (r \ r)}$

por isso

Discussão

O paradoxo de Curry pode ser formulado em qualquer linguagem que suporte operações lógicas básicas que também permite que uma função autorrecursiva seja construída como uma expressão. Dois mecanismos que sustentam a construção do paradoxo são a auto-referência (a capacidade de se referir a "esta frase" de dentro de uma frase) e a compreensão irrestrita na teoria ingênua dos conjuntos. As linguagens naturais quase sempre contêm muitos recursos que podem ser usados ​​para construir o paradoxo, assim como muitas outras linguagens. Normalmente, a adição de recursos de metaprogramação a uma linguagem adicionará os recursos necessários. A lógica matemática geralmente não permite referência explícita às suas próprias sentenças. No entanto, o cerne dos teoremas da incompletude de Gödel é a observação de que uma forma diferente de autorreferência pode ser adicionada; veja o número de Gödel .

O axioma da compreensão irrestrita adiciona a capacidade de construir uma definição recursiva na teoria dos conjuntos. Este axioma não é apoiado pela moderna teoria dos conjuntos .

As regras lógicas usadas na construção da prova são a regra de suposição para a prova condicional, a regra da contração e o modus ponens . Eles estão incluídos nos sistemas lógicos mais comuns, como a lógica de primeira ordem.

Consequências para alguma lógica formal

Na década de 1930, o paradoxo de Curry e o paradoxo de Kleene-Rosser relacionado desempenharam um papel importante em mostrar que os sistemas lógicos formais baseados em expressões auto-recursivas são inconsistentes . Isso inclui algumas versões do cálculo lambda e da lógica combinatória .

Curry começou com o paradoxo de Kleene-Rosser e deduziu que o problema central poderia ser expresso neste paradoxo de Curry mais simples. Sua conclusão pode ser declarada dizendo que a lógica combinatória e o cálculo lambda não podem ser tornados consistentes como linguagens dedutivas, embora ainda permitindo a recursão.

No estudo da lógica combinatória ilativa (dedutiva) , Curry em 1941 reconheceu a implicação do paradoxo como implicando que, sem restrições, as seguintes propriedades de uma lógica combinatória são incompatíveis:

1. Completude combinatória . Isso significa que um operador de abstração é definível (ou primitivo) no sistema, o que é um requisito do poder expressivo do sistema.
2. Completude dedutiva . Este é um requisito de derivabilidade, a saber, o princípio de que em um sistema formal com implicação material e modus ponens, se Y é demonstrável a partir da hipótese X, então também há uma prova de X → Y.

Resolução

Observe que, ao contrário do paradoxo do mentiroso ou do paradoxo de Russell, o paradoxo de Curry não depende de qual modelo de negação é usado, pois é completamente livre de negação. Assim, as lógicas paraconsistentes ainda podem ser vulneráveis ​​a esse paradoxo, mesmo que sejam imunes ao paradoxo do mentiroso.

Sem resolução no cálculo lambda

A origem da Igreja Alonzo 's cálculo lambda pode ter sido, 'Como você pode resolver uma equação, para fornecer uma definição de uma função?'. Isso é expresso nesta equivalência,

Esta definição é válida se houver uma e apenas uma função que satisfaça a equação , mas inválida caso contrário. Este é o cerne do problema que Stephen Cole Kleene e, em seguida, Haskell Curry descobriram com a lógica combinatória e o cálculo Lambda. ${\ displaystyle f}$${\ displaystyle f \ x = y}$

A situação pode ser comparada a definir

Essa definição é adequada, desde que apenas valores positivos sejam permitidos para a raiz quadrada. Em matemática, uma variável quantificada existencialmente pode representar vários valores, mas apenas um de cada vez. A quantificação existencial é a disjunção de muitas instâncias de uma equação. Em cada equação há um valor para a variável.

No entanto, em matemática, uma expressão sem variáveis ​​livres deve ter um e apenas um valor. Portanto, só pode representar . No entanto, não há maneira conveniente de restringir a abstração lambda a um valor ou de garantir que haja um valor. ${\ displaystyle {\ sqrt {4}}}$${\ displaystyle +2}$

O cálculo lambda permite a recursão ao passar a mesma função que é chamada como parâmetro. Isso permite situações em que tem várias ou nenhuma solução para . ${\ displaystyle f \ x = y}$${\ displaystyle f}$

O cálculo lambda pode ser considerado parte da matemática se apenas as abstrações lambda que representam uma única solução para uma equação forem permitidas. Outras abstrações lambda são incorretas em matemática.

O paradoxo de Curry e outros paradoxos surgem no cálculo Lambda por causa da inconsistência do cálculo Lambda considerado como um sistema dedutivo . Veja também cálculo dedutivo lambda .

Domínio dos termos do cálculo lambda

O cálculo lambda é uma teoria consistente em seu próprio domínio . No entanto, não é consistente adicionar a definição de abstração lambda à matemática geral . Os termos lambda descrevem valores do domínio de cálculo lambda. Cada termo lambda possui um valor nesse domínio.

Ao traduzir expressões da matemática para o cálculo lambda, o domínio dos termos do cálculo lambda nem sempre é isomórfico ao domínio das expressões matemáticas. Essa falta de isomorfismo é a fonte das aparentes contradições.

Resolução em idiomas irrestritos

Existem muitas construções de linguagem que implicitamente invocam uma equação que pode ter nenhuma ou muitas soluções. A resolução de som para esse problema é vincular sintaticamente essas expressões a uma variável quantificada existencialmente. A variável representa os valores múltiplos de uma forma significativa no raciocínio humano comum, mas também válida na matemática.

Por exemplo, uma linguagem natural que permite a função Eval não é matematicamente consistente. Mas cada chamada para Eval nessa linguagem natural pode ser traduzida para a matemática de uma forma consistente. A tradução de Eval (s) para a matemática é

Então, onde s = "Eval (s) → y",

Se y for falso, então x = x → y é falso, mas isso é uma falsidade, não um paradoxo.

A existência da variável x estava implícita na linguagem natural. A variável x é criada quando a linguagem natural é traduzida para a matemática. Isso nos permite usar uma linguagem natural, com semântica natural, mantendo a integridade matemática.

Resolução na lógica formal

O argumento na lógica formal começa assumindo a validade da nomeação (X → Y) como X. No entanto, este não é um ponto de partida válido. Primeiro, devemos deduzir a validade da nomenclatura. O seguinte teorema é facilmente comprovado e representa tal nomenclatura:

Na declaração acima, a fórmula A é nomeada como X. Agora tente instanciar a fórmula com (X → Y) para A. No entanto, isso não é possível, pois o escopo de está dentro do escopo de . A ordem dos quantificadores pode ser invertida usando Skolemization : ${\ displaystyle \ existe X}$${\ displaystyle \ forall A}$

No entanto, agora a instanciação dá

que não é o ponto de partida para a prova e não conduz a uma contradição. Não há outras instanciações para A que conduzam ao ponto de partida do paradoxo.

Resolução na teoria dos conjuntos

Na teoria dos conjuntos de Zermelo – Fraenkel (ZFC), o axioma da compreensão irrestrita é substituído por um grupo de axiomas que permitem a construção de conjuntos. Portanto, o paradoxo de Curry não pode ser declarado no ZFC. ZFC evoluiu em resposta ao paradoxo de Russell.

Veja também

• Paradoxo de Russell
• Paradoxo de Girard
• Paradoxo de Kleene-Rosser
• Paradoxo do mentiroso
• Lista de paradoxos
• Paradoxo de richard
• Teoria dos conjuntos de Zermelo-Fraenkel
• Combinador de ponto fixo
• Cálculo dedutivo lambda
• Deixe expressão

Referências

links externos

• Beall, JC "Paradoxo de Curry" . Em Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .
• Cantini, Andrea. "Paradoxos e Lógica Contemporânea" . Em Zalta, Edward N. (ed.). Stanford Encyclopedia of Philosophy .
• Os pinguins governam o universo: uma prova de que os pinguins governam o universo , uma discussão breve e divertida do paradoxo de Curry.