Logica matematica/Calcolo delle proposizioni/Sistema di Hilbert: differenze tra le versioni

Contenuto cancellato Contenuto aggiunto
m Correggo sintassi in formula matematica secondo mw:Extension:Math/Roadmap
 
Riga 110:
Come accennato in precedenza, altri connettivi possono essere introdotti mediante definizioni, ad esempio:
 
# <math>A \andland B =_{Def} \neg(A \to \neg B)</math>;
# <math>A \orlor B =_{Def} \neg A \to B</math>;
# <math>A \leftrightarrow B =_{Def} (A \to B) \andland (B \to A)</math>.
 
Osserviamo che, in questo contesto, abbiamo dato delle definizioni per i connettivi perché non possiamo utilizzare la nozione di [[Logica/Calcolo delle proposizioni#Completezza di insiemi di connettivi|completezza di insiemi di connettivi]], che si basa sulla nozione di valutazione booleana. Qui, infatti, stiamo solo considerando un "calcolo", che è una nozione puramente sintattica, dunque non siamo autorizzati a utilizzare nozioni semantiche, quali l'equivalenza logica. Non possiamo usare nozioni semantiche fintantoché non dimostreremo un teorema che ci dice che "possiamo utilizzare le tautologie come teoremi", ovvero il teorema di completezza.
Riga 133:
Il teorema di deduzione ci dice che una formula può passare da sinistra a destra della relazione <math>\vdash</math> introducendo il connettivo <math>\to</math>, oppure da destra a sinistra eliminandolo. Questo risultato è importante per due ragioni. In primo luogo, perché ci fornisce la possibilità di esprimere una relazione metalinguistica (quale <math>\vdash</math>) mediante una formula del linguaggio.
 
In secondo luogo, esso ci fornisce la possibilità di trattare generiche derivazioni da insiemi di formule come teoremi. Infatti, in virtù della proprietà di compattezza di <math>\vdash</math>, abbiamo che, se <math>\Gamma \vdash A</math>, allora esiste un insieme finito <math>\Gamma_0 \subseteq \Gamma</math> tale che <math>\Gamma_0 \vdash A</math>. Siccome <math>\Gamma_0</math> è finito, sarà del tipo <math>\{A_1,...,A_n\}</math>, o equivalentemente <math>\{A_1 \andland ... \andland A_n\}</math>, quindi <math>\Gamma \vdash A</math> implica <math>\Gamma_0 \vdash A</math>, che equivale a <math>A_1 \andland ... \andland A_n \vdash A</math> e <math>A_1,...,A_n \vdash A</math>. Per il teorema di deduzione, otteniamo <math>\vdash (A_1 \andland ... \andland A_n) \to A</math> e <math>\vdash A_1 \to(... \to (A_n \to A)...)</math>.
 
== Consistenza ==
Riga 184:
:<math>\Gamma \vdash A</math> sse <math>\Gamma \vDash A</math>.
 
La proprietà al punto i è detta ''correttezza e completezza debole'', mentre quella al punto ii è detta ''correttezza e completezza forte''. In effetti, per le logiche in cui, come nel nostro caso, vale un teorema di compattezza e di deduzione, i due enunciati sono equivalenti: <math>\Gamma \vdash B</math> può essere scritto come <math>\vdash (A_1 \andland ... \andland A_n) \to B</math>, dove <math>(A_1 \andland ... \andland A_n)</math> è la congiunzione delle formule di <math>\Gamma</math>.
 
Dire che l'insieme dei teoremi è parte dell'insieme delle tautologie assicura che l'apparato deduttivo è corretto, non può infatti dimostrare formule non valide o contraddittorie. Dire che l'insieme delle tautologie è parte dell'insieme dei teoremi assicura che l'apparato deduttivo è completo, cioè che tutte le formule valide sono dimostrabili.