Os teoremas de Herbrand e Parsons revisitados

Em 1930, Jacques Herbrand deu uma caracterização das validades de primeira ordem em termos de tautologias apropriadas. Enunciaremos e daremos um esboço de demonstração (via teoria dos modelos) deste teorema para um caso particular. Com base neste teorema, damos uma nova demonstração do teorema de Charles Parsons de 1970/72 que caracteriza as funções demonstravelmente totais da aritmética de Peano com indução restrita a predicados r.e.. Este resultado de Parsons pode ser visto como uma realização "parcial" do programa de Hilbert. Falaremos brevemente sobre esta temática.