Non primitiveness of "ix" (Grice, p. 139 in Davidson/Hintikka)

----

In taking up the second alternative and treat 'ix' as a quantifier, Grice proposes to define 'ix'.

----

Thus:

G₁ix₃ )(₈ Ex7Fx6 & (y)4F1y2 )(3 y2 =1 x2

is provable

by definitional substitutiona for the

right-hand size of the formula ... together

with applications of the rules

for subscript-adjustement."