Teoria pierwszego rzędu (lub system dedukcyjny) – zbiór formuł zdaniowych T danego języka pierwszego rzędu, spełniający następujący warunek:
gdzie CnL(T) to zbiór wszystkich konsekwencji logicznych zbioru formuł zdaniowych T.