Cette section donne une brève présentation de la grammaire du calcul des prédicats dans un langage formel couramment utilisé en logique classique par la plupart des mathématiciens.

Cette grammaire peut donc être formalisée et utilisée dans tout programme d'ordinateur pour décider si une proposition (assertion) est bien formée.

On considère donc, comme données primitives du langage:
(*) Les mots 'prédicat' et 'fonction' ont ici les sens définis dans les sections précédentes.
On appellera termes les formules composées ainsi :
Un terme est 'clos' s'il ne contient pas de nom de variable.

Les termes ont pour but de représenter les objets sur lesquels vont s'appliquer des prédicats.

Les énoncés ou formules du 'calcul des prédicats du premier ordre' sont les suivants, et uniquement les suivants  :

Exemple: On veut exprimer formellement que le sinus d'un nombre réel est toujours compris entre -1 et 1, ce qui donnera:
∀ x  ((x∈ℝ) ⇒((EstInf(-1,sin(x))∧( EstInf(sin(x),1))))
avec les conventions d'écriture définissant le prédicat EstInf(x,y) ssi x ≤ y et x∈ℝ pouvant être écrit sous forme prédicative EstElementDe(x,ℝ).
Il va de soi qu'EN PRATIQUE on écrira:
∀x ∈ ℝ -1 ≤ sin(x) ≤ 1
Il s'agit simplement de montrer qu'en théorie tout énoncé peut prendre la forme standard décrite plus haut.