Io non ho capito la formula, quindi dico delle cose generali.
che sat sia on operatore di relazione chi lo capisco può confermarlo e @leon_89 l’ha confermato. Detto questo mi pare strano che non esista un simbolo già predisposto e sul quale convengano gli utenti di “soddisfa a”; Nessun altro operatore di relazione appare scritto in lettere nell’antologia genarla dei simboli di Scop Pakin (texdoc symbols)-a4); anzi quata antologia lo riporta come sinonimo di \models che a sua volta è sinonimo di \rightmodels; antologia dei simboli, pagina 33, tabella 76 (che comincia nella pagina 32, ma quel che ci interessa è nella pagina 33).
tr non può essere una variabile; le variabili sono sì in corsivo ma sono fatte di una sola lettera con quante apposizioni si vuole, di solito le apposizione sono al priede, come dei deponenti e sono scritti in tondo.
Gli informatici mi hanno coperto di contumelie quando ho scritto una frase del genere in un mio articolo sulla composizione della matematica; evidentemente non hanno l’abitudine di leggere di che cosa si sta parlando, perché è vero che essi usano parole alfanumeriche che chiamano varibaili per rappresentare simbolicamante dei registri della CPU e/o delle parole di memoria, ma quelle non sono variabili matematiche. In matematicha, che si parli di scienze sperimentali o di scienze esatte, la matematica richiede variabili rappresentate da una sola lettera latina o greca, inclinata, e composta con caratteri diversi (con o senza grazie, nere, o chiare, calligrafiche o semplicemnte corsive) con quante apposizioni si vuole, scritte in tedno se rappresentano delle “qualifiche” della variabile, e scritte in cordico se rappresentano quantità che pososno variare e a cui la varibaile è legata.
Questo è quanto dice ogni manuale di tipografia che parli della composizione della matematica (di cui la logica mi par bene che sia una disciplina che nel forma il copro generale; mi esprimo male, ma come ho detto sono un vilis mechanicus) Le norme ISO impongono altre regole, ma non modificano di certo queste che ho appena detto. (per esempio, le norme ISO richiedono che le costanti matematiche come e, pi greca, gamma, e simili simboli) siano scritti in tondo, per distinguerli da simboli analoghi di cose misurabili, anche se fisicamente parlando sono o dovrebbero essere delle costanti della fisica).
Tornando alla soddisfacibilità, il comando \satidfies è sininimo di \models che a sua volta è siniimo di rightmodels. Non so se @leon_89, usa sat in quel senso, perché come ho detto non capisco il significato della formula. Colpa mia che non la capisco, ma suggerirei di dare un’occhiata all’antologia dei simboli, prima di inventarne di nuovi.