<p><code>DEDUCT_ANTISYM_RULE</code> only applies to propositions, while <code>REFL</code> 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.</p>

CC BY-SA 4.0
2020-06-09T06:42:11.487Z
Thank you Andrej
Łukasz Lew
CC BY-SA 4.0
2020-06-09T06:08:06.587Z
2020-06-09T06:08:06.587Z
Andrej Bauer
<p><a href="https://en.m.wikipedia.org/wiki/HOL_Light#logical_foundations" rel="nofollow noreferrer">HOL Light</a>
assumed <code>REFL</code> as a primitive.
Why does it need to do so?
Can't <code>REFL</code> rule be deduced in this way using <code>ASSUME</code> twice and <code>DEDUCT_ANTISYM_RULE</code> once?</p>

<p><span class="math-container">$$\frac{\overline{\{p\}\vdash p} \quad \overline{\{p\}\vdash p}}{\vdash p = p}$$</span></p>

CC BY-SA 4.0
2020-06-08T18:42:59.440Z
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.
Geoffrey Irving
<lo.logic><type-theory><proof-assistants><hol-light><hol>
Why REFL rule is primitive in HOL Light?
Łukasz Lew
# Why REFL rule is primitive in HOL Light?

(Asked by: username_0 on 2020-06-08)

[HOL Light](https://en.m.wikipedia.org/wiki/HOL_Light#logical_foundations)
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}$$

**Tags:** lo.logic, type-theory, proof-assistants, hol-light, hol
> **Comments:**
> **username_1**: 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.  

---

## 1 answers

### Answer by username_2 on 2020-06-09. Score: 6 | Accepted answer

`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.

> **Comments:**
> **username_0**: Thank you Andrej  

---

