Da Semântica para Demonstrações de Consistência e a Volta

Abstract

O presente artigo contém duas teses principais. Primeiro, que o ponto de partida em uma demonstração de consistência de um sistema formal é uma noção semântica. Essa tese é apresentada a partir de uma análise das etapas pelas quais uma demonstração de consistência passa, uma vez que um atributo de fórmulas com base em alguma interpretação deve ser estipulado já na etapa inicial. Para avançar cada uma das etapas, uma demonstração de consistência deve produzir um ganho de entendimento correspondente em relação ao sistema. Confirmamos a tese por um estudo de casos de três sistemas em que três demonstrações construtivas de consistência correspondentes são analisadas. O estudo é restrito a demonstrações construtivas pois no caso modelo-teórico a tese é evidente. Estudamos a lógica de primeira ordem, a aritmética sem indução, também conhecida como aritmética de Robinson, e a aritmética com indução ou de Peano. Em seguida, consideramos a relação entre consistência e verdade na aritmética sob o prisma do estudo de casos. A partir disso, podemos formular a segunda tese: há uma concepção da verdade aritmética que não se compromete de partida com a consistência. Tal tese é motivada tendo em vista as limitações para demonstrações de consistência apresentadas.