Sobre a Filosofia Formalista da Matemática - Parte II

 Nesta postagem, estou dando continuidade à discussão anterior sobre o Programa Formalista da Matemática a partir da versão original de Hilbert e cogitando a possibilidade de uma reformulação do referido programa a partir de certos aspectos lógico-formais com base em um resultado obtido em Sarmento (2022).

Considere-se, inicialmente, o seguinte texto:  entrada da Stanford Encyclopedia of Philosophy sobre Hilbert’s Program [First published Thu Jul 31, 2003; substantive revision Fri May 24, 2019] o autor Prof. Richard Zach observa que:

"According to Hilbert, there is a privileged part of mathematics, contentual elementary number theory, which relies only on a 'purely intuitive basis of concrete signs'. Whereas the operating with abstract concepts was considered 'inadequate and uncertain', there is a realm of

extra-logical discrete objects, which exist intuitively as immediate experience before all thought. If logical inference is to be certain, then these objects must be capable of being completely surveyed in all their parts, and their presentation, their difference, their succession (like the objects themselves) must exist for us immediately, intuitively, as something which cannot be reduced to something else. (Hilbert 1922b, 202; the passage is repeated almost verbatim in Hilbert 1926, 376, Hilbert 1928, 464, and Hilbert 1931b, 267)

These objects were, for Hilbert, signs. The domain of contentual number theory consists in the finitary numerals, i.e., sequences of strokes. These have no meaning, i.e., they do not stand for abstract objects, but they can be operated on (e.g., concatenated) and compared. Knowledge of their properties and relations is intuitive and unmediated by logical inference. Contentual number theory developed this way is secure, according to Hilbert: no contradictions can arise simply because there is no logical structure in the propositions of contentual number theory.

The intuitive-contentual operations with signs forms the basis of Hilbert’s metamathematics. Just as contentual number theory operates with sequences of strokes, so metamathematics operates with sequences of symbols (formulas, proofs). Formulas and proofs can be syntactically manipulated, and the properties and relationships of formulas and proofs are similarly based in a logic-free intuitive capacity which guarantees certainty of knowledge about formulas and proofs arrived at by such syntactic operations. Mathematics itself, however, operates with abstract concepts, e.g., quantifiers, sets, functions, and uses logical inference based on principles such as mathematical induction or the principle of the excluded middle. These “concept-formations” and modes of reasoning had been criticized by Brouwer and others on grounds that they presuppose infinite totalities as given, or that they involve impredicative definitions (which were considered by the critics as viciously circular). Hilbert’s aim was to justify their use. To this end, he pointed out that they can be formalized in axiomatic systems (such as that of Principia or those developed by Hilbert himself), and mathematical propositions and proofs thus turn into formulas and derivations from axioms according to strictly circumscribed rules of derivation. Mathematics, so Hilbert, “becomes an inventory of provable formulas.” In this way the proofs of mathematics are subject to metamathematical, contentual investigation. The goal of Hilbert’s program is then to give a contentual, metamathematical proof that there can be no derivation of a contradiction, i.e., no formal derivations of a formula $A$ and of its negation $\neg A$. [Meus itálicos destacados em vermelho].

    A respeito dessa caracterização geral do programa formalista de Hilbert, W. Stegmüller (1977), pág. 341, observa que: "A parte essencialmente clássica [da matemática] é reconstruída axiomaticamente e inteiramente formalizada, mediante uso da lógica matemática; transforma-se, desse modo, em puro cálculo. A  outra parte, ou seja, a metamatemática, tem feição bem diversa: não se trata de teoria formalizada, mas, ao contrário, de teoria dotada de conteúdo e formulada em linguagem comum. Seu objeto de estudo é aquele puro cálculo, cabendo-lhe apresentar provas de que a teoria matemática, transformada em cálculo, está livre de contradições (é consistente). Na verificação metamatemática de que inexistem as contradições, só devem ser empregados, conforme Hilbert, os métodos que são aceitos pelos intuicionistas. ... As maneiras de inferir que, sob o prisma intuicionista, se mostram passíveis de crítica são utilizadas apenas na matemática formalizada; na metamatemática, ao contrário, só aparecem inferências que o intuicionismo considera isentas de crítica."

    Em ambos os extratos acima, de Zach e Stegmüller, foi enfatizado que em nível metamatemático -com o intuito de estabelecer provas de consistência das teorias matemáticas formalizadas-  somente seriam admissíveis procedimentos finitários estabelecidos pelos intuicionistas como legítimos, a saber, a utilização do princípio do terceiro-excluído apenas para conjuntos de cardinalidade finita, a rejeição de definições impredicativas e a possibilidade de existência de problemas indecidíveis na aritmética, haja vista que, de acordo com a abordagem intuicionista, poderia ocorrer que não teríamos um algoritmo capaz de decidir, em geral, 'se há um número natural que satisfaça uma propriedade P ou, caso contrário, seria possível demonstrar uma contradição lógica da hipótese de existência desse número'.

    W. Stegmüller (1977), pág. 514, assinala que: "Para o intuicionista, o conceito de prova ou demonstração substitui o conceito de verdade. Não se deve dar a esta palavra um sentido técnico especial, mas o amplo sentido que associamos a 'fundamentar'. Em cada situação concreta em que somos solicitados a fornecer uma prova (para uma dada assertiva), um particular conceito de prova está presente e, o que é mais importante, sempre dispomos de um método efetivo para decidir se uma pretensa prova de fato o é (embora não tenhamos qualquer processo para decidir se uma sentença é verdadeira ou não)." [Meus itálicos destacados em vermelho]. 

    Neste extrato, Stegmüller observa que o conceito de prova substitui, de acordo com a abordagem intuicionista, o conceito de verdade, haja vista que recorremos a procedimentos efetivos para verificar se há de fato uma sequência dedutiva para uma dada sentença (verdadeira) como consequência lógica de um argumento. 

    Do meu ponto de vista, o sistema de aritmética (recursiva) generalizada (abreviada aqui como AG) introduzido em Sarmento (2022) tem, em virtude de sua construção formal e do metateorema de completude para este sistema [veja Theorem 3.1.1 - completeness metatheorem em Sarmento (2022)], um caráter semântico deflacionário (i.e., "a função do predicado 'é verdadeiro' pode ser completamente explicada por meio do esquema T" - veja a entrada da Wikipédia abaixo). Pois, para qualquer sentença aritmética (ou a negação dessa sentença) expressável em AG há um procedimento efetivo de prova via esquema de indução de ordem superior (ou de ordem transfinita) que nos permite decidir se a dada sentença é demonstrável ou não em AG. Nesta acepção, pressupondo-se a consistência de AG, i.e., Consis(AG), temos um procedimento efetivo de decidibilidade, em um nível superior da hierarquia aritmética de AG, para a verdade de qualquer sentença aritmética (ou de sua negação) expressável em AG. Essa espécie de abordagem deflacionista é compatível, no meu entendimento, com a teoria minimalista advogada por P. Horwich. 

    Dessa perspectiva, ao contrário da versão formalista original de Hilbert, não se trata de defender, em nível metamatemático, uma abordagem estritamente finitária (ou construtivista estrito senso), haja vista que, após os resultados de Gödel (1931), métodos de caráter finitário não são suficientemente 'fortes' para uma prova de consistência da aritmética.

    Continuaremos essa discussão em uma próxima postagem.

Mais informações »