formalióji aritmètika, formalioji sistema, nustatanti natūraliųjų skaičių pagrindines savybes. 1891 G. Peano suformulavo penkias aritmetikos aksiomas: nulis yra natūralusis skaičius; koks bebūtų natūralusis x, egzistuoja paskesnis narys s(x); koks bebūtų natūralusis x, nulis nėra lygus s(x); jei s(x) = s(y), tai x = y. Matematinės indukcijos principas yra penktoji aksioma. 1901 R. J. W. Dedekindas formalizavo G. Peano aksiomas ir sudarė aritmetikos aksiomų sistemą. 1930 Edmundas Georgas Hermannas Landau (Vokietija) įrodė, kad šių aksiomų su tam tikra aibių teorijos dalimi visiškai pakanka natūraliųjų, racionaliųjų ir kompleksinių skaičių savybėms nustatyti. Formaliosios aritmetikos abėcėlė susideda iš loginių operacijų (neigimas, konjunkcija, disjunkcija, implikacija), kvantorių, funkcinių simbolių (sudėtis, daugyba, paskesnis narys), individinės konstantos (nulis), individinių kintamųjų ir pagalbinių simbolių (skliaustų). Formaliosios aritmetikos aksiomų sistema susideda iš 2 dalių: loginių aksiomų ir išvedimo taisyklių (klasikinės logikos predikatų skaičiavimas); aritmetikos aksiomų: 1. (x = y) → (s(x) = s(y)); 2. (x = y) → → ((x = z) → (y = z)); 3. ¬ (s(x) = 0); 4. (s(x) = s(y)) → (x = y); 5. (x + 0) = x; 6. (x + s(y)) = s(x + y); 7. (x·0) = 0; 8. (x·s(y)) = ((x·y) + x); 9. (R(0) & ∀ x(R(x) → R(s(x)))) → ∀ x R(x); čia x, y, z – individiniai kintamieji, R(x) – kuri nors formulė aritmetikos abėcėlėje. Paskutinė aksioma vadinama indukcijos aksioma. Remiantis formaliosios aritmetikos aksiomomis galima gauti visus pagrindinius aritmetikos rezultatus. 1931 K. Gödelis įrodė, kad formalioji aritmetika nėra tobula (pilnoji), t. y., egzistuoja aritmetinių teiginių, išreiškiamų formaliosios aritmetikos formulėmis, kurių negalima įrodyti ar paneigti remiantis formaliosios aritmetikos aksiomomis.
35