Il calcolo $ℱ_T$

• Il calcolo logico $ℱ_T$ consiste nelle argomentazioni provabili in Fitch usando tutte e sole le regole di introduzione ed eliminazione dei connettivi.

• Una argomentazione è provabile in Fitch se e solo se è validata da TAUT CON

• Notazione:

  $$ P_1,...P_n \vdash_T Q $$

  • Questa notazione indica che esiste una prova in $ℱ_T$ con premesse $P_1, P_2 ... P_n$ e conseguenza $Q$. Ricordare che:

    $$ \models_T indica\ conseguenza\ tautologica $$

Teorema di validità (soundness)

$$ Se\ P_1,...P_n \vdash_T Q,\ allora\ P_1,...P_n\models_TQ $$

• Se abbiamo dato una prova in ℱ di Q a partire da P1, ... Pn, è certo che Q è conseguenza tautologica di P1, ... Pn
• Contrapposta: se sappiamo che Q non è conseguenza tautologica delle premesse P1, ... Pn (esempio: controesempio sulle tavole di verità), allora siamo certi che non ci può essere una prova in $ℱ_T$ di Q a partire da P1, ... Pn

Teorema di completezza (completness)

$$ Se\ P_1,...P_n\models_TQ,\ allora\ P_1,...P_n\vdash_T Q $$

• Se sappiamo che Q è conseguenza tautologica delle premesse $P_1, ... P_n$ (ad esempui facendo vedere con le tavole di verità che non ci sono controesempi), siamo certi che esista una prova in $ℱ_T$ di Q a partire da $P_1, ... P_n$
• Contrapposta: se facciamo vedere che non c'e una dimostrazione in $ℱ_T$ di Q a partire da $P_1, .. P_n$, allora è certo che Q non è conseguenza tautologica di $P_1,...P_n$.

Teorema di validità e completezza in forma generale

• Un insieme 𝛤, eventualmente infinito, di enunciati è detto teoria.
• Il teorema di validità e completezza vale anche per teorie infinite

$$ \Gamma \vdash_T Q\ se\ e\ solo\ se\ \Gamma\models_TQ $$