Quería saber si para la el ERP de f en la ecuación de f(a<->b) podíamos definirlo como f(a<->b) = (f(a->b) ^ f(b->a)) ya habiendo definido f(a->b). Muchas gracias, un saludo.
Hola Juan Diego:
Si seguimos el ERP, en el lado derecho podés usar f(a) y f(b)
pero no podés usar (f(a->b) ni f(b->a)).
No quiere decir que no puedas definir una función usando una regla como esa. Lo que digo es que no cumple con el ERP de PROP y por lo tanto no es lo que pide el ejercicio