3
$\begingroup$

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}$$

$\endgroup$
1
  • $\begingroup$ 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. $\endgroup$ Jun 8 '20 at 18:42
5
$\begingroup$

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.

$\endgroup$
1
  • $\begingroup$ Thank you Andrej $\endgroup$ Jun 9 '20 at 6:42

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.