Formula ben formata

Nella logica matematica si chiama formula ben formata o - brevemente - fbf una stringa di simboli che, intuitivamente, rappresenti un'espressione sintatticamente corretta. Più esattamente, una formula ben formata di un sistema formale è una sequenza di simboli ottenuta mediante le regole fissate dalla grammatica del sistema formale stesso.

Nel caso particolare di un linguaggio del primo ordine ${\displaystyle L}$ o -la definizione induttiva di fbf è la seguente:

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 (per convenzione, non si scrivono le parentesi esterne)

${\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.