Formule predikátové logiky

Formule predikátové logiky (predikátová formule, formule) je každá posloupnost symbolů z jazyka predikátové logiky, která vznikne aplikací následujících pravidel v konečně mnoha krocích:

1. Je-li -ární predikátový symbol a jsou termy, pak je formule. Takto vzniklou formuli nazýváme atomická formule.
2. Jsou-li formule, pak i jsou formule.
3. Je-li proměnná a formule, pak i jsou formule.