W systemie zupełnym każde prawdziwe zdanie jest dowodliwe.
System formalny pierwszego rzędu – system, w którym użyto wyłącznie standardowych reguł wnioskowania oraz wszystkie jego aksjomaty są wyrażone w logice pierwszego rzędu, czyli nie dopuszcza się kwantyfikatorów po zmiennych przebiegających zbiory.
System formalny rozstrzygalny (efektywny) – taki system, którego algorytm wnioskowania da się zaprogramować na maszynie Turinga. Żeby system był rozstrzygalny, potrzeba i wystarcza, żeby istniała tylko jedna (ale odpowiednia) reguła wnioskowania (najczęściej przyjmuje się modus ponens) oraz żeby jego zbiór aksjomatów dał się wygenerować za pomocą maszyny Turinga.
Aksjomatyka Peana – pewien system formalny pierwszego rzędu, opisujący liczby naturalne.
Twierdzenia Pierwsze, o niezupełności Każdy niesprzeczny system formalny pierwszego rzędu, zawierający w sobie aksjomaty Peana, musi być niezupełny. Oznacza to, że żaden system formalny pierwszego rzędu nigdy nie „pokryje” w całości zbioru wszystkich twierdzeń arytmetyki. Nie oznacza to, że zbiór wszystkich twierdzeń arytmetyki nie istnieje, a jedynie, że nie może on być wygenerowany przez żaden system formalny.