Extensions of System GHP: higher orders

On p. 133, Grice considers the introduction of

a = b

using something like Leibniz's law for the identity of indescirnibles. He thus considers the second-order formulae of his natural deduction system:

The first formula is:


∀F₅F₁a₃ )(₂ F₁b₄


The second formula obviously bears different subscripts, and reads:

∀F₅F₁a₂ )(₄F₁b₃

---

Only in the first case are "a" and "b" dominant, and their existence

is IMPLIED. In the second case, it is merely "impicated".