Wstęp do formalizacji Logika pierwszego rzędu jest podstawą, na której formalizujemy większość matematyki. We wstępie do wspomnianej powyżej książki Goldsterna i Judaha traktującej właśnie o tej tematyce, Saharon Szelach napisał: [Na gruncie matematyki] możemy zdefiniować czym jest dowód i wykazać, że w pewnym sensie „być prawdziwym” i „mieć dowód” znaczą to samo (twierdzenie Gödla o pełności). (…) Nie możemy wyciągnąć sami siebie z bagna za włosy: nie możemy udowodnić w naszym systemie, że nie ma w nim sprzeczności (twierdzenie Gödla o niezupełności) (…) Możemy zbudować ogólną teorię teorii matematycznych (teoria modeli).
System rachunku predykatów pierwszego rzędu składa się z: zmiennych nazwowych (litery, za które wolno podstawić nazwy dowolnych przedmiotów), stałych nazwowych (nazwy własne przedmiotów), liter predykatowych (predykaty), symboli funkcyjnych (funktory nazwotwórcze od argumentów nazwowych), stałych logicznych (spójniki prawdziwościowe rachunku zdań i kwantyfikatory), znaków pomocniczych (nawiasy), symbolu równości.