Aritmética de função elementar

Em teoria da prova, que é um ramo da lógica matemática, aritmética de função elementar, também chamada de AFE (EFA), aritmética elementar ou aritmética de função exponencial, é o sistema da aritmética com propriedades elementares habituais de 0, 1, +, ×, xy, em conjunto com a indução para fórmulas com quantificadores limitados.

A AFE é um sistema lógico muito fraco, cujo ordinal da prova teórica é ω3, mas ainda parece ser capaz de provar muito da matemática ordinária que pode ser expressa em linguagem aritmética de primeira-ordem.

Definição

AFE é um sistema em lógica de primeira ordem (com igualdade). Sua linguagem contém:

  • duas constantes 0, 1,
  • três operações binárias +, ×, exp, com exp(x,y) normalmente escrita como xy,
  • um símbolo de relação binária < (Isto não é realmente necessário já que ele pode ser escrito em termo das outras operações e é algumas vezes omitido, mas é conveniente para se definir quantificadores limitados).

Quantificadores limitados são aqueles na forma ∀(x<y) e ∃(x<y) que são abreviações para ∀x(x<y)→,,, e ∃x(x<y)∧... na maneira usual.

Os axiomas de AFE são

  • Os axiomas da Aritmética de Robinson para 0, 1, +, ×, <
  • Os axiomas para exponenciação: x0 = 1, xy+1 = xy×x.
  • Indução para fórmulas cujos quantificadores são limitados (mas que podem conter variáveis livres).

Grande conjectura de Friedman

A grande conjectura de Harvey Friedman implica que muitos teoremas matemáticos, tal como o Último teorema de Fermat, podem ser provados em sistemas muito fracos como o AFE.

A declaração original da conjectura de Friedman (1999) é:

"Todo teorema publicado nos Anais da Matemática cuja declaração envolve somente objetos matemáticos finitos (por exemplo, o que lógicos chamam de enunciado aritmético) pode ser provado em AFE. AFE é o fragmento fraco da Aritmética de Peano baseado nos usuais axiomas sem quantificadores para 0, 1, +, ×, exp, junto com o esquema de indução para todas as fórmulas na linguagem cujos quantificadores são limitados."

Enquanto é fácil construir enunciados aritméticos artificiais que são verdadeiros mas não têm prova em AFE, o objetivo da conjectura de Friedman é que exemplos naturais de tais enunciados na matemática parecem ser raros. Alguns exemplos naturais incluem enunciados de consistência provenientes da lógica, vários enunciados relacionados à Teoria de Ramsey tais como o lema da regularidade de Szemerédi e o teorema menor dos grafos, e o algoritmo de Tarjan para uma estrutura de dados de subconjuntos-disjuntos.

Sistemas relacionados

Pode-se omitir o símbolo exp de função binária da linguagem ao se tomar a artimética de Robinson junto com a indução de todas as fórmulas com quantificadores limitados e um axioma enunciando, grosso modo, que exponenciação é uma função definida em todos os lugares. Isto é similar ao AFE e tem a mesma força prova-teórica mas é mais complicado de se trabalhar.

Existem fragmentos fracos da aritmética de segunda ordem chamados RCA* 0 e WKL* 0 que têm a mesma força de consistência da AFE e são conservadores sobre ela por Π0 2 sentenças, o que é às vezes estudado em matemática reversa (Simpson 2009).

Aritmética recursiva elementar (ARE/ERA) é um subsistema da aritmética recursiva primitiva (ARP/PRA) onde a recursão é restrita a somas e produtos limitados. Isto também tem as mesmas Π0 2 sentenças que AFE, no sentido de que sempre que AFE prova ∀x∃y P(x,y), com P sendo livre de quantificadores, ARE prova a fórmula aberta P(x,T(x)), com T um termo definível em ARE.

Assim como PRA, ARE pode ser definida de maneira completamente livre de lógica, somente com as regras de substituição e de indução, e definindo equações para todas as funções recursivas elementares. No entanto, diferente de PRA, as funções recursivas elementares podem ser caracterizadas pelo fecho sob composição e projeção de um número finito de funções básicas, sendo assim, somente um número finito de equações definidoras é necessário.

Veja também

Referências