FOM: on the definability of "polyadic comprehension"
Roger Bishop Jones
rbjones at rbjones.com
Thu Sep 14 02:11:34 EDT 2000
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.
More information about the FOM