• Aggiungendo altri enunciati analoghi, detti postulati o assiomi, possiamo assiomatizzare le proprietà particolari che esistono nei mondi dei blocchi (TW), ma non necessariamente in altre strutture.

<aside> 💡 Assiomatizzare un insieme di circonstanza: Fornire una teoria 𝛤 (insieme di enunciati) tale che tutti i modelli di 𝛤 (tutte le L-strutture che rendono veri tutti gli enunciati della teoria) siano tutte e le sole L-strutture che descrivono, astrattamente, l'insieme desiderato di circonstanze.

</aside>

Il sistema assiomatico TW(SH)

• Definiamo una teoria SH che assiomatizza i predicati di TW che riguardano la forma dei blocchi (SHape).
• Predicati del Linguaggio L(SH): P(L(SH)) = {Tet/1, Cube/1, Dodec/1, SameShape/2}

Assiomi di TW(SH)

• Nessun blocco ha due forme

$$ SH1.\neg\exist x (Cube(x)\wedge Tet(x)) \\ SH2.\neg\exist x (Cube(x)\wedge Dodec(x)) \\ SH3. \neg\exist x (Tet(x)\wedge Dodec(x)) $$

• Ci sono solo tetraedri, dodecaedri e cubi

$$ SH4.\forall x (Cube(x)\vee Dodec(x)\vee Tet(x)) $$

• SameShape Intro

$$ SH5.\forall x\forall y((Cube(x)\wedge Cube(y))\rightarrow SameShape(x,y)) \\ SH6\ e\ SH7 \ per\ Dodec\ e\ Tet $$

• SameShape Elim

$$ SH8.\forall x\forall y((SameShape(x,y)\wedge Cube(x))\rightarrow Cube(y)) \\ SH9\ e\ SH10\ per\ Dodec\ e\ Tet $$

• Una dimostrazione in TW(SH) è una dimostrazione in FOL che, oltre alle premesse, usa anche gli assiomi di TW(SH)

$$ Def:\ P_1,...,P_n\vdash_{TW(SH)} Q\ se\ e\ solo\ se\ SH_1,...,SH_{10}, P_1,...,P_n\vdash_{FO}Q $$

<aside> 💡 Teorema: (da non confondere con teoria) enunciato provato senza premesse

</aside>