OP, la risposta breve a tutti i tuoi dubbi è che puoi formalizzarli, ma ti sarà del tutto inutile a capire la cosa che volevi capire 40 messaggi fa.
Il motivo della confusione è che stai mescolando due aspetti della faccenda: il linguaggio naturale, da un lato, cioè "se questo è vero, e questo implica quest'altro, allora quest'altro è vero", che non ha niente di ovvio, ma è semplicemente una presupposizione del nostro pensiero, e dall'altro il linguaggio formale in cui questo si rende preciso: si fissa un insieme di variabili, si definiscono i vari connettivi booleani (congiunzione, disgiunzione, implicazione, etc.), li si raccoglie in un insieme $L$ cosa che finora non ha attribuito nessun significato, cioè nessun valore di verità, e poi si fissa una funzione di interpretazione, da $L$ a un insieme di valori di verità, usando la struttura di algebra di Boole di questo insieme, e definendo per induzione, a partire dal valore di verità dei generatori, i valori di verità di \(p\land q,p\lor q,p\Rightarrow q\)... Viene fatto qui https://builds.openlogicproject.org/con ... -logic.pdf e il mio consiglio è (alternativamente)
o di lasciar perdere del tutto questi problemi, oppure di tornare a rispondere SOLO QUANDO LE PRIME DODICI PAGINE DI QUESTO TESTO TI SONO CRISTALLINAMENTE CHIARE.
Quando hai deciso, a tuo rischio, la seconda cosa, ti accorgerai che una "tautologia" non è un concetto metafisico, bensì è nient'altro che una formula "sempre vera rispetto a ogni valutazione". E il modus ponens è una tautologia, perché grazie alla definizione induttiva data per \(\varphi = p\land (p\Rightarrow q))\Rightarrow q\) si dimostra che \(\mathfrak v(\varphi)=true\) per ogni valutazione: infatti, questo riduce all'equazione
\[y\lor \lnot(x \land (y\lor \lnot x))\] vera nell'algebra dei Booleani. Se fai il conto, ti accorgerai che \(y\lor \lnot(x \land (y\lor \lnot x))\) è solo una parola lunga lunga per scrivere "1".