In order answer questions like “What are X, anyway?”, we can (phenomenologically) turn the question into something like “What can we do with X?” or “What consequences does X have?”
For example, consider the question “What are ordered pairs, anyway?”. Sometimes you see “definitions” of ordered pairs in terms of set theory. Wikipedia says that the standard definition of ordered pairs is:
(a, b) := {{a}, {a, b}}
Many mathematicians find this “definition” unsatisfactory, and view it not as a definition, but an encoding or translation. The category-theoretic notion of a product might be more satisfactory. It pins down the properties that the ordered pair already had before the “definition” was proposed and in what sense ANY construction with those properties could be used. Lambda calculus has a couple constructions that look superficially quite different from the set-theory ones, but satisfy the category-theoretic requirements.
I guess this is a response at the meta level, recommending this sort of “phenomenological” lens as the way to resolve these sort of questions.
Lambda calculus has a couple constructions that look superficially quite different from the set-theory ones, but satisfy the category-theoretic requirements.
… as does the set-theoretic one.
ETA: Now that I read more closely, you didn’t imply otherwise.
In order answer questions like “What are X, anyway?”, we can (phenomenologically) turn the question into something like “What can we do with X?” or “What consequences does X have?”
For example, consider the question “What are ordered pairs, anyway?”. Sometimes you see “definitions” of ordered pairs in terms of set theory. Wikipedia says that the standard definition of ordered pairs is:
(a, b) := {{a}, {a, b}}
Many mathematicians find this “definition” unsatisfactory, and view it not as a definition, but an encoding or translation. The category-theoretic notion of a product might be more satisfactory. It pins down the properties that the ordered pair already had before the “definition” was proposed and in what sense ANY construction with those properties could be used. Lambda calculus has a couple constructions that look superficially quite different from the set-theory ones, but satisfy the category-theoretic requirements.
I guess this is a response at the meta level, recommending this sort of “phenomenological” lens as the way to resolve these sort of questions.
… as does the set-theoretic one.
ETA: Now that I read more closely, you didn’t imply otherwise.