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
[modifica | modifica wikitesto]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
[modifica | modifica wikitesto]Una teoria formale è una 4-tupla
- è un insieme finito di simboli. Una sequenza finita di simboli è chiamata espressione della teoria formale.
- è il sottoinsieme delle formule ben formate delle espressioni della teoria formale.
- è un sottoinsieme delle formule ben formate della teoria formale ed è chiamato insieme degli assiomi.
- è un insieme finito di relazioni che riguardano le formule ben formate chiamate regole di inferenza.
Una formula ben formata è una conseguenza in un insieme di formule ben formate della teoria formale se e solo se, c'è una sequenza di formule ben formate, tali che l'ultima equivale alla prima ed è ricavata applicando iterativamente una di queste regole:
- è un assioma,
- è ricavata dalla formula precedente attraverso una regole di inferenza,
- è una formula ben formata della teoria formale.
