Przykłady Język teorii mnogości to gdzie jest binarnym symbolem relacyjnym. Język teorii grup to gdzie jest binarnym symbolem funkcyjnym. Język ciał uporządkowanych to gdzie są binarnymi symbolami funkcyjnymi a jest binarnym symbolem relacyjnym.
Dowody w językach pierwszego rzędu Ustalmy alfabet (tak więc jest to zbiór złożony ze stałych, symboli funkcyjnych i symboli relacyjnych).
Podstawienia termów za zmienne Przypuśćmy, że i są termami języka oraz jest jedną ze zmiennych. Definiujemy podstawienie jako term, który powstaje z poprzez literalne zastąpienie w nim wszystkich egzemplarzy zmiennej termem
W przypadku zmiennej termu i formuły podstawienie definiuje się bardziej subtelnie, co najlepiej ująć indukcyjnie względem budowy formuły (por. ): jeśli jest formułą atomową to jeśli to gdzie jeśli to
oraz jeśli gdzie to jeśli oraz w przeciwnym wypadku.
Aby móc wysłowić niektóre z aksjomatów Rachunku Predykatów konieczne jest pewne ograniczenie operacji podstawiania w formule. Mianowicie, powiadamy, że podstawienie termu w formule za zmienną jest dopuszczalne lub, że zmienna jest wolna dla termu w formule , ozn.