Darf man in der Prädikatenlogik mathematische Terme nutzen?

Bsp: PL: f(x) = f(y) -> x = y

Dürfe ich es so ersetzen, dass x, y = 1 und f(x) = x ist? Das sähe dann so aus:

=>. 1 = 1. ->. 1 = 1

Und dann noch ne kurze Frage zur Unerfüllbarkeit: R(x, y). -> x = x

Wenn R(x, y) immer falsch ist, kann man alles nach dem Pfeil ignorieren, oder?