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.
AFE é um sistema em lógica de primeira ordem (com igualdade). Sua linguagem contém: 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.
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) é: 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.
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.
