Formula ben formata: differenze tra le versioni

Versione delle 22:46, 2 lug 2007

Versione delle 13:35, 2 gen 2008

Riga 1:

{{S|matematica}}

Nella [[logica matematica]] si chiama '''formula ben formata''' o - brevemente - '''fbf''' di un [[sistema formale]] una stringa di simboli che, intuitivamente, rappresenti un'espressione sintatticamente corretta. Piùe esattamente,che viene definita mediante le regole della grammatica del sistema formale stesso.

una ''formula ben formata'' di un [[sistema formale]] è una sequenza di simboli ottenuta mediante le regole fissate dalla grammatica del sistema formale stesso.

Definizioni specifiche di '''formule ben formata''' vengono date nell'ambito della [[logica proposizionale]] e dei [[linguaggio del primo ordine|linguaggi del primo ordine]].

Nel caso particolare di un [[linguaggio del primo ordine]] <math>L</math> o -la definizione induttiva di '''fbf''' è la seguente:

Prima si definisce una '''formula atomica''' come una formula del tipo

:<math>A(t_1,...,t_n)</math>

dove <math>A</math> è un simbolo per predicato n-ario e <math>t_1,...,t_n</math> sono [[termini (logica)|termini]].

poi si da la seguente definizione induttiva:

<blockquote style="padding: 1em; border: 2px dotted purple;">

:1) ogni [[formula atomica]] di <math>L</math> è una ''fbf'' di <math>L</math>;

:2) se <math>\mathcal A</math> e <math>\mathcal B</math> sono ''fbf'' allora lo sono anche <math>(\neg \mathcal A)</math>, <math>(\mathcal A \rightarrow \mathcal B)</math>, e <math>(\forall x \mathcal A)</math>;

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

</blockquote>

Esempi di formule ben formate nel linguaggio dell' [[aritmetica di Peano]] sono (per convenzione, non si scrivono le parentesi esterne)

:<math>x+y=0</math>

:<math>\forall z (x+y=0)</math>

:<math>(x=x) \to (\forall x (S(x)=S(y)))</math>

Non è invece una fbf

:<math>(x=x) \to (\forall x (S(x)))</math>

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

[[en:Well-formed formula]]