Another question about HOL

Another question about HOL
by Dennis J. Darland
July 31, 2008
Last revised 31.07.2008 09.28 time
Copyright © 2008 Dennis J. Darland
Another thought I had:

The main feature of HOL would seem to be quantifying over predicates.

But in a sense - don't all possible n-ary predicates exist?

E.g. For any two disjoint sets of ordered n-ary tuples A and B, you can define a relation such that the tuples in A are true and the ones in B are false.

Any n-ary predicates with finite extensions, at any rate, can be so defined with equality and "or"

It seemed to me elsewhere that not all, but only some, nary predicates with infinite extension exist - see on substances

But the successor relation would have a infinite extension - so its existence would seem to be contingent - at least along this line of reasoning!