predicate

In the formula ∀F(Fx ↔ Fy) → x = y, F should be called a predicate variable or a property variable.

Here's why:

• Predicate/Property: In first-order logic, predicates (or properties) are represented by symbols like F, G, H, etc. These variables stand for any arbitrary property that can be applied to objects in the domain of discourse.
• Variable: The use of the universal quantifier (∀) indicates that the formula holds for any property that F might represent. This means F is not a specific, fixed property but rather a variable ranging over all possible properties.

Therefore, calling F a "premise" would be inaccurate because premises typically refer to specific propositions or statements within an argument, whereas F represents any arbitrary property. Calling it a "function" is also not quite right, as functions typically map objects to other objects, while predicates map objects to truth values (true or false).

So, in the context of the identity of indiscernibles formula, F is most accurately described as a predicate variable or a property variable. It allows us to express the principle that if two objects share all the same properties (regardless of what those properties might be), then those objects must be identical.