Caratteristiche del metalinguaggio della matematica

Salve a tutti. Volevo chiedervi quali devono essere le caratteristiche del metalinguaggio avente come linguaggio oggetto una teoria matematica (geometria, algebra, analisi...ecc) .

1) Deve essere anch'esso un linguaggio formalizzato? Hilbert diceva, se non mi sbaglio, che il metalinguaggio non era costituito da assiomi ed in esso non è necessario ricavare teoremi, tutte le affermazioni (come quelle dell'aritmetica finitaria) sono ovvie, intuitive immediate;

2) Deve contenere il principio di induzione finitaria giusto?

3) Volendo introdurre i valori di verità alla Tarski dobbiamo appoggiarci su predicati di verità (NEL METALINGUAGGIO) della forma: "p" è vera se e solo se p ove p è una generica affermazione (come ad esempio 2<3). Tarski richiede che il linguaggio oggetto sia contenuto nel metalinguaggio. Questo perchè nella frase in grassetto p compare a destra del se e solo se? Quella in grassetto è una formula nel metalinguaggio giusto? Dunque anche il se e solo se che compare in essa deve far parte del vocabolario del metalinguaggio?

C'è qualcosa di simile a trattare le teorie matematiche come oggetti matematici, ma certamente non è un metalinguaggio. Da che contesto parti?

Ciao caulacau, innanzitutto grazie per la tua risposta. Il punto di vista che sto adottando è quello iniziale di Hilbert. Lui in particolar modo parla di aritmetica finitaria come quella parte di aritmetica ovvia immediata che non necessita di dimostrazioni (Tait la identifica con l'aritmetica primitiva finitaria). In questo modo non avrebbe la necessità di essere formalizzata anch'essa. Del resto si comprende che se così non fosse avremmo bisogno pure di un meta-meta-linguaggio. In questo modo "retrocedendo all'infinito" non si troverebbero mai i fondamenti della matematica. Il fatto che il metalinguaggio sia autoevidente permette di spezzare questa catena infinita. Ora ho letto quello che ha fatto Godel, lui in pratica ha fatto vedere, se non mi sbaglio, che l'aritmetica può fare da metalinguaggio di sè stessa. Però, nel fare questo, è stato attento a non uscire dai canoni fissati da Hilbert (ovvero metadimostrazioni che si devono concludere in un numero finito di passi).
Il primo punto che vorrei chiederti è questo: se la metamatematica è così ovvia come mai esistono le metadimostrazioni (come la consistenza, la completezza)? Non dovrebbero essere evidenti questi fatti? Tu hai detto che non è la metamatematica che tratta le teorie matematiche come "oggetti di studio" Allora cos'è?

Tu hai detto che non è la metamatematica che tratta le teorie matematiche come "oggetti di studio" Allora cos'è?

https://ncatlab.org/nlab/show/category+theory