I think I need to make explicit that universal introduction has to replace all instances of the given name with the variable. I think. I want to think a bit more about it but I realized we need to rule out a derivation of forall x Rax from Raa, in cases where a is arbitrary. (Suppose we have forall x Rxx as a premise.)
I think I need to make explicit that universal introduction has to replace all instances of the given name with the variable. I think. I want to think a bit more about it but I realized we need to rule out a derivation of forall x Rax from Raa, in cases where a is arbitrary. (Suppose we have forall x Rxx as a premise.)