• usa le conoscenze del contesto TW
• In Fitch ANA CON ci permette di inferire un enunciato che segue dagli enunciati selezionati in virtù della semantica dei connettivi vero-funzionali, dei quantificatori, del predicato d'identità e dei predicati di TW

$$ Sia\ C_1, ... C_n\ \models_{TW}\ D\ una\ conseguenza\ logica\ nel\ mondo\\dei\ blocchi. \\.\\ Se\ fra\ le\ premesse\ o\ le\ conseguenze\ intermedie\ di\ una\\ prova\ abbiamo\ C_1,...C_n\ ,\ allora\ nella\ prova\ possiamo\ inferire\ D. $$

<aside> 🔥 La regola D inferita dev'essere valida nel contesto TW.

</aside>