Comment by foldr

Right, but you can't ensure that the only models of 'bijective functions' are actually bijective functions. To switch to a slightly simpler example, you can translate statements such as "x is finite" into a first order language (for example, set theory), but you can't ensure that x actually is finite in the models of this statement.