# Why REFL rule is primitive in HOL Light?

HOL Light assumed REFL as a primitive. Why does it need to do so? Can't REFL rule be deduced in this way using ASSUME twice and DEDUCT_ANTISYM_RULE once?

$$\frac{\overline{\{p\}\vdash p} \quad \overline{\{p\}\vdash p}}{\vdash p = p}$$

• I’m not sure, but it’s plausible this is just an optimization. You’d have to apply the above derivation for each desired $p$ separately. Jun 8 '20 at 18:42

DEDUCT_ANTISYM_RULE only applies to propositions, while REFL applies to all terms of all types. Your suggestion only shows that every propositions is equal (equivalent) to itself, but it could not be used to show that ever number equals itself.

• Thank you Andrej Jun 9 '20 at 6:42