W tej teorii można przeprowadzić dowody formalne poprawności programów, np. dowód poprawności algorytmu Euklidesa. Nb. podręcznikowe dowody poprawności algorytmu Euklidesa bazują na nieformalnym sformułowaniu aksjomatu Archimedesa, przedstawianym bez dowodu. Aksjomat Archimedesa jest twierdzeniem algorytmicznej teorii liczb naturalnych.
Język tej teorii zdeterminowany jest przez alfabet i zbiór wyrażeń poprawnie zbudowanych.
W alfabecie tej teorii wyróżnia się stałe 0 i 1, operatory „s” (następnik), „+” (dodawanie), „*” (mnożenie) i relację „=” równości.
Aksjomaty algorytmicznej teorii liczb naturalnych
ten aksjomat stwierdza, że każda element struktury jest osiągalny z zera przez dodawanie jedynki, tj. nie ma elementów niestandardowych.
Przykłady twierdzeń tej teorii to m.in. schemat indukcji:
niech oznacza dowolną formułę pierwszego rzędu ze zmienną wolną
tw. o poprawności algorytmu Euklidesa
Algorytmiczna teoria liczb wymiernych Antoni Kreczmar udowodnił [], że każde ciało spełniające własność stopu algorytmu Euklidesa jest izomorficzne z ciałem liczb naturalnych. Inaczej mówiąc algorytmiczne własności programów wykonywanych w ciele liczb wymiernych wynikają z następującej formuły: