# Paradoxo de Curry

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:
* $(X\in X)\iff ((X\in X)\to Y)$
    Definição de X
* $(X\in X)\to ((X\in X)\to Y)$
    de 1
* $(X\in X)\to Y$
    de 2, contradição
* $((X\in X)\to Y)\to (X\in X)$
    de 1
* $X\in X$
    de 3 e 4, modus ponens
* $Y$
    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,
    $f=\lambda x.x\to y$ = 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. Sua conclusão pode ser declarado como tendo dito que a lógica combinatória e Lambda cálculo não poderia ser coerente como língua dedutivo, permitindo que a recursividade.
No estudo de ilativo (dedutivo) lógica combinatória, 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:
* Completude combinatória. Isto significa que um operador de abstracção é definível (ou primitiva) no sistema, o que é um requisito sobre o poder expressivo do sistema.
* Completude dedutivo. Este é um requisito em derivabilidade, ou seja, o princípio de que em um sistema formal com implicação e modus ponens materiais, se Y é dedutível a partir da hipótese X, em seguida, há também uma prova de X → Y.

## Resolução

Nota-se que ao contrário do paradoxo do mentiroso ou o paradoxo de Russell, esse paradoxo não depende de qual é o modelo de negação é usada, uma vez que é completamente livre de negação. Assim lógicas paraconsistentes ainda pode estar vulnerável a este, mesmo que eles são imunes ao paradoxo do mentiroso.

### Resolução em linguagem natural

Consideração da frase "Se A então B", onde A se refere à frase cria uma falsidade se B é falso, porque na verdade não há nenhum valor para um que satisfaça a expressão A = "se A então false". Por isso, o resto do argumento é inválido porque ele está argumentando a partir de uma expressão que não tem nenhum valor possível (não existe).

### Sem resolução no lambda cálculo

A origem do cálculo lambda de Alonzo Church pode ter sido, "Como você pode resolver uma equação, para fornecer uma definição de uma função?". Isto é expresso neste equivalência,
Esta definição é válida se houver uma e apenas uma função f que satisfaz a equação f x = y, mas inválido em contrário. Este é o cerne do problema que Stephen Cole Kleene e, em seguida, Haskell Curry descobriu com lógica combinatória e Lambda calculus.
A situação pode ser comparada com a definição,
Esta definição é muito bem contanto que apenas valores positivos são permitidos para a raiz quadrada. Em matemática uma variável quantificada existencialmente podem representar vários valores, mas apenas um de cada vez. Quantificação existencial é a disjunção dos muitos exemplos de uma equação. Em cada equação não é um valor para a variável.
No entanto, em matemática, uma expressão sem variáveis livres deve ter um e somente um valor. assim ${\sqrt {4}}$ crepresentam apenas uma $+2$. No entanto Não Há nenhuma Maneira conveniente parágrafo restringir a abstracção de hum valor de lambda, or parágrafo assegurar that há hum valor.
Lambda cálculo permite recursão fazendo passar a mesma função que chamado, como um parâmetro. Isto permite situações onde$f\ x=y$ tem múltiplas, ou não há soluções para $f$.
Lambda calculus podem ser considerados como parte da matemática se apenas lambda abstrações que representam uma única solução para uma equação são permitidos. Outras abstrações lambda estão incorretas em matemática.
Paradoxo de Curry, e outros paradoxos surgem em Lambda Calculus devido à inconsistência de Lambda cálculo considerada como um sistema dedutivo. Veja também lambda cálculo dedutivo.

#### Domínio dos termos de lambda cálculo

Lambda calculo é uma teoria consistente em seu próprio domínio. No entanto, não é consistente para adicionar a definição lambda abstração para a matemática em geral. Termos Lambda descrever valores do domínio cálculo lambda. Cada termo lambda tem um valor nesse domínio.
Ao traduzir expressões de matemática para cálculo lambda o domínio de termos de cálculo nem sempre é isomorfo ao domínio das expressões matemáticas. Esta falta de isomorfismo é a fonte de a aparente contradição.

### Resolução em linguagens sem restrições

Há muitas construções de linguagem que implicitamente invocar uma equação que pode ter nenhum ou muitas soluções. A resolução de som para este problema é vincular sintaticamente estas expressões a uma variável existencialmente quantificado. A variável representa os vários valores em uma maneira que seja significativa no raciocínio humano comum, mas também é válido em matemática.
Por exemplo, uma linguagem natural que permite que a função de Eval não é matematicamente consistente. Mas cada chamada para Eval em que a linguagem natural pode ser traduzido em matemática em uma maneira que seja consistente. A tradução de Eval (s) em matemática é,
    permitir x = Eval(s) em x
então onde s = "Eval(s) → y"
    permirtir x = x → y in x
Se y é falso, então o x = x → y é falso, mas isso é uma falsidade, não é um paradoxo.
A existência da variável x estava implícito na linguagem natural. A variável x é criado quando a linguagem natural é traduzido em matemática. Isso nos permite usar a linguagem natural, com a semântica naturais, mantendo a integridade matemática.

### Resolução na lógica formal

O argumento na lógica formal começa com assumindo a validade da nomeação (X → Y) como X. No entanto, este não é um ponto de partida válido. Primeiro temos de deduzir a validade da nomeação. O seguinte teorema é facilmente comprovado e representa uma tal nomeação.
Na declaração acima da fórmula A é denominado como X. Agora tentar instanciar com a fórmula (X → Y) A. No entanto, isto não é possível, pois existe o âmbito de \ X está dentro do âmbito da \ forall Uma. A fim de os quantificadores podem ser invertida utilizando Skolemização.
No entanto, agora dá instanciação,
que não é o ponto de partida para a prova e não conduz a uma contradição. Não existem outras instâncias para A que levam ao ponto de o paradoxo de partida.

### Resolução na teoria dos conjuntos

Em Zermelo-Fraenkel o axioma da compreensão irrestrita é substituído com um grupo de axiomas que permitem a construção de conjuntos. Assim, o paradoxo de Curry não se pode afirmar em ZFC. ZFC evoluiu em resposta ao paradoxo de Russell.