Logica matematica/Calcolo delle proposizioni/I tableaux semantici: differenze tra le versioni

Contenuto cancellato Contenuto aggiunto
m Correggo sintassi in formula matematica secondo mw:Extension:Math/Roadmap
Riga 18:
* α-formula: formula ''proposizionale congiuntiva'', la cui soddisfacibilità equivale alla soddisfacibilità di entrambe le sue componenti;
* β-formula: formula ''proposizionale disgiuntiva'', la cui soddisfacibilità equivale alla soddisfacibilità di almeno una tra le sue due componenti.
In altre parole, lo schema raggruppa in due categorie tutte le formule del calcolo proposizionale del tipo <math>(\neg A)</math> e <math>(A \circ B)</math>, con <math>\circ \in \{\orlor,\andland,\rightarrow,\leftrightarrow\}</math>: quelle che agiscono ''congiuntivamente'' e quelle che agiscono ''disgiuntivamente''.
 
=== Regole di espansione ===
Riga 32:
 
==== Congiunzione ====
<math>\frac{S,\mathrm{T}A\andland B}{S,\mathrm{T}A,\mathrm{T}B}\mathrm{T}\andland</math>
 
<math>\frac{S,\mathrm{F}A\andland B}{S,\mathrm{F}A|S,\mathrm{F}B}\mathrm{F}\andland</math>
 
==== Disgiunzione ====
<math>\frac{S,\mathrm{T}A\orlor B}{S,\mathrm{T}A|S,\mathrm{T}B}\mathrm{T}\orlor</math>
 
<math>\frac{S,\mathrm{F}A\orlor B}{S,\mathrm{F}A,\mathrm{F}B}\mathrm{F}\orlor</math>
 
==== Implicazione ====
Riga 149:
 
==== Dimostrazione ====
Il lemma si dimostra per induzione strutturale sulle regole di espansione. Consideriamo solo il caso della '''<math>\mathrm{T}</math>'''-regola della disgiunzione. Sia <math>\beta</math> una formula soddisfacibile della forma <math>\beta_1\orlor\beta_2</math>, allora <math>\mathcal{M_V} \models \beta</math>, per qualche modello <math>\mathcal{M_V}</math>, dunque <math>\mathcal{M_V} \models \beta_1</math> oppure <math>\mathcal{M_V} \models \beta_2</math>. Se <math>\mathcal{T_1}</math>è il tableau iniziale per <math>\mathrm{T}\beta</math>, e <math>\mathcal{T_2}</math> è il tableau ottenuto espandendo <math>\mathcal{T_1}</math> tramite l'applicazione della '''<math>\mathrm{T}</math>'''-regola della disgiunzione, <math>\mathcal{T_2}</math> è <math>\mathrm{T}\beta_1|\mathrm{T}\beta_2</math>, ovvero <math>\mathcal{M_V} \models \beta_1</math> oppure <math>\mathcal{M_V} \models \beta_2</math>; dunque <math>\beta</math> è soddisfacibile sse almeno <math>\beta_1</math> o <math>\beta_2</math> è soddisfacibile. Di conseguenza, almeno un ramo di <math>\mathcal{T_2}</math> dev'essere soddisfacibile, e quindi <math>\mathcal{T_1}</math> è soddisfacibile sse <math>\mathcal{T_2}</math> è soddisfacibile.
 
=== Teorema dei modelli ===
Riga 201:
 
=== Non contraddizione ===
<math>\underline{\mathrm{F}\neg(A\andland \neg A)}_{\mathrm{F}\neg} </math>
 
<math>\underline{\mathrm TA\andland \neg A}_{\mathrm T\andland} </math>
 
<math>\underline{\mathrm TA, \mathrm T\neg A}_{\mathrm T\neg} </math>
Riga 210:
 
=== Terzo escluso ===
<math>\underline{\mathrm FA\orlor\neg A}_{\mathrm F\orlor} </math>
 
<math>\underline{\mathrm FA, \mathrm F\neg A}_{\mathrm F\neg} </math>
Riga 226:
 
=== Modus ponens ===
<math>\underline{\mathrm F(A \to B) \andland A \to B}_{\mathrm F\to} </math>
 
<math>\underline{\mathrm T(A \to B) \andland A, \mathrm FB}_{\mathrm T\andland} </math>
 
<math>\underline{\mathrm TA \to B, \mathrm TA, \mathrm FB}_{\mathrm T\to} </math>
Riga 255:
 
=== Teorema di De Morgan ===
<math>\underline{\mathrm F \neg(A \andland B) \leftrightarrow (\neg A \orlor \neg B)}_{\mathrm F\leftrightarrow} </math>
 
<math>\underline{\mathrm T \neg(A \andland B), \mathrm F\neg A \orlor \neg B}_{\mathrm T\neg}|
\underline{\mathrm F \neg(A \andland B), \mathrm T\neg A \orlor \neg B}_{\mathrm F\neg}
</math>
 
<math>\underline{\mathrm FA \andland B, \mathrm F\neg A \orlor \neg B}_{\mathrm F\orlor}|
\underline{\mathrm TA \andland B, \mathrm T\neg A \orlor \neg B}_{\mathrm T\andland}
</math>
 
<math>\underline{\mathrm FA \andland B, \mathrm F\neg A, \mathrm F\neg B}_{\mathrm F\neg}|
\underline{\mathrm TA, \mathrm TB, \mathrm T\neg A \orlor \neg B}_{\mathrm T\orlor}
</math>
 
<math>\underline{\mathrm FA \andland B, \mathrm TA, \mathrm TB}_{\mathrm F\andland}|
\underline{\mathrm TA, \mathrm TB, \mathrm T\neg A}_{\mathrm T\neg}|
\underline{\mathrm TA, \mathrm TB, \mathrm T\neg B}_{\mathrm T\neg}
Riga 281:
 
=== Proprietà distributiva ===
<math>\underline{\mathrm F A\orlor(B \andland C) \leftrightarrow (A \orlor B) \andland (A \orlor C)}_{\mathrm F\leftrightarrow} </math>
 
<math>\underline{\mathrm T A\orlor(B \andland C), \mathrm F(A \orlor B) \andland (A \orlor C)}_{\mathrm T\orlor}|
\underline{\mathrm F A\orlor(B \andland C), \mathrm T(A \orlor B) \andland (A \orlor C)}_{\mathrm F\orlor} </math>
 
<math>\underline{\mathrm TA, \mathrm F(A \orlor B) \andland (A \orlor C)}_{\mathrm F\andland}|
\underline{\mathrm T B \andland C, \mathrm F(A \orlor B) \andland (A \orlor C)}_{\mathrm T\andland}|
\underline{\mathrm FA, \mathrm F B \andland C, \mathrm T(A \orlor B) \andland (A \orlor C)}_{\mathrm T\andland} </math>
 
<math>\underline{\mathrm TA, \mathrm F A \orlor B}_{\mathrm F\orlor}|
\underline{\mathrm TA, \mathrm F A \orlor C}_{\mathrm F\orlor}|
\underline{\mathrm TB, \mathrm TC, \mathrm F(A \orlor B) \andland (A \orlor C)}_{\mathrm F\andland}|
\underline{\mathrm FA, \mathrm F B \andland C, \mathrm T A \orlor B, \mathrm T A \orlor C}_{\mathrm T\orlor} </math>
 
<math>\overline{\mathrm TA}, \overline{\mathrm FA}, \mathrm FB|
\overline{\mathrm TA}, \overline{\mathrm FA}, \mathrm FC|
\mathrm TB, \mathrm TC, \mathrm F A \orlor B|
\mathrm TB, \mathrm TC, \mathrm F A \orlor C|
\overline{\mathrm FA}, \mathrm F B \andland C, \overline{\mathrm TA}, \mathrm T A \orlor C|
\mathrm FA, \mathrm F B \andland C, \mathrm TB, \mathrm T A \orlor C </math>
 
<math>
\underline{\mathrm TB, \mathrm TC, \mathrm F A \orlor B}_{\mathrm F\orlor}|
\underline{\mathrm TB, \mathrm TC, \mathrm F A \orlor C}_{\mathrm F\orlor}|
\underline{\mathrm FA, \mathrm F B \andland C, \mathrm TB, \mathrm T A \orlor C}_{\mathrm T\orlor} </math>
 
<math>
\overline{\mathrm TB}, \mathrm TC, \mathrm FA, \overline{\mathrm FB}|
\mathrm TB, \overline{\mathrm TC}, \mathrm FA, \overline{\mathrm FC}|
\overline{\mathrm FA}, \mathrm F B \andland C, \mathrm TB, \overline{\mathrm TA}|
\mathrm FA, \mathrm F B \andland C, \mathrm TB, \mathrm TC </math>
 
<math>
\underline{\mathrm FA, \mathrm F B \andland C, \mathrm TB, \mathrm TC}_{\mathrm F\andland} </math>
 
<math>