Sistema assiomatico di Hilbert-Bernays
Il sistema assiomatico di Hilbert-Bernays è un sistema formale ideato per fornire una base rigorosa alla logica proposizionale e alla logica in generale.
Fu sviluppato da David Hilbert e Paul Bernays, due importanti matematici e logici, come parte del programma di Hilbert, che mirava a formalizzare la matematica interamente attraverso un insieme di assiomi e regole logiche.
Il sistema è progettato per essere minimale ed essenziale.
Permette di dedurre tutte le proposizioni logiche valide usando solo pochi assiomi (15 schemi), alcuni connettivi logici e una sola regola di inferenza: il modus ponens.
Gli elementi fondamentali del sistema
Un sistema assiomatico si compone di:
- Assiomi: Proposizioni fondamentali accettate come vere senza bisogno di dimostrazione.
- Regole di inferenza: Regole che permettono di derivare nuove proposizioni (o formule) a partire dagli assiomi o da altre proposizioni già derivate.
Nel caso specifico del sistema di Hilbert-Bernays l’unica regola di inferenza è il modus ponens.
Il modus ponens è una regola deduttiva $ \frac{A \to B \quad A}{B} $ che afferma se \( A \to B \) (se \( A \) implica \( B \)) è vero, e se \( A \) è vero, allora posso dedurre \( B \).
Gli assiomi nel sistema di Hilbert-Bernays non sono proposizioni specifiche, ma 15 schemi di assiomi, ossia formule generali valide per ogni scelta delle proposizioni \( A, B, C \).
- \( A \to (B \to A) \)
Una proposizione \( A \) implica sempre che, se \( B \) è vero, \( A \) rimane vero. - \( (A \to (A \to B)) \to (A \to B) \)
Se da \( A \) posso dedurre \( B \) in due passi, allora posso dedurlo direttamente. - \( (A \to B) \to ((B \to C) \to (A \to C)) \)
Esprime la transitività dell'implicazione. - \( A \land B \to A \)
Da una congiunzione (\( A \land B \)) posso dedurre \( A \). - \( A \land B \to B \)
Da una congiunzione (\( A \land B \)) posso dedurre \( B \). - \( (A \to B) \to ((A \to C) \to (A \to B \land C)) \)
Se \( A \) implica \( B \) e \( C \), allora \( A \) implica la loro congiunzione \( B \land C \). - \( A \to A \lor B \)
Una proposizione \( A \) implica la disgiunzione \( A \lor B \), indipendentemente da \( B \). - \( B \to A \lor B \)
Una proposizione \( B \) implica la disgiunzione \( A \lor B \), indipendentemente da \( A \). - \( (A \to B) \to ((C \to B) \to (A \lor C \to B)) \)
Se \( A \) o \( C \) implicano \( B \), allora la disgiunzione \( A \lor C \) implica \( B \). - \( (A \leftrightarrow B) \to (A \to B) \)
Se \( A \) e \( B \) sono equivalenti, allora \( A \) implica \( B \). - \( (A \leftrightarrow B) \to (B \to A) \)
Se \( A \) e \( B \) sono equivalenti, allora \( B \) implica \( A \). - \( (A \to B) \to ((B \to A) \to (A \leftrightarrow B)) \)
Se \( A \) implica \( B \) e \( B \) implica \( A \), allora \( A \) e \( B \) sono equivalenti. - \( (A \to B) \to (\neg B \to \neg A) \)
Se \( A \) implica \( B \), allora la negazione di \( B \) implica la negazione di \( A \). - \( A \to \neg \neg A \)
Una proposizione \( A \) implica la negazione della sua negazione (\( \neg \neg A \)). - \( \neg \neg A \to A \)
La doppia negazione di \( A \) implica \( A \) stesso.
Questi 15 schemi sono sufficienti, insieme alla regola del modus ponens, per dedurre tutte le proposizioni vere della logica proposizionale.
Inoltre, catturano le proprietà fondamentali dei connettivi logici (\( \neg, \land, \lor, \to, \leftrightarrow \)).
- \( \neg \): negazione ("non")
- \( \land \): congiunzione ("e")
- \( \lor \): disgiunzione ("o")
- \( \to \): implicazione ("se... allora")
- \( \leftrightarrow \): equivalenza ("se e solo se")
Tutti gli altri operatori o costrutti logici possono essere definiti usando questi cinque connettivi fondamentali.
Perché il sistema di Hilbert-Bernays è importante?
Il sistema di Hilbert-Bernays è significativo per diversi motivi.
In primo luogo, è progettato per essere il più semplice e minimale possibile. Utilizza pochi assiomi e una sola regola di inferenza.
Inoltre, soddisfa la completezza. Tutte le verità logiche della logica proposizionale possono essere derivate usando questo sistema.
Ha influenzato lo sviluppo di sistemi logici più complessi, come la logica dei predicati.
Nota. Per questa ragione faceva parte del programma di Hilbert, che cercava di formalizzare tutta la matematica su basi solide e verificabili.
Un esempio pratico
Voglio dimostrare che $ A \to A $ detto anche "principio di identità", che afferma che una proposizione implica sé stessa.
Come primo passo utilizzo il primo assioma del sistema: \( A \to (B \to A) \), con \( B = A \), ottengo $ A \to (A \to A) $
Poi uso il secondo assioma: \( (A \to (A \to B)) \to (A \to B) \), con \( B = A \) e deduco:
$$ A \to A $$
Questo dimostra che il sistema permette di derivare anche proprietà logiche fondamentali a partire dagli assiomi, usando il modus ponens.
E così via.
