Segnatura primitiva di tarskis_world

Il contesto tarskis_world.cnt ha la seguente segnatura primitiva:

La segnatura primitiva
Fig.tw.1 La segnatura primitiva di tarskis_world.cnt
Con la sorta integer viene automaticamente importata la struttura degli interi e degli intervalli di interi. Qui ci serve per avere l'intervallo 1..8 degli indici della scacchiera, che è il tipo delle funzioni row e col.

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:

Un mondo di TW Un mondo di TW
Fig.tw.2 Un mondo di TW in 3D e in 2D
si rappresenta con l'interpretazione riportata nella parte sinistra della Fig.tw.3; il nomi interno u0 indica il cubo grande, u1 il cubo piccolo e u2 il tetraedro; la scacchiera riportata a destra si ottiene dalla interpretazione con Disegna mondo Tarski.
Interpretazione Disegno
Fig.tw.3 Interpretazione i1.intp che rappresenta il mondo in Fig.tw.2 e suo disegno

Assiomi di tarskis_world.cnt

Gli assiomi che riguardano la segnatura primitiva sono:

assiomi segnatura primitiva
Fig.tw.4 - Assiomi relativi alla segnatura primitiva di tarskis_world.cnt
ogni assioma o gruppo di assiomi è seguito da un commento che ne spiega il significato.

Gli altri assiomi del contesto tarskis_world.cnt sono definizioni esplicite che estendono la segnatura primitiva con i predicati non primitivi usati in TW:

Def esplicite 1 Def esplicite 2
Fig.tw.5 - Definizioni eplicite di tarskis_world.cnt
La segnatura estesa è quella mostrata in *out.logi quando si Verifica e salva il foglio tarskis_world.cnt. La segnatura estesa è riportata qui sotto:
Segnatura estesa
Fig.tw.6 - La segnatura estesa di tarskis_world.cnt
La segnatura si dice "estesa" perché aggiunge ai simboli primitivi (quelli non indicati con def e appartenenti alla segnatura primitiva i simboli esplicitamente definiti dagli assiomi, quelli indicati con def.

Modelli e interpretazione estesa

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:

Verifica modelli >> scelta intp >ok> Risultato
Fig.tw.7 Verifica modelli: modello i1.intp di tarskis_world.cnt
La corrispondente interpretazione estesa è mostrata in *out.logi:
Un mondo di TW
Fig.tw.8.a intrepretazione estesa di i1.intp
Si osservi che l'interpretazione estesa interpreta tutti i simboli definiti in modo corretto rispetto alla mondo virtuale assiomatizzato; potete controllare la correttezza della interpretazione estesa confrontandola con il mondo rappresentato da i1.intp, che riportiamo qui sotto per facilitare il controllo.
Un mondo di TW
Fig.tw.8.b Il mondo rappresentato da i1.intp