Il contesto tarskis_world.cnt ha la seguente segnatura primitiva:
I simboli primitivi riguardano forma, dimensione, posizione e nomi dei blocchi.
Vi è una corrispondenza precisa fra le
interpretazioni del primo ordine dei simboli primitivi e le operazioni
possibili con l'interfaccia grafica del tool TW (acronimo di "Tarski's World" del
libro di testo): per depositare un blocco sulla griglia lo si aggiunge all'universo; per
spostarlo in una data posizione si danno riga e colonna; per dargli
una forma F (F=Cube, Tet, Dodec) lo si aggiunge alla interpretazione di F; per dargli una
dimensione D (D=Small, Large, Medium) lo si aggiunge all'interpretazione di D. Ad esempio,
il mondo della seguente figura:
Gli assiomi che riguardano la segnatura primitiva sono:
Gli altri assiomi del contesto tarskis_world.cnt sono definizioni esplicite che
estendono la segnatura primitiva con i predicati non primitivi usati in TW:
Ogni interpretazione dei simboli primitivi che rappresenti un mondo disegnabile con il tool TW è modello degli assiomi e ogni modello degli assiomi rappresenta un mondo di TW, visualizzabile con Disegna mondo Tarski.
Per costruire un mondo di blocchi basta fornire l'interpretazione dei simboli primitivi. Se l'interpretazione è un modello, usando gli assiomi di definizione esplicita il sistema è in grado di ricavare in automatico l'interpretazione estesa a tutti i simboli definiti (quelli indicati con def in Fig.tw.6).
L'interpretazione estesa viene mostrata sul foglio *out.logi tutte le volte che
si chiede al sistema di valutare in una interpretazione primitiva
una formula o un foglio di formule collegato ad un contesto. In particolare
viene mostrata quando si verifica se una interpretazione primitiva è un modello del contesto,
usando Verifica modelli del menù Attività.
Ad esempio, per verificare che l'interpretazione i1.intp di Fig.tw.3 è modello
di tarskis_world.cnt si usa Verifica modelli
con foglio attivo tarskis_world.cnt. Si ottiene che l'interpretazione
primitiva i1.intp è un modello:
>>
>ok>