Categorias
Paradoxos

Paradoxo de Kleene – Rosser

Em matemática, o paradoxo de Kleene-Rosser é um paradoxo que mostra que certos sistemas de lógica formal são inconsistentes, em particular a versão da lógica combinatória de Curry, introduzida em 1930, e o cálculo lambda original de Church, introduzido em 1932–1933, ambos originalmente pretendidos como sistemas de lógica formal. O paradoxo foi exibido por Stephen Kleene e JB Rosser em 1935.

O paradoxo
Kleene e Rosser foram capazes de mostrar que ambos os sistemas são capazes de caracterizar e enumerar suas funções teóricas numéricas comprovadamente totais e definíveis, o que lhes permitiu construir um termo que replica essencialmente o paradoxo de Richard na linguagem formal.

Mais tarde, Curry conseguiu identificar os ingredientes cruciais dos cálculos que permitiam a construção desse paradoxo, e usou isso para construir um paradoxo muito mais simples, agora conhecido como paradoxo de Curry.

Em 1935, Kleene e Rosser publicaram uma prova de que certos sistemas de lógica formal são inconsistentes, no sentido de que toda fórmula que pode ser expressa em sua notação também é demonstrável. Acontece que existem apenas dois sistemas na literatura aos quais essa prova de inconsistência se aplica; ou seja, o sistema da Igreja de 1932-1933 e o que eu chamei de sistema 8 em 1934. Mas, apesar dessa aplicação limitada, o argumento de Kleene e Rosser representa um teorema de grande importância para a orientação de pesquisas futuras. É um teorema do mesmo caráter geral que os famosos teoremas da incompletude de Löwenheim, Skolem e Godel, que desempenharam um papel tão proeminente em pesquisas recentes em fundamentos matemáticos.

A prova de Kleene e Rosser é longa e intrincada e contém complicações que tendem a obscurecer o significado essencial de seu teorema. Por conseguinte, existe algum interesse no problema de tornar esse paradoxo mais acessível e de apresentá-lo de forma a destacar esse significado essencial de maneira mais clara. É isso que o presente artigo tenta fazer. O paradoxo é aqui apresentado e derivado por um método que apresenta muitas vantagens, do ponto de vista indicado, sobre o dos descobridores originais.

Antes de iniciarmos uma discussão detalhada, será conveniente examinar o paradoxo de maneira vaga e preliminar e explicar em termos intuitivos a idéia central em sua derivação

Um dos objetivos para os quais os matemáticos se esforçam na criação de sistemas formais é a completude – com a qual não quero dizer completude no sentido técnico, mas simplesmente a adequação do sistema para um propósito ou outro.

Existem dois tipos de completude que interessam especialmente; ambos são propriedades desejáveis ​​de sistemas formais de lógica matemática. Essas completidades combinatórias e dedutivas, respectivamente. Eles podem ser explicados da seguinte maneira. Uma teoria é combinatorialmente completa se, e somente se, toda expressão A formada a partir dos termos do sistema e um auxiliar indeterminado ou variável x, puder ser representada no sistema como uma função de x (isto é, podemos formar no sistema uma função cuja O valor de qualquer argumento é o mesmo que o resultado da substituição desse argumento por x em W). Uma teoria é dedutivamente completa se, sempre que pudermos derivar uma proposição B com a hipótese de outra proposição A, podemos derivar sem hipótese uma terceira proposição (como A ^) B) expressando essa dedutibilidade. A completitude combinatória é, portanto, uma propriedade relacionada às possíveis construções de termos (ou fórmulas) dentro do sistema; completude dedutiva refere-se às possíveis derivações. A integridade dedutiva é uma propriedade bem conhecida de certos sistemas; considerando que a completitude combinatória só foi alcançada nos últimos anos.

A essência do teorema de Kleene-Rosser é que mostra que esses dois tipos de completude são incompatíveis – isto é, que qualquer sistema que possua os dois seja inconsistente. O argumento é essencialmente um refinamento do paradoxo de Richard; mostra, de fato, que o paradoxo de Richard pode ser configurado formalmente dentro do sistema.

Para ver isso de uma maneira preliminar, vamos montar o paradoxo de Richard, como segue. Em qualquer sistema formal de aritmética, o número de funções numéricas definíveis de números naturais é enumerável; que eles, portanto, sejam enumerados, digamos em uma sequência

Deixando de lado a explicação desse paradoxo de um ponto de vista intuitivo, vamos considerar o que acontece no caso de um sistema que é tanto combinatória quanto dedutivamente completo. Nesse sistema, se uma função é uma função numérica – isto é, se fornece valores numéricos para todos os argumentos numéricos (u) -, uma declaração formal desse fato pode ser demonstrada no sistema, uma vez que é dedutivamente completa; por meio de uma enumeração recursiva de todos os teoremas, o conjunto de todas as funções numéricas pode ser efetivamente enumerado em uma sequência. Como a teoria é combinatória, podemos definir no sistema a função /; isso é comprovadamente uma função numérica, e a demonstração desse fato nos dirá efetivamente o valor de n de tal forma que a contradição acima certamente surgirá.

Isso mostra de maneira grosseira a natureza do paradoxo. Antes de prosseguirmos com os desenvolvimentos formais, interpolarei algumas observações sobre a presente prova e sua relação com a de Kleene e Rosser.

Nas investigações de Church e seus alunos, a integridade combinatória postulada é enfraquecida, pois é necessário que o A realmente contenha x – de modo que não seja necessário um aparato para representar uma constante como uma função; há também um enfraquecimento na pontuação da completude dedutiva. Essas complicações não evitam o paradoxo, como Kleene e Rosser mostraram; mas eles aumentam consideravelmente o comprimento e complexidade da derivação. Se o objetivo é expor o nervo central do paradoxo, a abordagem lógica é realizar a prova do caso mais simples, o da completude combinatória (e dedutiva) no sentido forte, e depois mostrar quais modificações são necessárias. realizar a prova para o caso mais complicado.