Buenas, me quedo la siguiente duda de la prueba de correctitud :
En el paso base RI1 se afirma lo siguiente : t^M = t^M. Ahora, t es un termino cualquiera,en particular, podria estar abierto.
De lo que entendi de semantica t^M (La funcion de interpretacion en M) solo se puede aplicar a terminos cerrados, entonces porque se aplica en esta prueba a un termino cualquiera? Habria que hacer una clausura primero o alguna otra manipulacion o puedo aplicar ^M a terminos abiertos?
Ademas : creo que se menciono en las clases de deduccion antural que el simbolo =' podria denotar a cualquier relacion binaria que satisfaga los 4 axiomas (RI1,...,RI4), entonces porque podemos afirmar que su interpretacion es la igualdad para usar por ejemplo la reflexividad de = en M o la simetria en el paso de RI2?