Teoria formale

Una teoria formale è un metodo per produrre asserzioni in forma matematica e per permettere l'induzione di formule derivate a partire da altre formule considerate primarie.

Descrizione informale

Da un certo punto di vista l'uso delle teorie formali per esprimere dei ragionamenti ha molti vantaggi rispetto alle descrizioni informali tipiche della lingua naturale in quanto non soffrono di problematiche quali ambiguità, incompletezza ed inconsistenza.

Da un altro punto di vista i sistemi basati esclusivamente sulle teorie formali sono carenti nel riuscire ad astrarre e creare conoscenza perché sono limitati agli assiomi con cui sono stati costruiti e alla conoscenza ricavabile da essi.

Descrizione formale

Una teoria formale è una 4-tupla ${\displaystyle \langle S,Fbf,A,R\rangle }$

• ${\displaystyle S}$ è un insieme finito di simboli. Una sequenza finita di simboli è chiamata espressione della teoria formale.
• ${\displaystyle Fbf}$ è il sottoinsieme delle formule ben formate delle espressioni della teoria formale.
• ${\displaystyle A}$ è un sottoinsieme delle formule ben formate della teoria formale ed è chiamato insieme degli assiomi.
• ${\displaystyle R}$ è un insieme finito di relazioni che riguardano le formule ben formate chiamate regole di inferenza.

Una formula ben formata ${\displaystyle X}$ è una conseguenza in un insieme di formule ben formate della teoria formale se e solo se, c'è una sequenza di formule ben formate, ${\displaystyle X_{1},X_{2},...X_{n}}$ tali che l'ultima equivale alla prima ed è ricavata applicando iterativamente una di queste regole:

• ${\displaystyle X_{a}}$ è un assioma,
• ${\displaystyle X_{a}}$ è ricavata dalla formula precedente attraverso una regole di inferenza,
• ${\displaystyle X_{a}}$ è una formula ben formata della teoria formale.

Voci correlate

• Informatica teorica
• Logica matematica

Portale Informatica

Portale Matematica