Logica pentru informatica

Pentru a construi multimea de formule a logicii cu predicate de ordinul I, LP1, avem nevoie de urmatoarele multimi de simboluri:  X = {x1,x2,...} : o multime cel mult numarabila de variabile functionale, sau, pe scurt, variabile.  P = {P1,P2,...} : o multime cel mult numarabila de simboluri predicative (sau predicate, sau relatii), cu aritati.

La randul sau, fiecare Pi este o multime de cel mult numarabila de predicate de aritate i (i t N). Elementele lui P0 se mai numesc ti variabile predicative.
F = {F1,F2,...} : o multime cel mult numarabila de simboluri functionale (sau functii), cu aritati, fiecare Fi fiind o multime de cel mult numarabila de functii de aritate i (i t N). Elementele lui F0 se mai numesc ti constante functionale.
C1 = {¬,t,t}: o multime de conectori logici (conective logice), la care se pot adauga, optional, ti alte simboluri cum ar fi ›, - etc.
C2 = {(tx)| x t X} t {(tx)| x t X}: o multime de cuantificatori (cuantori), universali, respectiv, existentiali. ((tx)se citette ”pentru fiecare x”, sau, ”pentru oricare(orice) x”, iar (tx) - ”exista x” ,”exista macar un x”, etc.).
Alfabetul total in LP1 reprezinta reuniunea multimilor precedente, impreuna cu parantezele rotunde ti virgula (pe scurt P):