Objeto formal

Em fundamentos da matemática, filosofia da matemática e filosofia da lógica,formalismo é uma teoria que sustenta afirmações matemáticas e lógicas e pode ser considerada como afirmações sobre as consequências de certas regras de manipulação de strings.

Por exemplo, a geometria euclidiana pode ser vista como um jogo onde suas jogadas consistem em mover-se ao redor de certas strings de símbolos chamadas axiomas de acordo com um conjunto de regras chamadas "regras de inferência" para gerar novas strings.

De acordo com o formalismo, as verdades expressadas na lógica e na matemática não são sobre números, conjuntos, ou triângulos ou qualquer outro assunto - de fato, elas não são "sobre" nada na verdade. Elas são formas sintáticas cujas formas e locais não têm significado se não receberem uma interpretação(ou semântica).

Formalismo é associado com métodos rigorosos. Normalmente, o formalismo significa a transformação do esforço para a formalização de uma dada área limitada. Em outras palavras, assuntos podem ser formalmente discutidos uma vez que capturados em um sistema formal, ou comumente suficiente dentro de algo "formalisável" com pretensão de ser um. Formalização completa está no domínio da ciência da computação.

Formalismo salienta provas axiomáticas usando teoremas, especificamente associados com David Hilbert. Um formalista é uma pessoa que pertence à escola de formalismo, que possui uma certa doutrina filosófica-matemática descendente de Hilbert.

Formalistas são relativamente tolerantes e convidativos para novas abordagens lógicas, para os sistemas não padrões de números, para novos conjuntos de teorias, etc. Quanto mais jogos estudamos, melhor. Porém, em todos os três exemplos, motivação é traçada a partir de preocupações matemáticas ou filosóficas existentes. Os "jogos" geralmente não são arbitrários.

Recentemente, alguns formalistas matemáticas propuseram que todo conhecimento matemático formal deve ser sistematicamente codificados em formatos legíveis para o computador, de modo a facilitar a checagem automática de provas matemáticas e do uso do teorema interativo provando no desenvolvimento de teorias matemáticas e programas de computador. Por causa de sua conexão com ciência da computação, essa ideia também é defendida por matemáticos intuicionistas e construtivistas na tradição "computabilidade".

Dedutivismo

Outra versão do formalismo é muitas vezes conhecido como dedutivismo. No dedutivismo, o teorema de Pitágoras não é uma verdade absoluta, mas relativa. Isso quer dizer, que se você interpreta as strings de tal forma que as regras do jogo se tornem verdade então você tem que aceitar o teorema, ou melhor, a interpretação do teorema de ter dado deve ser uma afirmação verdadeira,(As regras de um jogo teria que incluir, por exemplo, que as afirmações verdadeiras são atribuídas aos axiomas, e que as regras de inferência são a verdade de preservação, etc).

Sob dedutivismo, o mesmo ponto de vista é realizado para ser verdade para todos as outras afirmações da lógica formal e matemática. Assim, o formalismo não significa necessariamente que essas ciências dedutivas não são nada mais que jogos lógicos sem sentido. É normalmente esperado que exista alguma interpretação em que as regras do jogo se sustentem. Compare esta posição ao estruturalismo.

Considerando que os dedutivistas permitem ao matemático suspender o julgamento sobre as questões filosóficas profundas e proceder como se fundamentos epistemológicos sólidos estavam disponíveis. Muitos formalistas diriam que na prática, os sistemas axiomáticos a serem estudados são sugeridos pelas exigências da ciência particular.

Formalismo de Hilbert

Um grande defensor do formalismo era David Hilbert, cujo programa foi concebido para ser um completo e consistente axiomatização de toda a matemática. Hilbert procurou demonstrar a consistência dos sistemas matemáticos do pressuposto de que a "aritmética finitária"(um subsistema da habitual aritmética dos números inteiros positivos, escolhido para ser filosoficamente controversa) foi consistente(ou seja, não podem ser derivadas contradições do sistema).

A maneira que Hilbert tentou mostrar que um sistema axiomática era consistente foi formalizando usando uma linguagem particular(Snapper, 1979). A fim de formalizar um sistema axiomático, primeiro você deve escolher uma linguagem na qual você pode expressar e realizar operações dentro desse sistema. Esta linguagem deve incluir cinco componentes:

• Deve incluir variáveis como x, que podem representar alguns números.
• Deve ter quantificadores, tais como o símbolo de existência de um objeto.
• Deve incluir a igualdade.
• Deve incluir conectivos como ↔ para "se e somente se".
• Deve incluir certos termos indefinidos chamados parâmetros. Para geometria, esses termos indefinidos podem ser alguma coisa como um ponto ou uma reta para os quais nós ainda escolhemos símbolos.

Uma vez que escolhemos a linguagem, Hilbert pensou que pudéssemos provas todos os teoremas dentro de qualquer sistema axiomático usando nada mais do que os próprios axiomas e a linguagem formal escolhida.

A conclusão de Gödel em seu teorema da incompletude foi que você não pode provar consistência dentro de qualquer sistema axiomático rico o suficiente para incluir aritmética clássica. Por um lado, você deve usar somente a linguagem formal escolhida para formalizar este sistema axiomático; por outro lado, é impossível prova a consistência da linguagem em si (Snapper, 1979). Hilbert foi inicialmente frustrado pelo trabalho de Gödel porque ele quebrou o objetivo de sua vida para formalizar completamente tudo na teoria dos números (Reid e Weyl, 1970). Porém, Gödel não sentiu que ele contradisse tudo sobre o ponto de vista formalista de Hilbert. Depois que Gödel publicou seu trabalho, tornou-se evidente que a teoria da prova ainda tinha alguma utilidade, a única diferença é que ele não poderia ser usado para provar a consistência de toda a teoria dos números como Hilbert esperava (Reid and Weyl, 1970). Formalistas atuais usam a teoria da prova para profundar nossa compreensão na matemática, mas talvez por causa do trabalho de Gödel, eles não fazem nenhuma reivindicação sobre o significado semântico do trabalho que eles fazem com a matemática. As provas são simplesmente a manipulação de símbolos em nossa linguagem formal a partir de certas regras que chamamos de axiomas.

É importante notar que Hilbert não é considerado como um formalista rigoroso como formalista é definido hoje. Ele achava que havia algum significado e verdade na matemática, que é precisamente por isso que ele estava tentando provar a consistência da teoria dos números. Se a teoria dos números acabou por ser consistente, então tinha de haver algum tipo de verdade(Goodman, 1979). Formalistas rigorosos consideram a matemática para além de seu significado semântico. Eles veem a matemática como sintaxe pura: a manipulação de símbolos de acordo com certas regras. Eles, então, tentam mostrar que esse conjunto de regras é consistente, muito parecido com o que Hilbert tentou fazer(Goodman, 1979). Formalistas atualmente acreditam que os algoritmos computadorizados vão eventualmente assumir a tarefa de construir provas. Os computadores vão substituir os humanos em todas atividades matemáticas, como verificar se a prova é correta ou não(Goodman, 1979).

Hilbert foi inicialmente um dedutivista, mas, ele considerou certos métodos metamatemáticos para proporcionar resultados significativos e intrínsecos e foi realista com respeito à aritmética finitária. Mais tarde, ele realizou a opinião de que não há outros significados matemáticos, independente da interpretação.

Sistemas axiomáticos

Outros formalistas, como Rudolf Carnap, Alfred Tarski e Haskell Curry, considerados matemáticos para investigar sistemas axiomáticos formais. Lógicos matemáticos estudam sistemas formais mas são tão realistas como formalistas.

Principia Mathematica

Talvez a mais sérias tentativa de formalizar a teoria dos números foi feita por dois matemáticos Bertrand Russell e Alfred North Whitehead. Eles criaram uma obra, Principia Mathematica, que derivou a teoria dos números por manipulação de símbolos usando a lógica formal. Esta obra foi muito detalhada, e eles passaram a maior parte de uma década escrevendo-a. Até a página 379 do primeiro volume que não foram capaz de provar que 1 + 1 = 2.

Criticismo do formalismo

Gödel indicou um dos pontos fracos do formalismo ao abordar a questão da consistência em sistemas axiomáticos. Críticas mais recentes encontram-se na afirmação de formalistas que é possível informatizar toda a matemática. Estas críticas trazem à tona a questão filosófica da existência ou não de computadores que são capazes de pensar. Testes de Turing, em homenagem a Alan Turing, que criou o teste, são uma tentativa de fornecer critérios para julgar quando um computador é capaz de pensar. A existência de um computador que em princípio poderia passar por um teste de Turing provaria para os formalistas que computadores serão capazes de fazer toda a matemática. No entanto, existem os adversários desta reivindicação, como John Searle, que surgiu com o "quarto chinês" um experimento pensado. Ele apresentou o argumento que enquanto um computador pode ser capaz de manipular os símbolos que nós fornecemos, a máquina não atribui significados para esses símbolos.

Além disso, humanos podem criar várias maneias de provar o mesmo resultado, mesmo se eles podem achar que é um desafio de articular tais métodos. Uma vez que a criatividade requer pensamento ter uma base semântica, um computador não seria capaz de criar diferentes métodos de resolver o mesmo problema. De fato, um formalista não seria capa de dizer que essas outras formas de resolver os problemas existem simplesmente porque não foram formalizados(Goodman, 1979).

Outra crítica do formalismo é que as ideias matemáticas reais que ocupam os matemáticos estão longe dos jogos de manipulação de strings acima mencionados. Formalismo é o silêncio para a questão de quais sistemas axiomáticos devem ser estudados, já que nenhum é mais significativo do que o outro de um ponto de vista formal.

Referências

• Goodman, Nicholas D. "Mathematics as an Objective Science." The American Mathematical Monthly 86.7 (1979): 540-551. Print.
• Penrose, Roger. The Emperor's New Mind: concerning Computers, Minds, and the Laws of Physics. Oxford: Oxford UP, 1989. Print.
• Reid, Constance, and Hermann Weyl. Hilbert. Berlin: Springer-Verlag, 1970. Print.
• Snapper, Ernst. "The Three Crises in Mathematics: Logicism, Intuitionism and Formalism." Mathematics Magazine 52.4 (1979): 207-16. Print.
• Weir, Alan: "Formalism in the Philosophy of Mathematics." Stanford Encyclopedia of Philosophy (2011).