FOM: on the definability of "polyadic comprehension"

Roger Bishop Jones rbjones at
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.

Roger Jones

More information about the FOM mailing list