sistema formale

sistema formale

Sistema costituito da un linguaggio formale e un apparato deduttivo. Un esempio di s. f. è quello K per la logica proposizionale classica dato dalla coppia (L_K; D_K) dove L_K è il linguaggio simbolico del sistema, e D_K l’apparato per la costruzione delle inferenze nel sistema. Il linguaggio formale è costituito dall’alfabeto e dall’insieme delle formule del sistema. L’alfabeto di K è costituito (1) dalle lettere proposizionali (P₀,…,P_n); (2) dai connettivi logici ¬ e → (si noti che è possibile definire i connettivi ∧, ∨, ↔ a partire da ¬ e →); e dai simboli ausiliari:, ) e (. Combinando un numero finito di elementi dell’alfabeto si ottengono le cosiddette espressioni del sistema; tra queste vi sono alcune combinazioni sintatticamente ben formate dette formule ben formate, il cui insieme può essere definito ricorsivamente ponendo (1) la base dell’induzione: che ogni lettera proposizionale è una formula ben formata (formula atomica); (2) i passi dell’induzione: che se α è una formula ben formata, allora ¬α è una formula ben formata, e che se α e β sono due formule ben formate, allora (α→β) è ancora una formula ben formata; (3) la chiusura: che una espressione è una formula ben formata solo se lo è in base alle clausole (1) e (2) (dove α, β, γ sono metavariabili che variano sulle formule ben formate di K). L’apparato deduttivo è costituito dall’insieme degli assiomi e delle regole logiche del sistema. L’insieme di assiomi per il s. f. K considerato è costituito da tutte le esemplificazioni dei seguenti tre schemi di assioma: α→(β→α); (α→(β→γ))→((α→β)→(α→γ)); (¬β→¬α)→((¬β→α)→β). Come regola logica di deduzione per il sistema K considerato viene generalmente posta la regola del modus ponens, la quale asserisce che ‘da α e da α→β, segue β’. Posto un linguaggio formale e un apparato deduttivo è possibile definire il concetto di dimostrazione e di derivazione da ipotesi nel sistema. È possibile, inoltre, definire una semantica formale per il sistema interpretando (costruendo un modello) il suo linguaggio in una struttura e dando una definizione di soddisfacimento, verità, validità e conseguenza logica per le sue formule. Ovviamente è possibile costruire diversi s. f. per la logica proposizionale (considerando, per es., una s. f. con cinque connettivi: ¬, ∧, ∨, →, ↔); così come è possibile costruire s. f. per la logica del primo ordine, per quella del secondo ordine e così via, sia classiche sia non classiche, così come s. f. per specifiche teorie matematiche come quella dei numeri naturali, o dei numeri reali, o per la geometria elementare e altro ancora, ottenendo così le rispettive teorie formali. Costruito un s. f. è possibile studiare il suo linguaggio e il suo universo del discorso nell’ambito di una nuova teoria detta metateoria, dimostrando teoremi riguardanti la sintassi e la semantica della teoria oggetto. Proprietà metamatematiche molto importanti da dimostrare per i s. f. sono, per es., la correttezza, la completezza, la coerenza e la decidibilità.