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.[1]

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 supor 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)

assumption

2. X = (X → false)

substitute known value of Y

3. X = (¬X ∨ false)

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:

  1. Definição de X
  2. de 1
  3. de 2, contradição
  4. de 1
  5. de 3 e 4, modus ponens
  6. 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. [necessário esclarecer]

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