Formula ben formata

Nella logica matematica si chiama formula ben formata o - brevemente - fbf una stringa di simboli che rappresenti un'espressione sintatticamente corretta. Per un linguaggio del primo ordine ${\displaystyle L}$ o -una fbf si definisce induttivamente nel seguente modo:

Prima si definisce una formula atomica come una formula del tipo

${\displaystyle A(t_{1},...,t_{n})}$

dove ${\displaystyle A}$ è un simbolo per predicato n-ario e ${\displaystyle t_{1},...,t_{n}}$ sono termini.

poi si da la seguente definizione induttiva:

1) ogni formula atomica di ${\displaystyle L}$ è una fbf di ${\displaystyle L}$;

2) se ${\displaystyle {\mathcal {A}}}$ e ${\displaystyle {\mathcal {B}}}$ sono fbf allora lo sono anche ${\displaystyle \neg {\mathcal {A}}}$, ${\displaystyle {\mathcal {A}}\rightarrow {\mathcal {B}}}$, e ${\displaystyle \forall x{\mathcal {A}}}$;

3) tutte e sole le fbf sono definite dalle regole precedenti;

Esempi di formule ben formate nel linguaggio dell' aritmetica di Peano sono

${\displaystyle x+y=0}$

${\displaystyle \forall z(x+y=0)}$

${\displaystyle (x=x)\to \forall x(S(x)=S(y))}$

Non è invece una fbf

${\displaystyle (x=x)\to \forall x(S(x))}$

poiché S non è un simbolo per predicato bensì un simbolo per funzione.