FOM: on the definability of "polyadic comprehension"

[Roger Bishop Jones]

Though its primitive is functional (lambda) abstraction rather than set or
property abstraction, Church's Simple Theory of Types (which is equivalent
to omega order logic) has abstraction over just one argument as primitive,
in terms of which pairing can be defined and functions over arbitrary tuples
are then definable.

It would certainly seem odd if a putative definition of logic were to
include the former but not the latter.

Roger Jones