Paradoxo de Curry é um paradoxo que ocorre na teoria dos conjuntos ingênua ou lógicas ingênuas, e permite a derivação de uma sentença arbitrária de uma sentença auto-referente e algumas regras de dedução lógica aparentemente inócuas. É assim denominado em referência ao lógico Haskell Curry. Enquanto a teoria dos conjuntos ingênua falha em identificá-lo, um exame mais rigoroso revela que a sentença é auto-contraditória.
Ele também foi chamado paradoxo de Löb em referência a Martin Hugo Löb.
Declaração do paradoxo de Curry O paradoxo pode ser expresso em linguagem natural e em várias linguagens matemáticas; Linguagem Natural Lógica Formal Teoria dos conjuntos Logic com uma função Eval em cadeia Lambda Cálculo Lógica Combinatória
Linguagem Natural Reivindicações da forma "se A, então B" são chamados alegações condicionais. Paradoxo de Curry usa um tipo específico de sentença condicional auto-referencial, como demonstrado neste exemplo: Se esta frase é verdadeira, então a Alemanha faz fronteira com a China. Muito embora a Alemanha não faça fronteira com a China, a frase do exemplo certamente é uma sentença da linguagem natural, e assim a veracidade da sentença pode ser analisada. O paradoxo segue desta análise. Primeiro, técnicas de prova comum de linguagem natural podem ser usadas para provar que a sentença é verdadeira. Em segundo lugar, a verdade da sentença exemplo pode ser usada para provar que a Alemanha faz fronteira com a China. Porque a Alemanha não faz fronteira com a China, isso sugere que houve um erro em uma das provas.
A afirmação "A Alemanha faz fronteira com a China" poderia ser substituída por qualquer outra afirmação, e a sentença ainda seria demonstrável; assim, cada frase parece ser demonstrável. Porque a prova utiliza apenas métodos de dedução bem aceitos, e porque nenhum desses métodos parecem estar incorretos, esta situação é paradoxal.
Prova de que a sentença é verdadeira A análise a seguir é usada para mostrar que a frase "Se esta frase é verdadeira, então a Alemanha faz fronteira com a China" é ela própria verdadeira. A frase citada é da forma "se A então B", onde uma se refere ao próprio e B sentença refere-se a "Alemanha faz fronteira com a China".
O método usual para provar uma sentença condicional é mostrar que ao assumir que essa hipótese (A) é verdadeira, então a conclusão (B) pode ser comprovada a partir desse pressuposto. Portanto, para o objectivo da prova, assuma A.
Porque A refere-se à frase em geral, isto significa que assumindo que A é o mesmo que assumir que "Se A então B". Portanto, assumindo A, assumiu-se ambos A e "Se A então B". Destes, podemos obter B por modus ponens. Portanto, A implica B e provamos "Se esta frase é verdadeira então a Alemanha faz fronteira com a China" é verdadeiro. Portanto, "Alemanha faz fronteira com a China", mas sabemos que é falso, o que é um paradoxo.
Lógica Formal O exemplo na seção anterior usado não formalizada, o raciocínio de linguagem natural. Paradoxo de Curry também ocorre na lógica formal. Neste contexto, ele mostra que se nós supormos que há uma sentença formal de (X → Y), onde a própria X é equivalente a (X → Y), então podemos provar Y com uma prova formal. Um exemplo de uma prova formal é tal como se segue. Para explicação da notação lógica usada nesta seção, consulte a lista de símbolos lógicos.
0. X := (X → Y) suposição, o ponto de partida, o equivalente a "Se esta frase é verdadeira, então Y" 1. X → X Estado de suposição, também chamado de correção de local ou de hipótese 2. X → (X → Y) substituir lado direito de um, uma vez que X é equivalente a X → Y por 0 3. X → Y a partir de 2 por contracção 4. X trocar 3, by 0 5. Y de 4 e 3 por modus ponens Uma prova alternativa é através de lei de Peirce. Se X = X → Y, em seguida, (X → Y) → X. Isto, juntamente com a lei de Peirce ((X → Y) → X) → X e modus ponens implica X e Y posteriormente (como na prova acima).
Portanto, se Y for uma instrução demonstrável num sistema formal, não existe nenhuma instrução X em que o sistema de tal modo que X é equivalente à implicação (X → Y). Em contrapartida, a secção anterior mostra que, em linguagem natural (não formalizada), para todas as línguas declaração Y natural que existe uma linguagem natural declaração Z tal que Z é equivalente a (Z → Y) em linguagem natural. Ou seja, Z é "Se esta frase é verdadeira, então Y".
Em casos específicos em que a classificação de Y já é conhecido, alguns passos são necessários para revelar a contradição. Por exemplo, quando Y é "Alemanha fronteira China", sabe-se que Y é falsa.
1. X = (X → Y) assunção
2. X = (X → falso) substituição de Y pelo valor conhecido
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 admite qualquer sentença auto-referencial, em conjunto teorias que permitem a compreensão irrestrita, podemos, no entanto, provar qualquer declaração Y lógico, examinando o conjunto
A prova prossegue como se segue:
Definição de X
de 1
de 2, contradição
de 1
de 3 e 4, modus ponens
de 3 e 5, modus ponens Portanto, em uma teoria consistente conjunto, o conjunto {x| (x e x) -> Y} não existe para false Y. Isso pode ser visto como uma variante no paradoxo de Russell, mas é não idênticos. Algumas propostas de teoria dos conjuntos têm tentado lidar com o paradoxo de Russell não restringindo a regra de compreensão, mas restringindo as regras da lógica para que ele tolera 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 o descrito acima mostra que tal tarefa não é tão simples, porque pelo menos uma das regras de dedução utilizados na prova acima devem ser omitidas ou restrito.
Lógica com uma função de cadeia Eval Suponha que há uma função chamada eval, que recebe uma string e converte-lo em uma expressão lógica. Em seguida, considere a seqüência de caracteres, s = "eval(s) → y" então a expressão, eval(s) = eval(s) → y novamente dá o paradoxo de Curry.
Lambda Cálculo Paradoxo de Curry pode ser expresso em cálculo lambda. Considere uma função definida como r. r = ( λx. ((x x) → y) ) Então (r r) β-reduz para (r r) → y Se (rr) é verdadeiro, então o seu reduto (rr) → y também é verdadeiro, e, por modus ponens, por isso é y. Se (rr) é falsa, em seguida, (rr) → y é verdadeiro se pelo princípio da explosão, que é uma contradição. Então y é verdadeiro e como y pode ser qualquer declaração, qualquer afirmação pode ser provada verdadeira.
(R R) é uma computação não-terminante. Considerado como lógica, (rr) é uma expressão para um valor que não existe.
Em cálculo lambda simplesmente tipado, tais termos, como quaisquer combinadores de ponto fixo, não podem ser tirados e, portanto, não são admitidos; isto é suficiente para evitar problemas de consistência em combinação com conectivos lógicos. O λProlog, linguagem de programação, é baseado em tal combinação.
Lógica Combinatória Paradoxo de Curry também pode ser expresso em 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, por isso, uma tradução da aplicação do paradoxo de Curry em cálculo lambda seria suficiente.
Se m é a função implicação tendo dois parâmetros (que é m AB é equivalente a A → B), então r é de lógica combinatória, r = S (S (K m) (S I I)) (K y) Então r r = m (r r) y O paradoxo pode também ser produzido utilizando o combinador paradoxal de Curry, onde, = S m (K y) Então, Y f é a solução de,
então Y f = m (Y f) y
Discussão Terminologia Linguagem natural e lógica matemática são ambos baseados em afirmar algumas declarações para ser verdade. A declaração pode ser representado como um lógico (ou boolean) expressão (ou fórmula), que pode ser avaliado para dar um valor de verdadeiro ou falso. Uma afirmação é uma declaração ou expressão lógica que, afirma-se, quando avaliadas, vai dar o verdadeiro valor.
Demonstrações podem também ser considerados em formas mais complexas. As declarações podem ser qualificados pelo que afirma, ou acreditar neles, e por nível de certeza. No entanto, para a lógica, a simples definição dada acima é suficiente.
Problema de existência Este paradoxo é semelhante a, Paradoxo do mentiroso Paradoxo de Russell em que cada um paradoxo tenta dar um nome para algo que não existe. Esses paradoxos tudo tentativa de dar um nome ou representação a uma solução para a equação, X = ¬X Nota-se que o paradoxo não surge de fazer valer a declaração de ¬X, como tal declaração seria uma mentira. Ela surge a partir da consideração e nomeação da declaração. O paradoxo surge nomeando ou represente uma expressão da forma ¬X ser X. No caso de o Paradoxo de Curry, a negação é construído a partir implicação, X = X → false = ¬X ∨ false = ¬X O domínio de uma variável X boolean é o conjunto {verdadeiro, falso}. No entanto nem verdadeiro ou falso é uma solução para a equação acima. Assim deve ser errado afirmar a existência de X, e é mentira para nomear o ¬X expressão como X.
O paradoxo existe sempre uma expressão pode ser construído cujo valor não existe. Isto pode ser conseguido usando "esta afirmação", mas existem muitas outras características linguísticas, que permitem a construção de expressão que não existe.
Recursos de linguagem para expressar o paradoxo Paradoxo de Curry pode ser formulado em qualquer linguagem de suporte operações lógicos básicos que também permite que uma função de auto-recursiva para ser construído como uma expressão. A lista a seguir dá alguns mecanismos que sustentam a construção do paradoxo, mas a lista não é exaustiva. A auto-referência; "essa sentença". Através de nomenclatura de uma expressão que inclui o nome. Aplicar a teoria dos conjuntos ingênua (compreensão irrestrito). As expressões lambda. Uma função Eval em uma palavra. As regras lógicas utilizadas na construção de prova são, regra da assunção contração modus ponens A função de auto-recursiva pode então ser utilizado para definir um cálculo de terminação não cujo valor é a solução para uma equação. Em Paradoxo de Curry usamos implicação para a construção de uma negação, que constrói uma equação sem solução.
A expressão recursiva representa, em seguida, um valor que não existe. As leis da lógica são válidas somente para os valores booleanos em {verdadeiro, falso}, portanto, qualquer retenção sobre a expressão pode estar em erro.
As linguagens naturais quase sempre contêm muitos dos recursos que poderiam ser utilizados para construir o paradoxo, assim como muitas outras línguas. Normalmente a adição de recursos de programação meta para um idioma irá adicionar os recursos necessários.
Lógica matemática geralmente não tolerar referência explícita às suas próprias sentenças. No entanto, o coração de teoremas da incompletude de Gödel é a observação de que a auto-referência pode ser adicionado; veja o número de Gödel.
O axioma de compreensão Irrestrito adiciona a capacidade de construir uma definição recursiva na teoria dos conjuntos. Este axioma não é suportado pela teoria dos conjuntos moderna.
Consequências para alguma lógica formal Na década de 1930, o Paradoxo de Curry eo paradoxo Kleene-Rosser relacionada desempenhou um papel importante em mostrar que os sistemas formais de lógica com base em expressões de auto-recursiva são inconsistentes. Lambda calculo lógica combinatória Curry começou com o paradoxo Kleene-Rosser e deduziu que o problema central poderia ser expressa neste paradoxo mais simples do Curry.The Inconsistency of Certain Formal Logic Haskell B. Curry The Journal of Symbolic Logic Vol. 7, No. 3 (Sep., 1942), pp. 115-117 Published by: Association for Symbolic Logic