História da tese de Church-Turing

A história da tese de Church-Turing ("tese") envolve a história do desenvolvimento do estudo da natureza das funções cujos valores são efetivamente calculáveis; ou, em termos mais modernos, funções cujos valores são algoritmicamente computáveis. É um tópico importante na teoria matemática moderna e ciência da computação, particularmente associada com o trabalho de Alonzo Church e Alan Turing.

O debate e a descoberta do significado de "computação" e "recursividade" tem sido longa e controverso. Este artigo fornece detalhes deste debate e a descoberta dos Axiomas de Peano, em 1889, passando pela recente discussão sobre o significado de "axioma".

Axiomas de Peano

Em 1889, Giuseppe Peano apresentou Os princípios da aritmética, apresentados por um novo método, baseado na obra de Dedekind. Soare propõe que a origem da "recursão primitiva" começou com os axiomas de Peano, embora

"Bem antes do século XIX os matemáticos usavam o princípio da definição de uma função por indução. Em 1888 Dedekind provou, usando axiomas aceitos, que tal definição define uma única função, e aplicou-o para a definição das funções m+n, m x n, e mⁿ. Com base neste trabalho de Dedekind, Peano em 1889 e 1891, escreveu o familiar cinco [sic] axiomas para os inteiros positivos. Como um companheiro para o seu quinto [sic] axioma, indução matemática, Peano usou definição por indução, o que tem sido chamado de recursão primitiva (desde Péter em 1934 e Kleene em 1936) ... ."

Observe que, de fato, os Axiomas de Peano são 9 em número e o axioma 9 é o axioma da recursividade/indução.

"Posteriormente, os 9 axiomas foram reduzidos à 5 como "Axiomas 2, 3, 4 e 5, que tratam de identidade, pertencem à lógica subjacente. Isso deixa os cinco axiomas que tornaram-se universalmente conhecidos como "os Axiomas de Peano ... Peano reconhece (1891b, p. 93) que seus axiomas vêm de Dedekind ... ."

Hilbert e o Entscheidungsproblem

No Congresso Internacional de Matemáticos, em 1900, em Paris, o famoso matemático David Hilbert, apresentou um conjunto de problemas – agora conhecido como os Problemas de Hilbert – o seu farol iluminando o caminho para os matemáticos do século XX. Os problemas de Hilbert 2 e 10 introduziram o Entscheidungsproblem (o "problema de decisão"). Em seu 2º problema, ele pediu uma prova de que "aritmética" é "consistente". Kurt Gödel iria provar, em 1931, que, dentro do que ele chamou de "P" (hoje chamados de Aritmética de Peano), "existem sentenças indecidíveis [proposições]". Devido a isso, "a consistência de P não é provável em P, desde que P seja consistente". Enquanto a prova de Gödel apresentava as ferramentas necessárias para Alonzo Church e Alan Turing para resolver o Entscheidungsproblem, ele próprio não o respondeu.

É dentro do décimo problema de Hilbert em que a questão de um "Entscheidungsproblem" na verdade aparece. O cerne da questão foi o seguinte questionamento: "O que queremos dizer quando dizemos que uma função é "efetivamente calculável'"? A resposta seria algo para este efeito: "Quando a função é calculado através de procedimentos mecânicos (processo, método)." Apesar de facilmente afirmado hoje em dia, a pergunta (e resposta) seria passaria sem resposta por quase 30 anos antes de ser construída precisamente.

A descrição original do décimo problema de Hilbert começa da seguinte maneira:

"10. Determinação da solubilidade de uma equação Diofantina. Dada uma equação Diofantina com um número qualquer de quantidades desconhecidas e coeficientes racionais integrais: Ache um processo pelo qual é possível determinar em um número finito de operações se a equação tem solução racional em números inteiros.

Por volta de 1922, a pergunta específica de um "Entscheidungsproblem" aplicada a equações Diofantinas haviam desenvolvido para a questão mais geral sobre um "método de decisão" para qualquer fórmula matemática. Martin Davis explica isso da seguinte maneira: Suponha que temos um "procedimento calculacional" que consiste de (1) um conjunto de axiomas e (2) uma conclusão lógica escrita em lógica de primeira ordem, que é escrito em que Davis chama de "Regras de dedução de Frege" (ou o equivalente moderno da lógica Booleana). A tese de doutorado de Gödel provou que as regras de Frege eram completas "... no sentido de que cada fórmula válida era provável". Dado este fato encorajador, poderia haver um "procedimento calculacional" generalizado que poderia nos dizer se uma conclusão poderia ser derivada a partir de suas premissas? Davis, chama tais procedimentos calculacionais de "algoritmos". O Entscheidungsproblem seria um algoritmo, sendo assim. "Em princípio, um algoritmo para [o] Entscheidungsproblem teria reduzido todo o raciocínio dedutivo humano para cálculos brutos".

Em outras palavras: existe um "algoritmo", que pode dizer-nos se qualquer fórmula é "verdadeira" (i.e. um algoritmo que sempre corretamente produz uma decisão "verdade" ou "falsidade"?)

"... parecia claro para Hilbert, que com a solução deste problema, o Entscheidungsproblem, que deve ser possível, em princípio, resolver todas as questões matemáticas de uma maneira puramente mecânica. Assim, considerando problemas insolúveis como todos, mesmo em caso de Hilbert estivesse correto, então o próprio Entscheidungsproblem deveria ser insolúvel".

De fato: E quanto ao nosso Entscheidungsproblem algoritmo por si só? Pode ele determinar, em um número finito de passos, se ele, ele próprio, é "bem-sucedido" e "verdadeiro" (que é, ele não fica pendurado em uma interminável "ciclo" ou "loop", e ele produz corretamente uma decisão "verdade" ou "falsidade" sobre seu próprio comportamento e resultados)?

Três problemas do 2º e 10º problema de Hilbert

Em 1928 no Congresso Internacional de Matemática [em Bolonha, Itália] Hilbert refina a questão com muito cuidado em três partes. O seguinte é o resumo de Stephen Hawking:

• "1. Para provar que todas as afirmações verdadeiras matemáticas poderiam ser provadas, isto é, a completude da matemática.
• "2. Para provar que só as verdadeiras afirmações matemáticas poderiam ser provadas, isto é, a consistência da matemática,
• "3. Para provar a decidibilidade da matemática, isto é, a existência de um processo de decisão para decidir a verdade ou a falsidade de qualquer proposição matemática."

Simples funções aritméticas irredutíveis à recursão primitiva

Gabriel Sudão (1927) e Wilhelm Ackermann (1928) mostram funções recursivas que não são recursões primitivas:

"Há recursões que não são redutíveis à recursão primitiva; e, em particular, recursividade pode ser usada para definir uma função que não é recursiva primitiva?

"Esta questão surgiu a partir de uma conjectura de Hilbert em 1926, sobre o problema contínuo, e foi respondida [sim: há recursões que não são recursões primitivas] por Ackermann em 1928."

Nos anos subsequentes Kleene observou que Rózsa Péter (1935) havia simplificado o exemplo de Ackermann (cf. também Hilbert-Bernays, 1934") e Raphael Robinson (1948). Péter expôs um outro exemplo (1935), que empregou o argumento da diagonalização de Cantor. Péter (1950) e Ackermann (1940) também apresentaram o "indução transfinita", e isso levou Kleene a questionar:

"... será que podemos caracterizar em qualquer maneira exata a noção de qualquer "recursividade", ou a classe de todas as "funções recursivas."

Kleene conclui que todas as recursões" envolvem: (i) a análise formal, que ele apresenta em seu §54 Cálculos Formais de primitivas de funções recursivas e, (ii) o uso de indução matemática. Ele imediatamente afirma que, de fato, a definição de Gödel-Herbrand, realmente "caracteriza todas as funções recursivas" – veja a citação em 1934, abaixo.

Prova de Gödel

Em 1930, os matemáticos se reuniram para uma matemática de reunião e evento de aposentadoria de Hilbert. Como ele teria sorte,

"na mesma reunião, um jovem matemático tcheco, Kurt Gödel, anunciou os resultados que tratavam a [opinião de Hilbert de que todas as três respostas foram SIM com] um sério golpe."

Ele anunciou que a resposta para os dois primeiros de Hilbert três perguntas, de 1928, seria NÃO.

Posteriormente, Gödel, em 1931, publicou o seu famoso artigo Sobre Formalmente Indecidíveis, Proposições dos Princípios da Matemática e Sistemas Relacionados I. Em seu prefácio para este artigo científico Martin Davis oferece um cuidado:

"O leitor deve ser advertido de que [neste artigo] o que Gödel chama de funções recursivas são agora chamadas de funções recursivas primitivas. (A terminologia revisada foi introduzida por Kleene)."

Expansão de Gödel do "cálculo efetivo"

Para citar Kleene (1952), "A caracterização de todas as "funções recursivas" foi realizada na definição geral de função recursiva' por Gödel em 1934, que a construiu sob uma sugestão de Herbrand" (Kleene 1952:274). Gödel proferiu uma série de palestras no Instituto de Estudos Avançados de Princeton, NJ. Em um prefácio escrito por Martin Davis Davis observa que

"Dr. Gödel afirmou em uma carta que ele foi, na época destas palestras, não estava nem um pouco convencido de que o seu conceito de recursividade compunha todas as possíveis recursões ..."

Dawson afirma que essas palestras foram feitas para esclarecer preocupações de que os "teoremas de incompletude foram, de alguma forma, dependente das particularidades da sua formalização":

"Gödel mencionou o exemplo de Ackermann na seção final de seu artigo de 1934, como uma forma de motivar o conceito de "função geral recursiva" que ele definiu lá, mas, anteriormente, na nota de rodapé 3, ele já tinha conjeturado (como "um princípio heurístico") que todas as funções finitamente computáveis poderiam ser obtidas através de recursões de tipos bem mais gerais.

"A conjectura desde então tem despertado muito comentário. Em particular, quando Martin Davis comprometeu-se a publicar as aulas de 1934 de Gödel [em Davis, 1965:41ff] ele levou-a para ser uma variante da Tese de Church; mas, em uma carta para Davis ... Gödel declarou enfaticamente que "não era verdade", porque no momento de suas palestras ele não estava "convencido de forma alguma" de seu conceito de recursividade composta por "todos os possíveis recursões." Em vez disso, ele disse, "A conjectura apenas se refere à equivalência de 'processos (computação) finitos" e " procedimento recursivo.'" Para esclarecer a questão Gödel adicionou um postscript para as aulas, , no qual ele disse que o que tinha, finalmente, o convencido, de que funções computáveis intuitivamente, coincidem com aquelas da recursividade geral do trabalho de de Alan Turing (Turing 1937).

"A relutância de Gödel de reconhecer a recursividade geral ou a λ-definibilidade como caracterização adequada da noção informal da computabilidade efetiva foi examinada em detalhe por diversos autores [nota de Rodapé 248: "Ver especialmente Davis, 1982; Gandy 1980 e 1988; Sieg 1994"]. Há um consenso de que, na verdade, nem os formalismos de Gödel, nem de Church foram tão lúcido ou intrinsecamente persuasivo como as análises de Alan Turing, e Wilfried Sieg argumentou que as evidências em favor da Tese de Church forneceram a "confluência de diferentes noções" (o fato de que os sistemas propostos por Church, Gödel, Pós e Alan Turing de todos acabou por ter a mesma extensão) é menos convincente do que geralmente se supõe. Assim, o cuidado inato de Gödel eram bons motivos para seu ceticismo. Mas o que, então, ele tentava alcançar através de sua noção de recursividade geral? ...

"Em vez disso, Gödel obteve a sua definição [da classe geral de funções recursivas] através de modificações das idéias de Herbrand ...; e Wilfried Sieg argumentou que o seu verdadeiro propósito na seção final do artigo de 1934 [as anotações de aula] eram "desassociar funções recursivas a partir de epistemologicamente [de Herbrand] da noção restrita de prova", especificando "regras mecânicas para derivar equações." O que era mais geral sobre a noção de Gödel de recursivamente "geral" era, Sieg sugere, que Herbrand tinha a intenção apenas de caracterizar as funções que poderiam ser provadas ser recursiva, por meios finitos [250]."

Kleene

Kleene e Rosser transcreveram as aulas de 1934 de Gödel em Princeton. Em seu papel Geral de Funções Recursivas de Números Naturais Kleene afirma:

"Uma definição geral de função recursiva dos números naturais foi sugerida por Herbrand para Gödel, e foi usada por Gödel, com uma modificação importante em uma série de palestras na universidade de Princeton, em 1934 ...

"Uma função recursiva (relação), no sentido de Gödel ... agora vai ser chamada de uma função recursiva primitiva (relação).

Definição de Church de "efetivamente calculável"

O artigo de Church Um Problema Insolúvel da Teoria Fundamental dos números (1936) provou que o Entscheidungsproblem era indecidível dentro do λ-calculus e da recursividade geral de Gödel-Herbrand; além disso, Church cita dois teoremas de Kleene que provava que as funções definidas no λ-cálculo são idênticas às funções definidas pelo recursão geral:

"Teorema XVI. Cada função recursiva de inteiros positivos é λ-definível.¹⁶

"Teorema XVII. Cada função λ-definida de números inteiros positivos é recursiva.¹⁷

"¹⁶ ... . Na forma aqui foi obtido primeiramente por Kleene... .

"¹⁷ Este resultado foi obtido de forma independente pelo presente autor e S. C. Kleene ao mesmo tempo.

O artigo começa com uma longa nota de rodapé, 3. Outra nota de rodapé, 9, é também de interesse. Martin Davis afirma que "Este artigo é principalmente importante para a sua explícita declaração (desde então conhecida como Tese de Church) de que as funções que podem ser calculada por um algoritmo finito são precisamente as funções recursivas, e por consequência o fato de um problema explícito insolúvel pode ser dado":

"³ Como será apresentado, esta definição de cálculo efetivo pode ser declarada em qualquer uma das duas formas equivalentes, (1) ... λ-definível ... 2) ... recursiva ... . A noção de λ-definibilidade é devido, em conjunto, ao presente autor e a S. C. Kleene, os sucessivos passos no sentido de esta ter sido tomada pelo autor em Anais de Matemática, vol. 34 (1933), p. 863, e Kleene no American Journal of Mathematics, vol. 57 (1935), p. 219. A noção de recursividade no sentido do §4, a seguir, é devido, em conjunto, a Jacques Herbrand e Kurt Gödel, como está lá explicado. E a prova de equivalência dos dois conceitos é devido, essencialmente, ao Kleene, mas também, em parte, ao presente autor, e a J. B. Rosser ... . A proposta de identificar estas noções com a noção intuitiva de cálculo efetivo é feita pela primeira vez no presente artigo (ver a primeira nota de rodapé do §7 abaixo).

"Com o auxílio dos métodos de Kleene (Jornal Americano de Matemática, 1935), as considerações do presente artigo pode, comparativamente com ligeira modificação ser realizada inteiramente em termos de λ-definibilidade, sem fazer uso da noção de recursiveness. Por outro lado, uma vez que os resultados da presente pesquisa foram obtidos, foi demonstrado por Kleene (consulte seu próximo papel, "Funções recursivas gerais de números naturais") que análogos resultados podem ser obtidos inteiramente em termos de recursividade, sem fazer uso de λ-definibilidade. O fato, no entanto, que essas duas diferentem muito e, na opinião do autor, igualmente natural definições de efetivo calculability vir a ser equivalente acrescenta à força das razões apresentadas abaixo para crer que elas constituem uma forma geral, uma caracterização desta noção de como é consistente com a habitual compreensão intuitiva."

Nota de rodapé 9 encontra-se na seção §4 funções Recursivas:

"⁹Esta definição [de "recursiva"] está intimamente relacionada, e foi sugerido por uma definição de funções recursivas, que foi proposta por Kurt Gödel, em palestras na universidade de Princeton, N. J., de 1934, e creditada por ele, em parte, a uma inédita sugestão de Jacques Herbrand. As principais funções em que a presente definição de recursividade difere de Gödel são devido a S. C. Kleene.

"Em um próximo artigo por Kleene para ser intitulado "Geral de funções recursivas de números naturais," ... segue ... que toda função recursiva no presente sentido também é recursiva, no sentido de Gödel (1934) e, por outro lado."

Algum tempo antes do artigo de Church de Um Problema Insolúvel de Teoria de números (1936) um diálogo ocorrido entre Gödel e a Church se ou não λ-definibilidade seria suficiente para a definição da noção de "algoritmo" e "eficazmente calculável".

Em Church (1936) vemos, sob o capítulo §7 A noção de cálculo efetivo, uma nota de rodapé 18, que afirma o seguinte:

"¹⁸A questão da relação entre a calculabilidade efetiva e recursão (que é aqui proposto, para responder pela identificação de duas noções) foi criada por Gödel, em conversa com o autor. A correspondente questão da relação entre a calculabilidade efetiva e λ-definibilidade anteriormente tinha sido proposta pelo autor de forma independente."

Por "identificação" Church significa – não ", que estabelece a identidade do" – mas, ao invés de "fazer ser ou tornar-se idêntico", "conceber unidos" (como no espírito, o outlook ou princípio) (vt), e (vi) como "ser ou tornar-se o mesmo".

Post e "calculabilidade eficaz" como "lei natural"

Post dúvidas quanto recursão era uma definição adequada de "eficazmente calculável", além da publicação do artigo de Church, encorajou-o no outono de 1936, ao propor uma "formulação" com "fidelidade psicológica": Um trabalhador que se move através de "uma seqüência de espaços ou caixas" desempenhando o papel como de uma máquina de "atos primitivos" em uma folha de papel em cada caixa. O trabalhador está equipado com "um fixo conjunto alterável de direções". Cada instrução é composta de três ou quatro símbolos: (1) uma etiqueta de identificação/número, (2) uma operação, (3) a próxima instrução j_i; no entanto, se a instrução for do tipo (e), e a determinação é "sim", em SEGUIDA, a instrução j_i' COISA se ele for "não" a instrução j_eu. O "atos primitivos" são de apenas 1 em 5 tipos: (a) marcar o papel na caixa, ele (ou sobre-marca de uma marca já existe), (b) apagar a marca (ou apagar), (c) mover-se em uma sala para direita, (d) mover uma sala para a esquerda, (e) determinar se o papel estiver assinalada ou em branco. O trabalho é iniciado no passo 1 na partida de quarto, e faz o que as instruções instruí-los a fazer. (Veja mais no Post-Turing.)

Este assunto, mencionado na introdução sobre "teorias intuitivas" causaria um grande incômodo de Post sobre Church:

"The writer expects the present formulation to turn out to be logically equivalent to recursiveness in the sense of the Gödel-Church development.⁷ Its purpose, however, is not only to present a system of a certain logical potency but also, in its restricted field, of psychological fidelity. In the latter sense wider and wider formulations are contemplated. On the other hand, our aim will be to show that all such are logically reducible to formulation 1. We offer this conclusion at the present moment as a working hypothesis. And to our mind such is Church's identification of effective calculability with recursivness.⁸" (italics in original)

⁷ [he sketches an approach to a proof]

⁸ "Cf. Church, lock. cit, pp. 346, 356-358. Actually the work already done by Church and others carries this identification considerably beyond the working hypothesis stage. But to mask this identification under a definition hides the fact that a fundamental discovery in the limitiations of mathematicizing power of Homo Sapiens has been made and blinds us to the need of its continual verification."

In other words Post is saying "Just because you defined it so doesn't make it truly so; your definition is based on no more than an intuition." Post was searching for more than a definition: "The success of the above program would, for us, change this hypothesis not so much to a definition or to an axiom but to a natural law. Only so, it seems to the writer, can Gödel's theorem ... and Church's results ... be transformed into conclusions concerning all symbolic logics and all methods of solvability."

This contentious stance finds grumpy expression in Alan Turing 1939, and it will reappear with Gödel, Gandy, and Sieg.

Turing e computabilidade

A. M. Turing's paper On Computable Numbers, With an Application to the Entscheidungsproblem was delivered to the London Mathematical Society in November 1936. Again the reader must bear in mind a caution: as used by Turing, the word "computer" is a human being, and the action of a "computer" he calls "computing"; for example, he states "Computing is normally done by writing certain symbols on paper" (p. 135). But he uses the word "computation" in the context of his machine-definition, and his definition of "computable" numbers is as follows:

"The "computable" numbers may be described briefly as the real numbers whose expressions as a decimal are calculable by finite means ... .According to my definition, a number is computable if its decimal can be written down by a machine."

What is Turing's definition of his "machine?" Turing gives two definitions, the first a summary in §1 Computing machines and another very similar in §9.I derived from his more detailed analysis of the actions a human "computer". With regards to his definition §1 he says that "justification lies in the fact that the human memory is necessarily limited", and he concludes §1 with the bald assertion of his proposed machine with his use of the word "all"

"It is my contention that these operations [write symbol on tape-square, erase symbol, shift one square left, shift one square right, scan square for symbol and change machine-configuration as a consequence of one scanned symbol] include all those which are used in the computation of a number."

The emphasis of the word one in the above brackets is intentional. With regards to §9.I he allows the machine to examine more squares; it is this more-square sort of behavior that he claims typifies the actions of a computer (person):

"The machine scans B squares corresponding to the B squares observed by the computer. In any move the machine can change a symbol on a scanned square or can change any one of the scanned squares to another square distant not more than L squares from one of the other scanned squares ... The machines just described do not differ very essentially from computing machines as defined in §2 [sic], and corresponding to any machine of this type a computing machine can be constructed to compute the same sequence, that is to say the sequence computed by the computer."

Turing goes on to define a "computing machine" in §2 is (i) "a-machine" ("automatic machine") as defined in §1 with the added restriction (ii): (ii) It prints two kinds of symbols – figures 0 and 1 – and other symbols. The figures 0 and 1 will represent "the sequence computed by the machine".

Furthermore, to define the if the number is to be considered "computable", the machine must print an infinite number of 0's and 1's; if not it is considered to be "circular"; otherwise it is considered to be "circle-free":

"Um número é computável se difere por um número inteiro de o número calculado por uma máquina livre de ciclos."

Although he doesn't call it his "thesis", Turing proposes a proof that his "computability" is equivalent to Church's "effective calculability":

"In a recent paper Alonzo Church has introduced an idea of "effective calculability", which is equivalent to my "computability", but is very differently defined ... The proof of equivalence between "computability" and "effective calculability" is outlined in an appendix to the present paper."

The Appendix: Computability and effective calculability begins in the following manner; observe that he does not mention recursion here, and in fact his proof-sketch has his machine munch strings of symbols in the λ-calculus and the calculus munch "complete configurations" of his machine, and nowhere is recursion mentioned. The proof of the equivalence of machine-computability and recursion must wait for Kleene 1943 and 1952:

"The theorem that all effectively calculable (λ-definable) sequences are computable and its converse are proved below in outline."

Gandy (1960) seems to confuse this bold proof-sketch with Church's Thesis; see 1960 and 1995 below. Moreover a careful reading of Turing's definitions leads the reader to observe that Turing was asserting that the "operations" of his proposed machine in §1 are sufficient to compute any computable number, and the machine that imitates the action of a human "computer" as presented in §9.I is a variety of this proposed machine. This point will be reiterated by Turing in 1939.

Turing identifica calculabilidade efetiva com computação de máquina

Alan Turing's massive Princeton PhD thesis (under Alonzo Church) appears as Systems of Logic Based on Ordinals. In it he summarizes the quest for a definition of "effectively calculable". He proposes a definition as shown in the boldface type that specifically identifies (renders identical) the notions of "machine computation" and "effectively calculable".

"A function is said to be "effectively calculable" if its values can be found by some purely mechanical process. Although it is fairly easy to get an intuitive grasp of this idea, it is nevertheless desirable to have some more definite, mathematically expressible definition. Such a definition was first given by Gödel at Princeton in 1934 ... . These functions are described as "general recursive" by Gödel ... . Another definition of effective calculability has been given by Church ... who identifies it with λ-definability. The author has recently suggested a definition corresponding more closely to the intuitive idea (Turing [1], see also Post's [1]). It was stated above that "a function is effectively calculable if its values can be found by some purely mechanical process". We may take this statement literally, understanding by a purely mechanical process one which could be carried out by a machine. It is possible to give a mathematical description, in a certain normal form, of the structures of these machines. The development of these ideas leads to the author's definition of a computable function, and to an identification of computability † with effective calculability. It is not difficult, though somewhat laborious, to prove that these three definitions are equivalent.

"† We shall use the expression "computable function" to mean a function calculable by a machine, and we let "effectively calculable" refer to the intuitive idea without particular identification with any one of these definitions. We do not restrict the values taken by a computable function to be natural numbers; we may for instance have computable propositional functions."

This is a powerful expression. because "identicality" is actually an unequivocal statement of necessary and sufficient conditions, in other words there are no other contingencies to the identification" except what interpretation is given to the words "function", "machine", "computable", and "effectively calculable":

For all functions: IF "this function is computable by machine" THEN "this function is effectively calculable" AND IF "this function is effectively calculable" THEN "this function is computable by a machine."

Rosser: recursão, λ-cálculo, e computação de identidade da máquina de Turing

J. B. Rosser's paper An Informal Exposition of Proofs of Gödel's Theorem and Church's Theorem states the following:

"'Effective method' is here used in the rather special sense of a method each step of which is precisely predetermined and which is certain to produce the answer in a finite number of steps. With this special meaning, three different precise definitions have been given to date⁵. The simplest of these to state (due to Post and Turing) says essentially that an effective method of solving a certain set of problems exists if one can build a machine which will then solve any problem of the set with no human intervention beyond inserting the question and (later) reading the answer. All three definitions are equivalent, so it does not matter which one is used. Moreover, the fact that all three are equivalent is a very strong argument for the correctness of any one.

⁵ One definition is given by Church in I [i.e. Church 1936 An Unsolvable Problem of Elementary Number theory]. Another definition is due to Jacques Herbrand and Kurt Gödel. It is stated in I, footnote 3, p. 346. The third definition was given independently in two slightly different forms by E. L. Post ... and A. M. Turing ... . The first two definitions are proved equivalent in I. The third is proved equivalent to the first two by A. M. Turing, Computability and λ-definability [Journal of Symbolic Logic, vol. 2 (1937), pp. 153-163]."

Kleene e Tese I

Kleene defines "general recursive" functions and "partial recursive functions" in his paper Recursive Predicates and Quantifiers. The representing function, mu-operator, etc make their appearance. He goes on in §12 Algorithm theories to state his famous Thesis I, what he would come to call Church's Thesis in 1952:

"This heuristic fact, as well as certain reflections on the nature of symbolic algorithmic processes, led Church to state the following thesis²². The same thesis is implicitly in Turing's description of computing machines²³.

"Thesis I. Every effectively calculable function (effectively decidable predicate) is general recursive.

"Since a precise mathematical definition of the term effectively calculable (effectively decidable) has been wanting, we can take this thesis, together with the principle already accepted to which it is converse, as a definition of it ... the thesis has the character of an hypothesis – a point emphasized by Post and by Church²⁴.

²² Church [1] [An Unsolvable Problem of Elementary Number Theory]

²³ Turing [1] [On Computable numbers, with an application to the Entscheidungsproblem(1936)]

²⁴ Post [1, p. 105], and Church [2]

Teses de Kleene, Church, e Turing

In his chapter §60, Kleene defines the "Church's thesis" as follows:

" ... heuristic evidence and other considerations led Church 1936 to propose the following thesis.

"Thesis I. Every effectively calculable function (effectively decidable predicate) is general recursive.

"This thesis is also implicit in the conception of a computing machine formulated by Turing 1936-7 and Post 1936."

On page 317 he explicitly calls the above thesis "Church's thesis":

"§62. Church's thesis. One of the main objectives of this and the next chapter is to present the evidence for Church's thesis (Thesis I §60)."

About Turing's "formulation", Kleene says:

"Turing's formulation hence constitutes an independent statement of Church's thesis (in equivalent terms). Post 1936 gave a similar formulation."

Kleene proposes that what Turing showed: "Turing's computable functions (1936-1937) are those which can be computed by a machine of a kind which is designed, according to his analysis, to reproduce all the sorts of operations which a human computer could perform, working according to preassigned instructions."

This interpretation of Turing plays into Gandy's concern that a machine specification may not explicitly "reproduce all the sorts of operations which a human computer could perform" – i.e. his two examples are (i) massively symbol-parallel computation and two-dimensional computation e.g. Conway's "game of life". Therefore there may be processes that can "compute more" than a Turing machine can. See 1980 below.

Kleene defines Turing's Thesis as follows:

"§70. Turing's thesis. Turing's thesis that every function which would naturally be regarded as computable under his definition, i.e. by one of his machines, is equivalent to Church's thesis by Theorem XXX."

Indeed immediately before this statement, Kleene states the Theorem XXX:

"Theorem XXX (= Theorems XXVIII + XXIX). The following classes of partial functions are coextensive, i.e. have the same members: (a) the partial recursive functions, (b) the computable functions, (c) the 1/1 computable functions. Similarly with l [lower-case L] completely defined assumed functions Ψ."

Gödel, Máquinas de Turing, e calculabilidade efetiva

To his 1931 paper On Formally Undecidable Propositions, Gödel added a Note added 28 August 1963 which clarifies his opinion of the alternative forms/expression of "a formal system". He reiterates his opinions even more clearly in 1964 (see below):

"Note Added 28 August 1963. In consequence of later advances, in particular of the fact that due to A. M. Turing's work⁶⁹ a precise and unquestionably adequate definition of the general notion of formal system⁷⁰ can now be given, a completely general version of Theorems VI and XI is now possible. That is, it can be proved rigorously that in every consistent formal system that contains a certain amount of finitary number theory there exist undecidable arithmetic propositions and that, moreover, the consistency of any such system cannot be proved in the system.

"⁶⁹ See Turing 1937, p. 249.

"⁷⁰ In my opinion the term "formal system" or "formalism" should never be used for anything but this notion. In a lecture at Princeton (mentioned in Princeton University 1946, p. 11 [see Davis 1965, pp. 84-88 [i.e. Davis p. 84-88] ]), I suggested certain transfinite generalizations of formalisms, but these are something radically different from formal systems in the proper sense of the term, whose characteristic property is that reasoning in them, in principle, can be completely replaced by mechanical devices."

Gödel 1964 – In Gödel's Postscriptum to his lecture's notes of 1934 at the IAS at Princeton, he repeats, but reiterates in even more bold terms, his less-than-glowing opinion about the efficacy of computability as defined by Church's λ-definability and recursion (we have to infer that both are denigrated because of his use of the plural "definitions" in the following). This was in a letter to Martin Davis (presumably as he was assembling The Undecidable). The repeat of some of the phrasing is striking:

"In consequence of later advances, in particular of the fact, that, due to A. M. Turing's work, a precise and unquestionably adequate definition of the general concept of formal system can now be given, the existence of undecidable arithmetical propositions and the non-demonstrability of the consistence of a system in the same system can now be proved rigorously for every consistent formal system containing a certain amount of finitary number theory.

"Turing's work gives an analysis of the concept of "mechanical procedure" (alias "algorithm" or "computation procedure" or "finite combinatorial procedure"). This concept is shown to be equivalent to that of a "Turing machine".* A formal system can simply be defined to be any mechanical procedure for producing formulas, called provable formulas ... the concept of formal system, whose essence it is that reasoning is completely replaced by mechanical operations on formulas. (Note that the question of whether there exist finite non-mechanical procedures ... not equivalent with any algorithm, has nothing whatsoever to do with the adequacy of the definition of "formal system" and of "mechanical procedure.

"... if "finite procedure" is understood to mean "mechanical procedure", the question raised in footnote 3 can be answered affirmatively for recursiveness as defined in §9, which is equivalent to general recursiveness as defined today (see S. C. Kleene (1936) ...)"

" * See Turing 1937 ... and the almost simultaneous paper by E. L. Post (1936) ... . As for previous equivalent definitions of computability, which however, are much less suitable for our purpose, see A. Church 1936 ..."

Footnote 3 is in the body of the 1934 lecture notes:

"³ The converse seems to be true, if besides recursions according to the scheme (2) recursions of other forms (e.g., with respect to two variables simultaneously) are admitted. This cannot be proved, since the notion of finite computation is not defined, but it serves as a heuristic principle."

Davis does observe that "in fact the equivalence between his [Gödel's] definition [of recursion] and Kleene's [1936] is not quite trivial. So, despite appearances to the contrary, footnote 3 of these lectures is not a statement of Church's thesis."

Gandy: "computação de máquina", discreta, deterministica, e limitada por to "causação local" pela velocidade da luz

Robin Gandy's influential paper titled Church's Thesis and Principles for Mechanisms appears in Barwise et al. Gandy starts off with an unlikely expression of Church's Thesis, framed as follows:

"1. Introduction

"Throughout this paper we shall use "calculable" to refer to some intuitively given notion and "computable" to mean "computable by a Turing machine"; of course many equivalent definitions of "computable" are now available.

"Church's Thesis. What is effectively calculable is computable.

" ... Both Church and Turing had in mind calculation by an abstract human being using some mechanical aids (such as paper and pencil)"

Robert Soare (1995, see below) had issues with this framing, considering Church's paper (1936) published prior to Turing's "Appendix proof" (1937).

Gandy attempts to "analyze mechanical processes and so to provide arguments for the following:

"Tese de M. O que pode ser calculado através de uma máquina computável."

Gandy "exclude[s] from consideration devices which are essentially analogue machines ... .The only physical presuppositions made about mechanical devices (Cf Principle IV below) are that there is a lower bound on the linear dimensions of every atomic part of the device and that there is an upper bound (the velocity of light) on the speed of propagation of change". But then he restricts his machines even more:

"(2) Secondly we suppose that the progress of calculation by a mechanical device may be described in discrete terms, so that the devices considered are, in a loose sense, digital computers.

"(3) Lasty we suppose that the device is deterministic: that is, the subsequent behavior of the device is uniquely determined once a complete description of its initial state is given."

He in fact makes an argument for this "Thesis M" that he calls his "Theorem", the most important "Principle" of which is "Principle IV: Principle of local causation":

"Now we come to the most important of our principles. In Turing's analysis the requirement that the action depended only on a bounded portion of the record was based on a human limitation. We replace this by a physical limitation which we call the principle of local causation. Its justification lies in the finite velocity of propagation of effects and signals: contemporary physics rejects the possibility of instantaneous action at a distance."

Soare

Soare's thorough examination of Computability and Recursion appears. He quotes Gödel's 1964 opinion (above) with respect to the "much less suitable" definition of computability, and goes on to add:

"Kleene wrote [1981b, p. 49], "Turing's computability is intrinsically persuasive" but "λ-definability is not intrinsically persuasive" and "general recursiveness scarcely so (its author Gödel being at the time not at all persuaded) ... . Most people today accept Turing's Thesis"

Soare's footnote 7 (1995) also catches Gandy's "confusion", but apparently it continues into Gandy (1988). This confusion represents a serious error of research and/or thought and remains a cloud hovering over his whole program:

"⁷Gandy actually wrote "Church's thesis" not "Turing's thesis" as written here, but surely Gandy meant the latter, at least intensionally, because Turing did not prove anything in 1936 or anywhere else about general recursive functions."

Breger e o problema de axiomas tácitos

Breger points out a problem when one is approaching a notion "axiomatically", that is, an "axiomatic system" may have imbedded in it one or more tacit axioms that are unspoken when the axiom-set is presented.

For example, an active agent with knowledge (and capability) may be a (potential) fundamental axiom in any axiomatic system: "the know-how of a human being is necessary – a know-how which is not formalized in the axioms. ¶ ... Mathematics as a purely formal system of symbols without a human being possessing the know-how with the symbols is impossible ..."

He quotes Hilbert:

"In a university lecture given in 1905, Hilbert considered it "absolutely necessary" to have an "axiom of thought" or "an axiom of the existence of an intelligence" before stating the axioms in logic. In the margin of the script, Hilbert added later: "the a priori of the philosophers." He formulated this axiom as follows: "I have the capacity to think of objects, and to denote them by means of simple symbols like a, b,..., x, y,..., so that they can be recognized unambiguously. My thought operates with these objects in a certain way according to certain rules, and my thinking is able to detect these rules by observation of myself, and completely to describe these rules" [(Hilbert 1905,219); see also (Peckhaus 1990, 62f and 227)]."

Breger further supports his argument with examples from Giuseppe Veronese (1891) and Hermann Weyl (1930-1). He goes on to discuss the problem of then expression of an axiom-set in a particular language: i.e. a language known by the agent, e.g. German.

Veja mais sobre isso no Algoritmo de caracterizações, em particular a opinião de Searle de que, fora de qualquer computação tem de haver um observador que dá significado para os símbolos utilizados.

Sieg e definições axiomáticas

At the "Feferfest" – Solomon Feferman's 70th birthday – Wilfried Sieg first presents a paper written two years earlier titled "Calculations By Man and Machine: Conceptual Analysis", reprinted in (Sieg et al. 2002:390–409). Earlier Sieg published "Mechanical Procedures and Mathematical Experience" (in George 1994, p. 71ff) presenting a history of "calculability" beginning with Richard Dedekind and ending in the 1950s with the later papers of Alan Turing and Stephen Cole Kleene. The Feferfest paper distills the prior paper to its major points and dwells primarily on Robin Gandy's paper of 1980. Sieg extends Turing's "computability by string machine" (human "computor") as reduced to mechanism "computability by letter machine" to the parallel machines of Gandy.

Sieg cites more recent work including "Kolmogorov and Uspensky's work on algorithms" and (De Pisapia 2000), in particular, the KU-pointer machine-model), and artificial neural networks and asserts:

"The separation of informal conceptual analysis and mathematical equivalence proof is essential for recognizing that the correctness of Turing's Thesis (taken generically) rests on two pillars; namely on the correctness of boundedness and locality conditions for computors, and on the correctness of the pertinent central thesis. The latter asserts explicitly that computations of a computor can be mimicked directly by a particular kind of machine. However satisfactory one may find this line of analytic argument, there are two weak spots: the looseness of the restrictive conditions (What are symbolic configurations? What changes can mechanical operations effect?) and the corresponding vagueness of the central thesis. We are, no matter how we turn ourselves, in a position that is methodologically still unsatisfactory ... ."

He claims to "step toward a more satisfactory stance ... [by] abstracting further away from particular types of configurations and operations ..."

"It has been claimed frequently that Turing analyzed computations of machines. That is historically and systematically inaccurate, as my exposition should have made quite clear. Only in 1980 did Turing's student, Robin Gandy, characterize machine computations."

Whether the above statement is true or not is left to the reader to ponder. Sieg goes on to describe Gandy's analysis (see above 1980). In doing so he attempts to formalize what he calls "Gandy machines" (with a detailed analysis in an Appendix). About the Gandy machines:

" ... the definition of a Gandy machine is an "abstract" mathematical definition that embodies ... properties of parallel computations ... Second, Gandy machines share with groups and topological spaces the general feature of abstract axiomatic definitions, namely, that they admit a wide variety of different interpretations. Third, ... the computations of any Gandy machine can be simulated by a letter machine, [and] is best understood as a representation theorem for the axiomatic notion. [boldface added]

"The axiomatic approach captures the essential nature of computation processes in an abstract way. The difference between the two types of calculators I have been describing is reduced to the fact that Turing computors modify one bounded part of a state, whereas Gandy machines operate in parallel on arbitrarily many bounded parts. The representation theorems guarantee that models of the axioms are computationally equivalent to Turing machines in their letter variety."

Ver também

• Tese de Church-Turing

References

• Barwise, Jon, H. J. Keisler, and K. Kunen, Editors, 1980, The Kleene Symposium, 426 pages, North-Holland Publishing Company, Amsterdam, ISBN 0-444-85345-6
• Church, A., 1936a, in (Davis 1965:88ff), "An Unsolvable Problem of Elementary Number Theory"
• Church, A., 1936b, in (Davis 1965:108ff), "A Note on the Entscheidungsproblem"
• Church, A., 1938, The constructive second number class, Bull. Amer. Math. Soc. vol. 44, Number 4, 1938, pp. 224–232]
• Davis, Martin editor, 1965, The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions, Raven Press, New York, ISBN 0-911216-01-4. All the original papers are here including those by Gödel, Church, Turing, Rosser, Kleene, and Post mentioned in this article. Valuable commentary by Davis prefaces most papers.
• Davis, Martin, 2001, Engines of Logic: Mathematicians and the Origin of the Computer, W. W. Norton & Company, New York, ISBN 0-393-04785-7 pbk.
• Dawson, John William, Jr., 1997, Logical Dilemmas: The Life and Work of Kurt Gödel, 361 pages, A. K. Peters, Wellesley, MA, ISBN 1-56881-025-3, QA29.058D39.
• Dawson, John William and John William Dawson, Jr., 2005, Logical Dilemmas: The Life and Work of Kurt Gödel, 362 pages, A. K. Peters, Wellesley, MA, ISBN 978-1-56881-025-6
• De Pisapia, N., 2000, Gandy Machines: an abstract model of parallel computation for Turing Machines, the Game of Life, and Artificial Neural Networks, M.S. Thesis, Carnegie Mellon University, Pittsburgh.
• Dershowitz, Nachum and Gurevich, Yuri, 2007, A Natural Axiomatization of Church's Thesis, http://research.microsoft.com/~gurevich/Opera/188.pdf
• Gandy, Robin, 1978, Church's Thesis and the Principles for Mechanisms, in (Barwise et al. 1980:123-148)
• George, Alexander (+ed.), 1994, Mathematics and Mind, 216 pages, New York, Oxford University Press, ISBN 0-19-507929-9
• Gödel, K., 1930, in (van Heijenoort 1967:592ff), Some metamathematical results on completeness and consistency
• Gödel, K., 1931a, in (Davis 1965:4-38), On Formally Undecidable Propositions of the Principia Mathematica and Related Systems. I.
• Gödel, K., 1931b, in (van Heijenoort 1976:616ff) On completeness and consistency
• Gödel, K., 1934, in (Davis 1965:39-74), On Undecidable Propositions of Formal Mathematical Systems
• Gödel, K., 1936, in (Davis 1965:82ff), On The Length of Proofs, "Translated by the editor from the original article in Ergenbnisse eines mathematishen Kolloquiums, Heft 7 (1936) pp. 23-24." Cited by Kleene (1952) as "Über die Lāange von Beweisen", in Ergebnisse eines math. Koll, etc.
• Gödel, K., 1964, in (Davis 1965:71ff), Postscriptum
• Groshoz, Emily and Breger, Herbert, 2000, The Growth of Mathematical Knowledge, 416 pages, Kluwer Academic Publishers, Dordrect, The Netherlands, ISBN 0-7923-6151-2.
• Hawking, Stephen, 2005, God Created the Integers: The Mathematical Breakthroughs that Changed History, Edited, with Commentary by Stephen Hawking, Running Press, Philadelphia, ISBN 0-7624-1922-9
• Hodges, Andrew, 1983 , Alan Turing:The Engima, 1st edition, Simon and Schuster, New York, ISBN 0-671-52809-2
• Kleene, S. C., 1935, in (Davis 1965:236ff) General Recursive Functions of Natural Numbers
• Kleene, S. C., 1971, 1952 (10th impression 1991) Introduction to Metamathematics, 550 pages, North-Holland Publishing Company (Wolters-Noordhoff Publishing) ISBN 0-7204-2103-9
• Merriam-Webster Inc., 1983, Webster's Ninth New Collegiate Dictionary, 1563 pages, Merriam-Webster Inc., Springfield, MA, ISBN 0-87779-509-6
• Post, E. L., 1936, in (Davis 1965:288ff), Finite Combinatory Processes - Formulation 1 or The Journal of Symbolic Logic, Vol. 1, No. 3 (Sep., 1936), pp. 103–105.
• Rosser. J. B., 1939, An informal exposition of proofs of Gödel's Theorem and Church's Theorem, The Journal of Symbolic Logic. Vol. 4. (1939), pp. 53–60 and reprinted in (Davis 1967:223-230).
• Sieg, Wilfried, Richard Sommer, and Carolyn Talcott (eds.), 2002, Reflections on the Foundations of Mathematics: Essays in Honor of Solomon Feferman, Lecture Notes in Logic 15, 444 pages, A K Peters, Ltd., ISBN 1-56881-169-1
• Soare, Robert, 1996, Computability and Recursion, "Bulletin of Symbolic Logic 2", Volume 2, Number 3, September 1996, pp. 284–321.
• Turing, A. M. (1937) [Delivered to the Society 1936], «On Computable Numbers, with an Application to the Entscheidungsproblem» (PDF), Proceedings of the London Mathematical Society, 2, 42, pp. 230–65, doi:10.1112/plms/s2-42.1.230  and Turing, A.M. (1938). «On Computable Numbers, with an Application to the Entscheidungsproblem: A correction». Proceedings of the London Mathematical Society. 2. 43 (publicado em 1937). pp. 544–6. doi:10.1112/plms/s2-43.6.544  (See also: Davis 1965:115ff)
• Turing, A., 1939, in (Davis 1965:154ff), Systems of Logic Based on Ordinals
• van Heijenoort, Jean, 1976, From Frege To Gödel: A Source Book in Mathematical Logic, 116 pages, 1879–1931, 3rd Printing, original printing 1967, Harvard University Press, Cambridge Massachusetts, ISBN 0-674-31844-7 (pbk.).

Ligações externas

• O Boletim de Lógica Simbólica tem links para todos os volumes com papers on line.
• Alonzo Church, De 1938, The Constructive Second Number Class "Um discurso proferido por convite do Comitê de Programa da reunião da Society em Indianapolis, de 29 de dezembro de 1937."
• Kurt Gödel, em 1931, On formally undecidable propositions of Principia Mathematica and related systems I. Traduzido por Martin Hirzel, 27 de novembro de 2000.
• Emil L. Post, 1946, A Variant of a Recursively Unsolvable Problem
• Wilfried Sieg, 2005, CHURCH WITHOUT DOGMA: Axioms for computability, Carnegie Mellon University
• Wilfried Sieg, 2000, Calculations By Man and Machine: conceptual analysis, Carnegie Mellon University
• Robert I. Soare, 1995, Computability and Recursion
• Robert I. Soare, 1996, Computability and Recursion como ele apareceu no Boletim da Lógica Simbólica, Volume 2, Volume 2, Número 3, setembro de 1996.
• Masako Takahashi, 2004, On general recursive functions, International Christian University, em Particular, ver referências bibliográficas.
• A. M. Turing, 1936, On Computable Numbers, with an Application to the Entscheidungsproblem